囲碁や将棋をはじめとする二人零和有限確定完全情報ゲームにおいて 必勝法が存在するという証明が比較的に簡単にできることに感動を覚えたので、 \(\KaTeX \) 表記の練習がてら残しておこうと思う。
予備知識として量化子を用いたDe Morganの法則を使用する。 事象を \(P\) とするとき
$$ \begin{aligned} \overline{\exists x P} &= \forall x \overline{P} \\ \overline{\forall x P} &= \exists x \overline{P} \end{aligned} $$が成り立つ。 証明は一般的なDe Morganの法則より容易にできるので書かない。
ある二人零和有限確定完全情報ゲーム（引き分けも想定する）において、 必勝法が存在するとはどういうことか。 それは、自分が特定の手番（先手または後手）をもったとき、 相手がどんな合法手を指してきたとしても、 こちらがそれに応じたある手を指すことによって確実に勝利できるということである。
これを論理式で表現してみる。 先手 \(F\) と後手 \(S\) を想定し、先手がゲームに勝利するという事象を \(W_F\) とする。 行うゲームは \(n\) 手で終了するとする。（\(n\) は十分に大きな偶数としてよい）。 すると、ゲームは \(x_1, x_2, \dotsc, x_n\) の数列で表されることになる。
このとき、「このゲームは先手必勝である」という事象を \(P_F\) とすると、
$$ P_F = \exists x_1 \forall x_2 \exists x_3 \dotsc \forall x_n W_F $$と書ける。
ここで \(\overline{P_F}\) がどうなるかというと、
$$ \begin{aligned} \overline{P_F} &= \overline{\exists x_1 \forall x_2 \exists x_3 \dotsc \forall x_n W_F} \\ &= \forall x_1 \overline{\forall x_2 \exists x_3 \dotsc \forall x_n W_F} \\ &= \forall x_1 \exists x_2 \overline{\exists x_3 \dotsc \forall x_n W_F} \\ &= \dotsc \\ &= \forall x_1 \exists x_2 \forall x_3 \dotsc \exists x_n \overline{W_F} \end{aligned} $$と書ける。
\(\overline{W_F}\) が指す事象は先手が勝たないこと、つまり後手の勝利または引き分けである。 ここで
$$ \forall x_1 \exists x_2 \forall x_3 \dotsc \exists x_n \overline{W_F} $$が示すのは、「先手がどんな手を指したとしても、それに都度応じて後手がある手を指すことを続ければ、 必ず後手の勝利あるいは引き分けに終わる」ことである。 すなわち後手不敗である。
したがって上の式で証明できたのは、すべての二人零和有限確定完全情報ゲームにおいて
「先手必勝でなければ、後手不敗である」
ということである。 同様にすれば「後手必勝でなければ、先手不敗である」も証明可能である。 そしてこのふたつから以下のことがいえる。
すべての二人零和有限確定完全情報ゲームにおいて、先手あるいは後手のいずれかに不敗となる方法がある。
論理学は至極自明なことを定式化するだけだと思っていたが、 比較的非自明なことも語ってくれるのだという良い例だと思う。