二人零和有限確定完全情報ゲームにおける必勝法の存在

　囲碁や将棋をはじめとする二人零和有限確定完全情報ゲームにおいて必勝法が存在するという証明が比較的に簡単にできることに感動を覚えたので、はてなブログにおける $\TeX$ 表記の練習がてら残しておこうと思う。

　予備知識として量化子を用いたDe Morganの法則を使用する。

　 $P$ を事象とするとき

\begin{align} \overline{\exists x P} = \forall x \overline{P} \\\ \overline{\forall x P} = \exists x \overline{P} \end{align}

が成り立つ。

　証明は一般的なDe Morganの法則より容易にできるので書かない。

　ある二人零和有限確定完全情報ゲーム（引き分けも想定する）において、必勝法が存在するとはどういうことか。それは、自分が特定の手番（先手 or 後手）をもったとき、相手がどんな合法手を指してきたとしても、こちらがそれに応じたある手を指すことによって確実に勝利できるということである（より広義には、確実に敗北しないことを「必勝」と呼ぶ場合もあるので、語義に揺れがある。）。

　これを論理式で表現してみる。先手（F）と後手（S）を想定し、先手がゲームに勝利するという事象を $W _ F$ とする。行うゲームは $n$ 手で終了するとする（ $n$ は十分に大きな偶数としてよい。決着がついたあとの手はすべて「パス」で置き換えてしまえば問題ないからだ。）。すると、ゲームは $x _ 1, x _ 2, \dotsc , x _ n$ の数列で表されることになる。

　このとき、「このゲームは先手必勝である」という事象を $P _ F$ とすると、

\begin{align} P _ F = \exists x _ 1 \forall x _ 2 \exists x _ 3 \dotsc \forall x _ n W _ F \end{align}
と書ける。

　ここで、 $\overline{P _ F}$ がどうなるかというと、

\begin{align} \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{align}

と書けるのだ。

　 $\overline{W _ F}$ が指す事象は先手が勝たないこと、つまり後手の勝利または引き分けのいずれかに終わることである。つまりここで、最下段の