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

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

Во многих теоремах присутствуют утверждения с кванторами "для всех" и "существует". От того, в каком порядке кванторы входят в утверждение, зависит его смысл. Часто оказывается полезным представлять утверждения с кванторами как "игру", в которой участвуют два игрока - "для всех" и "существует". Есть выражение [math]\exists x_1 \forall x_2 \exists x_3 \dots Q x_n = \Psi(x_1,\dots ,x_n)[/math]. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. В зависимости от значения выражения после всех ходов. Цель игрока "существует" делать такие ходы, чтобы в конце получилась истина. А цель игрока "для всех" делать такие ходы, чтобы в конце получилась ложь.

Итак, есть выражение [math]\exists x_1 \forall x_2 \exists x_3 \dots Q x_n = \Psi(x_1,\dots ,x_n)[/math]. Если выражение [math]\Psi[/math] истинно, то у игрока "существует" есть такие ходы, чтобы прийти к победе. Если же выражение [math]\Psi[/math] ложно, то у игрока "для всех" есть такие ходы, чтобы прийти к победе. Докажем в случае, когда выражение [math]\Psi[/math] принимает истинное значение.

Докажем по индукции.

Для одного квантора. Если этот квантор "любой", то какой бы параметр не поставил игрок "для всех" выражение будет истинно по предположению. Если единственный квантор "существует", то по предположению есть такой параметр, что выражение будет истинно. Его и подставит игрок "существует", после чего сразу победит.

Пусть теперь верно для любого количества кванторов не превосходящих [math]n-1[/math]. Докажем для [math]n[/math] кванторов. Пусть первый квантор "существует", тогда [math]\Psi = \exists x_1 \Phi[/math]. По предположению найдётся такой параметр [math]x_1[/math], что [math]\Phi[/math] истинно. Но в выражении [math]\Phi \: n-1[/math] квантор, значит для [math]\Phi[/math] есть набор ходов. С выбранным [math]x_1[/math] и полученным набором ходов мы получим победную стратегию. Пусть теперь первый квантор "для всех", тогда [math]\Psi = \forall x_1 \exists x_2 \Phi[/math]. По предположению найдётся такой параметр [math]x_2[/math] для любого параметра [math]x_1[/math], что [math]\Phi[/math] истинно. Но в выражении [math]\Phi \: n-2[/math] квантора, значит для [math]\Phi[/math] есть набор ходов. С выбранным [math]x_2[/math] и полученным набором ходов мы получим победную стратегию.

Доказательство существования победной стратегии для игрока "для всех" при ложном выражении [math]\Psi[/math] аналогично.