Булевые формулы с кванторами как игры для двух игроков

Определение:

В игре участвуют два игрока — «для всех» и «существует». Есть утверждение $\exists x_1 \forall x_2 \exists x_3 \dots Q x_n \Psi(x_1,\dots ,x_n)\,$. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы утверждение $\exists x_1 \forall x_2 \exists x_3 \dots Q x_n \Psi(x_1,\dots ,x_n)\,$ получилось истинным. А цель игрока «для всех» делать такие ходы, чтобы итоговое выражение получилась ложным.

Интерпретация булевых формул с кванторами как игр для двух игроков

Теорема:

Дано утверждение: $P_1 = P_1(Q_1, \ldots, Q_n, \Psi(x_1,\dots ,x_n)) = Q_1 x_1 Q_2 x_2 \ldots Q_n x_n \Psi(x_1,\dots ,x_n),$ где $\{Q_i\}_{i=1}^{n}$ является чередующейся последовательностью кванторов $\forall$ и $\exists$. Если утверждение $P_1$ истинно, то у игрока «существует» есть набор ходов, используя который, он может победить. Если же утверждение $P_1$ ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.

Доказательство:

$\triangleright$

Выражение $P$ истинно. Провернём доказательство по индукции. База: в $P_1$ один квантор. Если единственный квантор — «любой», то какой бы параметр не поставил игрок «для всех» утверждение будет истинно по условию теоремы. Если единственный квантор — «существует», то, по условию, есть такой параметр, что утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит. Переход: теорема верна, когда утверждение $P_1$ содержит не более $n-1$ квантора, докажем, что она верна и для утверждений, содержащих $n$ кванторов. Пусть первый квантор «существует», тогда $P_1 = \exists x_1 P_2$, где $P_2 = P_2(Q_2, \ldots, Q_n, \Psi(x_1,\dots ,x_n)_{x_1=const})\,$. По условию теоремы найдётся такой параметр $x_1 = x_{1_0}$, что $P_1$ истинно. Но выражение $P_2$ истинно и содержит $n-1$ квантор, значит, для $P_2$ есть набор ходов игрока «существует», при котором он выигрывает. С выбранным $x_1 = x_{1_0}$ и полученным набором ходов мы получаем выигрышную стратегию. Пусть теперь первый квантор «для всех», тогда $P_1 = \forall x_1 \exists x_2 P_3$, где $P_3 = P_3(Q_3, \ldots, Q_n, \Psi(x_1, x_2,\dots ,x_n)_{x_1=const, x_2=const})\,$. По условию теоремы для любого параметра $x_1$ найдётся такой параметр $x_2 = x_{2_0}$, что $P_1$ истинно. Но утверждение $P_3$ истинно и содержит $n-2$ квантора, значит, для $P_3$ есть набор ходов игрока «существует», при котором он выигрывает. С выбранным $x_2 = x_{2_0}$ и полученным набором ходов мы получим выигрышную стратегию. Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении $\Psi$ аналогично.

$\triangleleft$

См. также

• Доказательство нерегулярности языков: лемма о разрастании
• Лемма о разрастании для КС-грамматик

Источники информации

• Wikipedia — True quantified Boolean formula