Интерпретация булевых формул с кванторами как игр для двух игроков — различия между версиями
Leugenea (обсуждение | вклад) (Полностью переделано оформление + исправлено много чего в тексте) |
|||
Строка 3: | Строка 3: | ||
Во многих теоремах присутствуют утверждения с кванторами «для всех» и «существует». От того, в каком порядке кванторы входят в утверждение, зависит его смысл. Часто оказывается полезным представлять утверждения с кванторами как «игру», в которой участвуют два игрока — «для всех» и «существует». Есть выражение <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>. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы в конце получилась истина. А цель игрока «для всех» делать такие ходы, чтобы в конце получилась ложь. | ||
− | Итак, есть выражение | + | Итак, есть выражение |
− | + | {{Теорема | |
− | + | |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> состоит не более, чем из <tex>n-1</tex> кванторов, докажем, что она верна и для выражений, состоящих из <tex>n</tex> кванторов. | ||
+ | #*: Пусть первый квантор «существует», тогда <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> аналогично. | ||
+ | }} | ||
[[Категория: Теория формальных языков]] | [[Категория: Теория формальных языков]] | ||
[[Категория: Автоматы и регулярные языки]] | [[Категория: Автоматы и регулярные языки]] |
Версия 08:17, 17 января 2012
Интерпретация булевых формул с кванторами как игр для двух игроков
Во многих теоремах присутствуют утверждения с кванторами «для всех» и «существует». От того, в каком порядке кванторы входят в утверждение, зависит его смысл. Часто оказывается полезным представлять утверждения с кванторами как «игру», в которой участвуют два игрока — «для всех» и «существует». Есть выражение
. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы в конце получилась истина. А цель игрока «для всех» делать такие ходы, чтобы в конце получилась ложь.Итак, есть выражение
Теорема: |
|
Доказательство: |
|