editor
177
правок
Изменения
Фиксы в формулировках и русском языке
==Интерпретация булевых формул с кванторами как игр для двух игроков==
Во многих теоремах присутствуют утверждения с кванторами «для всех» и «существует». От того, в каком порядке кванторы входят в утверждение, зависит его смысл. Часто оказывается полезным представлять утверждения с кванторами как «игру», в которой участвуют два игрока — «для всех» и «существует». Есть выражение <tex>\exists x_1 \forall x_2 \exists x_3 \dots Q x_n = \Psi(x_1,\dots ,x_n)</tex>. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы в конце получилась истинаитоговое выражение получилось истинным. А цель игрока «для всех» делать такие ходы, чтобы в конце итоговое выражение получилась ложьложным.
{{Теорема
|statement=
<tex>\Psi(x_1,\dots ,x_n) = \exists x_1 \forall x_2 \exists x_3 \dots Q x_n</tex> {{---}} выражение.
# Если выражение <tex>\Psi</tex> истинно, то у игрока «существует» есть такие ходынабор ходов, чтобы прийти к победеиспользуя который, он может победить.# Если же выражение <tex>\Psi</tex> ложно, то у игрока «для всех» есть такие ходынабор ходов, используя который, чтобы прийти к победеон может победить.
|proof=
# Доказательство Выражение <tex>\Psi</tex> истинно. Провернём доказательство по индукции.
#* '''База:''' квантор один.
#*: Если единственный квантор {{---}} «любой», то какой бы параметр не поставил игрок «для всех» выражение будет истинно по условию теоремы.
