170
правок
Изменения
Нет описания правки
Для каждого символа <tex>s \in \Pi</tex> заведём константу <tex>s</tex>, для каждого состояния <tex>q \in Q</tex> заведём константу <tex>q</tex>. Чтобы специальным образом кодировать ленту, введём две двухместные функции: <tex>|</tex> и <tex>\cdot</tex>, а также одноместную функцию <tex>g</tex>. [[ Машина Тьюринга#conf | Конфигурацию ]] <tex>\langle c_0 c_1 \ldots c_{l - 1}, q, c_l \ldots c_m \rangle</tex> теперь можно представить следующей формулой (опять же будем использовать инфиксную запись для удобства):
* <tex>q | c_0 \cdot c_1 \cdot \ldots \cdot c_{l - 1} \cdot g(c_l) \cdot c_{l + 1} \cdot \ldots \cdot c_m</tex>
Заведём множество формул <tex>A</tex>. Для каждого перехода, сдвигающего головку влевавлево, <tex>\delta(q, c_1) = \langle p, c_2, \leftarrow \rangle</tex> добавим в <tex>A</tex> формулу <tex>\forall x \forall y ((q | x \cdot c_0 \cdot g(c_1) \cdot y) = (p | x \cdot g(c_0) \cdot c_2 \cdot y))</tex>. Для переходов, сдвигающих головку вправо или оставляющих на месте, аналогичным образом добавим соответствующие формулы в <tex>A</tex>.
Также введём предикат <tex>yes</tex> и добавим в <tex>A</tex> формулу <tex>\forall x (yes(Y | x))</tex>.
Заметим, что по построению из <tex>A_0 \& A_1 \& \ldots \& A_n</tex> следует равенство двух формул, кодирующих любые две конфигурации <tex>C_1</tex> и <tex>C_2</tex>, такие что <tex>C_1 \vdash^* C_2</tex>. Поскольку предикат равенства согласован с предикатными символами (в частности с <tex>yes</tex>), то оценка <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> совпадает с оценкой <tex>yes(u)</tex>, где <tex>u</tex> {{---}} формула, кодирующая некую конфигурацию <tex>C</tex>, что <tex>C_0 \vdash^* C</tex>, где <tex>C_0</tex> {{---}} начальная конфигурация, опять же при условии <tex>A_0 \& A_1 \& \ldots \& A_n</tex>.
Если <tex>M</tex> допускает <tex>w</tex>, то <tex>C_0 \vdash^* \langle u, Y, v \rangle</tex>, поэтому оценка <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> совпадает с оценкой <tex>yes(Y|x)</tex> для какого-то <tex>x</tex>. По построению из <tex>A_0 \& A_1 \& \ldots \& A_n</tex> в частности следует, что <tex>\forall x (yes(Y | x))</tex>, а значит, в этом случае <tex>f(\langle M, w \rangle)</tex> оказывается общезначима.
Если же <tex>M</tex> не допускает <tex>w</tex>, то и доказательства для <tex>f(\langle M, w \rangle)</tex> существовать не будет. Это вытекает из того факта, что во всём множестве <tex>A</tex> присутствует лишь одна формула, содержащая предикат <tex>yes</tex> {{---}} <tex>\forall x (yes(Y | x))</tex>. Поэтому доказать следование <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> можно лишь через эту формулу. Для подмены аргументов в предикатах существуют только аксиомы равенства, но а <tex>(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> не равна никакой другой формуле вида <tex>(Y | x)</tex>, поэтому от <tex>\forall x (yes(S Y | x_0 \cdot x_1 \cdot \ldots \cdot x_kx)</tex> не перейти к ни к какой другой формуле вида <tex>yes(Y S | xx_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex>, а значит, и доказательство <tex>f(\langle M, w \rangle)</tex> построить не удастся, поэтому . Поэтому эта формула не будет общезначимой.
Таким образом, <tex>U \le_{m} L</tex>, а значит, <tex>L</tex> неразрешим, поскольку <tex>U</tex> неразрешим.
