editor
177
правок
Изменения
м
→Интерпретация булевых формул с кванторами как игр для двух игроков
#*: Пусть первый квантор «существует», тогда <tex>\Psi = \exists x_1 \Phi</tex>. По условию теоремы найдётся такой параметр <tex>x_1</tex>, что <tex>\Phi</tex> истинно. Но выражение <tex>\Phi</tex> состоит из <tex>n-1</tex> квантора, значит, для <tex>\Phi</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_1</tex> и полученным набором ходов мы получаем выигрышную стратегию.
#*: Пусть теперь первый квантор «для всех», тогда <tex>\Psi = \forall x_1 \exists x_2 \Phi</tex>. По условию теоремы для любого параметра <tex>x_1</tex> найдётся такой параметр <tex>x_2</tex>, что <tex>\Phi</tex> истинно. Но выражение <tex>\Phi</tex> содержит <tex>n-2</tex> квантора, значит, для <tex>\Phi</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_2</tex> и полученным набором ходов мы получим выигрышную стратегию.
# Доказательство существования выигрышной стратегии для игрока «для всех» при ложном выражении <tex>\Psi</tex> аналогично.
}}
[[Категория: Теория формальных языков]]
[[Категория: Автоматы и регулярные языки]]
