非構成的

多項式時間での解法が存在することが示されているにも関わらず、それを実際にどうやったらいいか分からない問題がある、という話を聞きました。グラフの一部をくっつけて簡略するマイナーという操作によって閉じているグラフの族に属しているかは、有限個の禁止マイナーのどれかを持つか否かと同値になるそうです。が、非構成的な証明なので対応する禁止マイナーが何かは分からず、結果的に解法の存在は分かっていても、具体的な手続きは分からないのだそうです。

非構成的 I

quiz

n*m の長方形のタイルがある。
先手後手が交互にタイルを取っていく。最後のタイルを取ったほうが負けである。あるタイルが取られたときにそれ以降それよりも右下にあるタイルは取れない。たとえば、タイルが 5*5 だったとしよう。はじめに左上のタイルのすぐ右下のタイルを取ると、取られていないタイルを■、取れないタイルを□であらわすと

■ ■ ■ ■ ■
■ □ □ □ □
■ □ □ □ □
■ □ □ □ □
■ □ □ □ □

あとは、斜めの軸に対称になるように取っていけば先手が勝てる。

さて、このゲームは (n,m) がどういう数のときに先手必勝か。

非構成的 II

quiz

n 以下の正整数が並んでいる。先手後手交互に並んでいる数字のどれかを言う。言われた数字の約数がその後すべて言えなくなる。数字を言えなくなった方が負け。
たとえば、n が 4 のときに、先手がはじめに 2 といえば、2の約数である 1,2 が言えなくなり、残りが 3,4 なので先手が勝てる。
さて、このゲームは n がどういう数のときに先手必勝か。

Herbrand

証明もその否定の証明もできないような命題 A があったとして、論理式φをφ(x) = (x=0 and A) or (x=1 and not A) とすると、「φ(0) or φ(1)」である。でも、「φ(0)」、「φ(1)」のどちらも示せないことが分かる。
∃ は or のようなものですから。