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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Переформулировка теоремы. Теперь она, кажется, нормальная)
(Убрано много-премного бреееееда)
Строка 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>. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы утверждение <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) = Q_1 x_1 Q_2 x_2 \dots Q_n x_n</tex>, где <tex>\{Q_i\}_{i=1}^{n}</tex> является чередующейся последовательностью кванторов <tex>\forall</tex> и <tex>\exists</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 ,x_n)</tex>, где <tex>\{Q_i\}_{i=1}^{n} </tex> является чередующейся последовательностью кванторов <tex>\forall</tex> и <tex>\exists</tex>.
# Если выражение <tex>\Psi</tex> истинно, то у игрока «существует» есть набор ходов, используя который, он может победить.
+
# Если утверждение <tex>P_1</tex> истинно, то у игрока «существует» есть набор ходов, используя который, он может победить.
# Если же выражение <tex>\Psi</tex> ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.
+
# Если же утверждение <tex>P_1</tex> ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.
 
|proof=
 
|proof=
# Выражение <tex>\Psi</tex> истинно. Провернём доказательство по индукции.
+
# Выражение <tex>P</tex> истинно. Провернём доказательство по индукции.
#* '''База:''' квантор один.
+
#* '''База:''' в <tex>P_1</tex> один квантор.
#*: Если единственный квантор {{---}} «любой», то какой бы параметр не поставил игрок «для всех» выражение будет истинно по условию теоремы.
+
#*: Если единственный квантор {{---}} «любой», то какой бы параметр не поставил игрок «для всех» утверждение будет истинно по условию теоремы.
#*: Если единственный квантор {{---}} «существует», то, по условию, есть такой параметр, что выражение будет истинно. Его и подставит игрок «существует», после чего сразу победит.
+
#*: Если единственный квантор {{---}} «существует», то, по условию, есть такой параметр, что утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит.
#* '''Переход:''' теорема верна, когда выражение <tex>\Psi</tex> состоит не более, чем из <tex>n-1</tex> кванторов, докажем, что она верна и для выражений, состоящих из <tex>n</tex> кванторов.
+
#* '''Переход:''' теорема верна, когда утверждение <tex>P_1</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>P_1 = \exists x_1 P_2</tex>, где <tex>P_2 = P_2(Q_2, \ldots, Q_n, \Psi(x_1,\dots ,x_n)_{x_1=const})</tex>. По условию теоремы найдётся такой параметр <tex>x_1 = x_{1_0}</tex>, что <tex>P_1</tex> истинно. Но выражение <tex>P_2</tex> истинно и содержит <tex>n-1</tex> квантор, значит, для <tex>P_2</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_1 = x_{1_0}</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>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, \dots ,x_n)_{\forall x_1, x_2=const})</tex>. По условию теоремы для любого параметра <tex>x_1</tex> найдётся такой параметр <tex>x_2 = x_{2_0}</tex>, что <tex>P_1</tex> истинно. Но утверждение <tex>P_3</tex> истинно и содержит <tex>n-2</tex> квантора, значит, для <tex>P_3</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_2 = x_{2_0}</tex> и полученным набором ходов мы получим выигрышную стратегию.
 
# Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении <tex>\Psi</tex> аналогично.
 
# Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении <tex>\Psi</tex> аналогично.
 
}}
 
}}

Версия 08:53, 21 января 2012

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

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

Теорема:
Дано утверждение: [math]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 ,x_n)[/math], где [math]\{Q_i\}_{i=1}^{n} [/math] является чередующейся последовательностью кванторов [math]\forall[/math] и [math]\exists[/math].
  1. Если утверждение [math]P_1[/math] истинно, то у игрока «существует» есть набор ходов, используя который, он может победить.
  2. Если же утверждение [math]P_1[/math] ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.
Доказательство:
[math]\triangleright[/math]
  1. Выражение [math]P[/math] истинно. Провернём доказательство по индукции.
    • База: в [math]P_1[/math] один квантор.
      Если единственный квантор — «любой», то какой бы параметр не поставил игрок «для всех» утверждение будет истинно по условию теоремы.
      Если единственный квантор — «существует», то, по условию, есть такой параметр, что утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит.
    • Переход: теорема верна, когда утверждение [math]P_1[/math] содержит не более [math]n-1[/math] квантора, докажем, что она верна и для утверждений, содержащих [math]n[/math] кванторов.
      Пусть первый квантор «существует», тогда [math]P_1 = \exists x_1 P_2[/math], где [math]P_2 = P_2(Q_2, \ldots, Q_n, \Psi(x_1,\dots ,x_n)_{x_1=const})[/math]. По условию теоремы найдётся такой параметр [math]x_1 = x_{1_0}[/math], что [math]P_1[/math] истинно. Но выражение [math]P_2[/math] истинно и содержит [math]n-1[/math] квантор, значит, для [math]P_2[/math] есть набор ходов игрока «существует», при котором он выигрывает. С выбранным [math]x_1 = x_{1_0}[/math] и полученным набором ходов мы получаем выигрышную стратегию.
      Пусть теперь первый квантор «для всех», тогда [math]P_1 = \forall x_1 \exists x_2 P_3[/math], где [math]P_3 = P_3(Q_3, \ldots, Q_n, \Psi(x_1, x_2, \dots ,x_n)_{\forall x_1, x_2=const})[/math]. По условию теоремы для любого параметра [math]x_1[/math] найдётся такой параметр [math]x_2 = x_{2_0}[/math], что [math]P_1[/math] истинно. Но утверждение [math]P_3[/math] истинно и содержит [math]n-2[/math] квантора, значит, для [math]P_3[/math] есть набор ходов игрока «существует», при котором он выигрывает. С выбранным [math]x_2 = x_{2_0}[/math] и полученным набором ходов мы получим выигрышную стратегию.
  2. Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении [math]\Psi[/math] аналогично.
[math]\triangleleft[/math]