Изменения

Во многих теоремах присутствуют утверждения с кванторами «для всех» и «существует». От того, в каком порядке кванторы входят в утверждение, зависит его смысл. Часто оказывается полезным представлять утверждения с кванторами как «игру», в которой {{Определение|definition = В игре участвуют два игрока — {{---}} «для всех» и «существует». Есть утверждение <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> получилось истинным. А цель игрока «для всех» делать такие ходы, чтобы итоговое выражение получилась ложным.}}</noinclude><includeonly>{{#if:{{{id|}}}|<span id="{{{id}}}"></span>|}}{{#if: {{{neat|}}}|<div style="background-color: #fcfcfc; float:left;"><div style="background-color: #ddd;">'''Определение:'''</div><div style="border:1px dashed #2f6fab; padding: 8px;">{{{definition}}}</div></div>|<table border="0" width="100%"><tr><td style="background-color: #ddd">'''Определение:'''</td></tr><tr><td style="border:1px dashed #2f6fab; padding: 8px; background-color: #fcfcfc;">{{{definition}}}</td></tr></table>}}</includeonly>

Дано утверждение: <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>.

*[https://en.wikipedia.org/wiki/True_quantified_Boolean_formula| Wikipedia {{---}} True quantified Boolean formula]

[[Категория:Свойства конечных автоматовМатематическая логика]]