Изменения

'''if''' <tex>Q_1 == \forall</tex>

'''if''' <tex>Q_1 == \exists</tex>

Построим такую функцию <tex>f \colon \forall </tex>, что <tex>x \in L \Leftrightarrow f(x) \in TQBF</tex> и <tex>T(f, x) \le p(|x|)</tex>. Так как <tex>L \in \mathrm{PS}</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая распознающая его распознаёт за полиномиальное от с использованием памяти полиномиального размера входа время. Пусть <tex>I</tex> — мгновенное описание конфигурация <tex>M</tex>. Размер конфиграции есть <tex>r(n)</tex>, где <tex>n</tex> — длина входа, тогда <tex>r</tex> — некоторый полином. Тогда выражение <tex>\exists I</tex> обозначает <tex> (\exists x_1x_0^I) (\exists x_2x_1^I)\cdotsdots(\exists x_nx_{r(n)}^I)</tex>, где <tex>\{x_i^I\}</tex> — все переменные мгновенного описания конфигурации <tex>MI</tex>. Аналогично выражение <tex> \forall I</tex> обозначает <tex> (\forall x_1x_0^I) (\forall x_2x_1^I)\dots(\forall x_nx_{r(n)}^I)</tex>. Теперь рассмотрим два мгновенных описания Всего конфигурации у ДМТ <tex>M\, O(p(n))</tex>, где <tex>p</tex> — некоторый полином. Рассмотрим функцию <tex>\phi(A, B, t)</tex>, проверяющую следующее условие: конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> и не более, чем за <tex>2^t</tex> шагов. <tex>\phi(A, B, 0) = (A = B) \lor (A \vdash B)</tex>. Напишем рекурсивную функцию  <tex>\phi(A, B, t) = \exists R \, \phi(A, R, t-1) \land \phi(R, B, t-1)</tex>. Заметим, что данная формула имеет экспоненциальный размер длины, которая будет переводить утверждение поэтому воспользуемся квантором <tex>\forall</tex> и перепишем её следующим образом: <tex>\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, t-1) \lor [\neg(U = A\vdash^tBland V = R) \land \neg(U = R \land V = B)]\}</tex> в . Размер полученной функции <tex>TQBF\phi(A, B, t)</tex> за полиномиальное полиномиален относительно длины входа время<tex>n</tex>.

<tex>\phi(A, B, t) = \\ (\exists R) (\forall U) (\forall V) \ \{\phi(U, V, t/2) \lor [\neg(A = U \land R = V) \land \neg(R = U \land B = V)]\}</tex> :Переменые <tex> U </tex> и <tex>V</tex> важно рассмотреть только в двух случаях: когда первое из них стартовое, второе — промежуточное, или первое — промежуточное, а второе — финишное. Поэтому для всех остальных вариантов выражение <tex>[\neg(A = U \land R = V) \land \neg(R = U \land B = V)]</tex> будет истинно. Если <tex>A = U \land R = V</tex> то, чтобы <tex>\phi(A, B, t)</tex> было истинно, необходимо наличие такого мгновенного описания <tex>R</tex>, чтобы было выполненно утверждение: <tex>A\vdash^{t/2}R</tex>. Если <tex>R = U \land B = V</tex> то, нас интересует мгновенное описание <tex>R</tex> такое, что <tex>R\vdash^{t/2}B</tex>.Заметим, что размер функции <tex>\phi(A, B, t)</tex> равен размеру <tex>\phi(A, B, t/2)</tex> с константной добавкой <tex>(\exists R) (\forall U) (\forall V) \ \{\ * \lor [\neg(A = U \land B = R) \land \neg(A = R \land B = V)]\}</tex> .Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>TQBF</tex>.

<tex>f(M, w) = (\exists I_sI_{st}) (\exists I_fI_{fin}) (x_x_0^{I_{I_s, 0st}} = start \land x_x_1^{I_{I_s, 1st}} = w[1] \land \dots \land x_{I_s, |w|^{I_{st}} = w[|w|]) \land ((\exists i) x_\, x_i^{I_{I_f, ifin}} = finish) \land \phi(StartI_{st}, FinishI_{fin}, log_2(2^{log_2O(c^{1+p(n))}})))</tex>.

Докажем, что получившаяся булева формула с кванторами удовлетворима тогда и только тогда, когда сведение <tex>w \in Lf</tex>верное.

Если <tex>w \in L</tex>, то стартовое и финишное состояние заданы корректно. Также существует путь из стартового состояния можно попасть стартовой конфигурации в финишное за полиномиальное времяфинишную, причём длины не более чем <tex>2^{O(p(n))}</tex>, а значит формула <tex>\phi</tex> верна.

Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартовой конфигурации в финишную не более чем <tex>2^{O(p(n))}</tex>. Значит, ДМТ <tex>M</tex> допускает слово <tex>w</tex>. Тогда <tex>w \not\in L</tex>, то если мы зададим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.