Изменения

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

Дано выражениеутверждение: <tex>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 Q_n ,x_n)</tex>, где <tex>\{Q_i\}_{i=1}^{n}</tex> является чередующейся последовательностью кванторов <tex>\forall</tex> и <tex>\exists</tex>.# Если выражение утверждение <tex>\PsiP_1</tex> истинно, то у игрока «существует» есть набор ходов, используя который, он может победить.# Если же выражение утверждение <tex>\PsiP_1</tex> ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.

# Выражение <tex>\PsiP</tex> истинно. Провернём доказательство по индукции.#* '''База:''' в <tex>P_1</tex> один квантор один.#*: Если единственный квантор {{---}} «любой», то какой бы параметр не поставил игрок «для всех» выражение утверждение будет истинно по условию теоремы.#*: Если единственный квантор {{---}} «существует», то, по условию, есть такой параметр, что выражение утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит.#* '''Переход:''' теорема верна, когда выражение утверждение <tex>\PsiP_1</tex> состоит содержит не более, чем из <tex>n-1</tex> кванторовквантора, докажем, что она верна и для выраженийутверждений, состоящих из содержащих <tex>n</tex> кванторов.#*: Пусть первый квантор «существует», тогда <tex>P_1 = \Psi exists x_1 P_2</tex>, где <tex>P_2 = P_2(Q_2, \ldots, Q_n, \exists Psi(x_1 ,\Phidots ,x_n)_{x_1=const})</tex>. По условию теоремы найдётся такой параметр <tex>x_1= x_{1_0}</tex>, что <tex>\PhiP_1</tex> истинно. Но выражение <tex>\PhiP_2</tex> состоит из истинно и содержит <tex>n-1</tex> квантораквантор, значит, для <tex>\PhiP_2</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_1= x_{1_0}</tex> и полученным набором ходов мы получаем выигрышную стратегию.#*: Пусть теперь первый квантор «для всех», тогда <tex>\Psi P_1 = \forall x_1 \exists x_2 P_3</tex>, где <tex>P_3 = P_3(Q_3, \ldots, Q_n, \Psi(x_1, x_2, \Phidots ,x_n)_{\forall x_1, x_2=const})</tex>. По условию теоремы для любого параметра <tex>x_1</tex> найдётся такой параметр <tex>x_2= x_{2_0}</tex>, что <tex>\PhiP_1</tex> истинно. Но выражение утверждение <tex>\PhiP_3</tex> истинно и содержит <tex>n-2</tex> квантора, значит, для <tex>\PhiP_3</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_2= x_{2_0}</tex> и полученным набором ходов мы получим выигрышную стратегию.