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

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

Версия 08:29, 17 января 2012

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

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

Теорема:
[math]\Psi(x_1,\dots ,x_n) = \exists x_1 \forall x_2 \exists x_3 \dots Q x_n[/math] — выражение.
  1. Если выражение [math]\Psi[/math] истинно, то у игрока «существует» есть набор ходов, используя который, он может победить.
  2. Если же выражение [math]\Psi[/math] ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.
Доказательство:
[math]\triangleright[/math]
  1. Выражение [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[/math] состоит из [math]n-1[/math] квантора, значит, для [math]\Phi[/math] есть набор ходов игрока «существует», при котором он выигрывает. С выбранным [math]x_1[/math] и полученным набором ходов мы получаем выигрышную стратегию.
      Пусть теперь первый квантор «для всех», тогда [math]\Psi = \forall x_1 \exists x_2 \Phi[/math]. По условию теоремы для любого параметра [math]x_1[/math] найдётся такой параметр [math]x_2[/math], что [math]\Phi[/math] истинно. Но выражение [math]\Phi[/math] содержит [math]n-2[/math] квантора, значит, для [math]\Phi[/math] есть набор ходов игрока «существует», при котором он выигрывает. С выбранным [math]x_2[/math] и полученным набором ходов мы получим выигрышную стратегию.
  2. Доказательство существования выигрышной стратегии для игрока «для всех» при ложном выражении [math]\Psi[/math] аналогично.
[math]\triangleleft[/math]