Неразрешимость исчисления предикатов первого порядка — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(См. также)
Строка 4: Строка 4:
 
|proof=
 
|proof=
 
Обозначим язык всех общезначимых формул <tex>L = \{w | w</tex> {{---}} общезначимая формула исчисления предикатов первого порядка<tex>\}</tex>. Покажем, что [[Разрешимые (рекурсивные) языки#uni | универсальный язык]] <tex>U</tex> [[m-сводимость | m-сводится]] к <tex>L</tex>. Для этого нужно построить вычислимую функцию <tex>f</tex>, которая принимает на вход пару из [[ Машина Тьюринга | машины Тьюринга ]] <tex>M = \langle \Sigma, \Pi, B, Q, Y, N, S, \delta \rangle</tex> и слова <tex>w</tex> и возвращает некоторую формулу исчисления предикатов, причём:
 
Обозначим язык всех общезначимых формул <tex>L = \{w | w</tex> {{---}} общезначимая формула исчисления предикатов первого порядка<tex>\}</tex>. Покажем, что [[Разрешимые (рекурсивные) языки#uni | универсальный язык]] <tex>U</tex> [[m-сводимость | m-сводится]] к <tex>L</tex>. Для этого нужно построить вычислимую функцию <tex>f</tex>, которая принимает на вход пару из [[ Машина Тьюринга | машины Тьюринга ]] <tex>M = \langle \Sigma, \Pi, B, Q, Y, N, S, \delta \rangle</tex> и слова <tex>w</tex> и возвращает некоторую формулу исчисления предикатов, причём:
* <tex>f(\langle M, w \rangle) \in L \iff M</tex> попадает в допускающее состояние <tex>Y</tex> на входе <tex>w</tex>.
+
:<tex>f(\langle M, w \rangle) \in L \iff M</tex> попадает в допускающее состояние <tex>Y</tex> на входе <tex>w</tex>.
 
Введём двухместный предикат <tex>=</tex> со следующими аксиомами равенства (для удобства будем использовать инфиксную запись):
 
Введём двухместный предикат <tex>=</tex> со следующими аксиомами равенства (для удобства будем использовать инфиксную запись):
* <tex>\forall x (x = x)</tex> {{---}} рефлексивность;
+
* <tex>\forall x (x = x)</tex> {{---}} [[Рефлексивное отношение | рефлексивность]],
* <tex>\forall x \forall y (x = y \rightarrow y = x)</tex> {{---}} симметричность;
+
* <tex>\forall x \forall y (x = y \rightarrow y = x)</tex> {{---}} [[Симметричное отношение | симметричность]],
* <tex>\forall x \forall y \forall z ((x = y \& y = z) \rightarrow x = z)</tex> {{---}} транзитивность;
+
* <tex>\forall x \forall y \forall z ((x = y \wedge y = z) \rightarrow x = z)</tex> {{---}} [[Транзитивное отношение | транзитивность]],
* для каждой функции <tex>f</tex> от <tex>n</tex> аргументов <tex>\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \& \ldots \& x_n = y_n) \rightarrow f(x_1, \ldots x_n) = f(y_1, \ldots y_n)</tex>  {{---}} согласованность с функциональными символами;
+
* для каждой функции <tex>f</tex> от <tex>n</tex> аргументов <tex>\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \wedge \ldots \wedge x_n = y_n) \rightarrow f(x_1, \ldots x_n) = f(y_1, \ldots y_n)</tex>  {{---}} согласованность с функциональными символами,
* для каждого предиката <tex>p</tex> от <tex>n</tex> аргументов <tex>\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \& \ldots \& x_n = y_n) \rightarrow (p(x_1, \ldots x_n) \rightarrow p(y_1, \ldots y_n))</tex>  {{---}} согласованность с предикатными символами.
+
* для каждого предиката <tex>p</tex> от <tex>n</tex> аргументов <tex>\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \wedge \ldots \wedge x_n = y_n) \rightarrow (p(x_1, \ldots x_n) \rightarrow p(y_1, \ldots y_n))</tex>  {{---}} согласованность с предикатными символами.
 
Для каждого символа <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>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>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>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>.
  
Строка 20: Строка 20:
  
 
Теперь можно построить формулу <tex>f(\langle M, w \rangle)</tex>:
 
Теперь можно построить формулу <tex>f(\langle M, w \rangle)</tex>:
* <tex>(A_0 \& A_1 \& \ldots \& A_n) \rightarrow yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex>, где <tex>x_0 x_1 \ldots x_k = w</tex>.
+
:<tex>(A_0 \wedge A_1 \wedge \ldots \wedge A_n) \rightarrow yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex>, где <tex>x_0 x_1 \ldots x_k = w</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>A_0 \wedge A_1 \wedge \ldots \wedge 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 \wedge A_1 \wedge \ldots \wedge 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>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 \wedge A_1 \wedge \ldots \wedge 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(Y | x)</tex> не перейти к <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</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(Y | x)</tex> не перейти к <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex>, а значит, и доказательство <tex>f(\langle M, w \rangle)</tex> построить не удастся. Поэтому эта формула не будет общезначимой.
Строка 31: Строка 31:
  
 
== См. также ==
 
== См. также ==
* [http://neerc.ifmo.ru/wiki/index.php?title=%D0%98%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5_%D0%BF%D1%80%D0%B5%D0%B4%D0%B8%D0%BA%D0%B0%D1%82%D0%BE%D0%B2 Исчисление предикатов]
+
* [[Исчисление предикатов]]
* [http://neerc.ifmo.ru/wiki/index.php?title=%D0%A0%D0%B0%D0%B7%D1%80%D0%B5%D1%88%D0%B8%D0%BC%D1%8B%D0%B5_(%D1%80%D0%B5%D0%BA%D1%83%D1%80%D1%81%D0%B8%D0%B2%D0%BD%D1%8B%D0%B5)_%D1%8F%D0%B7%D1%8B%D0%BA%D0%B8 Разрешимые языки]
+
* [[Разрешимые (рекурсивные) языки | Разрешимые языки]]
* [http://neerc.ifmo.ru/wiki/index.php?title=M-%D1%81%D0%B2%D0%BE%D0%B4%D0%B8%D0%BC%D0%BE%D1%81%D1%82%D1%8C m-сводимость]
+
* [[m-сводимость]]
* [http://neerc.ifmo.ru/wiki/index.php?title=%D0%9F%D1%80%D0%B8%D0%BC%D0%B5%D1%80%D1%8B_%D0%BD%D0%B5%D1%80%D0%B0%D0%B7%D1%80%D0%B5%D1%88%D0%B8%D0%BC%D1%8B%D1%85_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87:_%D0%BF%D1%80%D0%BE%D0%B1%D0%BB%D0%B5%D0%BC%D0%B0_%D1%81%D0%BE%D0%BE%D1%82%D0%B2%D0%B5%D1%82%D1%81%D1%82%D0%B2%D0%B8%D0%B9_%D0%9F%D0%BE%D1%81%D1%82%D0%B0 Проблема соответствий Поста]
+
* [[Примеры неразрешимых задач: проблема соответствий Поста | Проблема соответствий Поста]]
  
 
== Источники информации ==
 
== Источники информации ==

Версия 17:40, 14 января 2016

Теорема:
Не существует алгоритма, определяющего по формуле исчисления предикатов первого порядка, является ли она общезначимой.
Доказательство:
[math]\triangleright[/math]

Обозначим язык всех общезначимых формул [math]L = \{w | w[/math] — общезначимая формула исчисления предикатов первого порядка[math]\}[/math]. Покажем, что универсальный язык [math]U[/math] m-сводится к [math]L[/math]. Для этого нужно построить вычислимую функцию [math]f[/math], которая принимает на вход пару из машины Тьюринга [math]M = \langle \Sigma, \Pi, B, Q, Y, N, S, \delta \rangle[/math] и слова [math]w[/math] и возвращает некоторую формулу исчисления предикатов, причём:

[math]f(\langle M, w \rangle) \in L \iff M[/math] попадает в допускающее состояние [math]Y[/math] на входе [math]w[/math].

Введём двухместный предикат [math]=[/math] со следующими аксиомами равенства (для удобства будем использовать инфиксную запись):

  • [math]\forall x (x = x)[/math] рефлексивность,
  • [math]\forall x \forall y (x = y \rightarrow y = x)[/math] симметричность,
  • [math]\forall x \forall y \forall z ((x = y \wedge y = z) \rightarrow x = z)[/math] транзитивность,
  • для каждой функции [math]f[/math] от [math]n[/math] аргументов [math]\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \wedge \ldots \wedge x_n = y_n) \rightarrow f(x_1, \ldots x_n) = f(y_1, \ldots y_n)[/math] — согласованность с функциональными символами,
  • для каждого предиката [math]p[/math] от [math]n[/math] аргументов [math]\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \wedge \ldots \wedge x_n = y_n) \rightarrow (p(x_1, \ldots x_n) \rightarrow p(y_1, \ldots y_n))[/math] — согласованность с предикатными символами.

Для каждого символа [math]s \in \Pi[/math] заведём константу [math]s[/math], для каждого состояния [math]q \in Q[/math] заведём константу [math]q[/math]. Чтобы специальным образом кодировать ленту, введём две двухместные функции: [math]|[/math] и [math]\cdot[/math], а также одноместную функцию [math]g[/math]. Конфигурацию [math]\langle c_0 c_1 \ldots c_{l - 1}, q, c_l \ldots c_m \rangle[/math] теперь можно представить следующей формулой (опять же будем использовать инфиксную запись для удобства):

[math]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[/math]

Заведём множество формул [math]A[/math]. Для каждого перехода, сдвигающего головку влево, [math]\delta(q, c_1) = \langle p, c_2, \leftarrow \rangle[/math] добавим в [math]A[/math] формулу [math]\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))[/math]. Для переходов, сдвигающих головку вправо или оставляющих на месте, аналогичным образом добавим соответствующие формулы в [math]A[/math].

Также введём предикат [math]yes[/math] и добавим в [math]A[/math] формулу [math]\forall x (yes(Y | x))[/math].

Наконец, чтобы предикат равенства был корректно задан, добавим все аксиомы равенства в [math]A[/math]. Поскольку число функций и предикатов конечно, множество [math]A[/math] будет конечно. Занумеруем его элементы как [math]A_0, A_1, \dots A_n[/math].

Теперь можно построить формулу [math]f(\langle M, w \rangle)[/math]:

[math](A_0 \wedge A_1 \wedge \ldots \wedge A_n) \rightarrow yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)[/math], где [math]x_0 x_1 \ldots x_k = w[/math].

Заметим, что по построению из [math]A_0 \wedge A_1 \wedge \ldots \wedge A_n[/math] следует равенство двух формул, кодирующих любые две конфигурации [math]C_1[/math] и [math]C_2[/math], такие что [math]C_1 \vdash^* C_2[/math]. Поскольку предикат равенства согласован с предикатными символами (в частности с [math]yes[/math]), то оценка [math]yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)[/math] совпадает с оценкой [math]yes(u)[/math], где [math]u[/math] — формула, кодирующая некую конфигурацию [math]C[/math], что [math]C_0 \vdash^* C[/math], где [math]C_0[/math] — начальная конфигурация, опять же при условии [math]A_0 \wedge A_1 \wedge \ldots \wedge A_n[/math].

Если [math]M[/math] допускает [math]w[/math], то [math]C_0 \vdash^* \langle u, Y, v \rangle[/math], поэтому оценка [math]yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)[/math] совпадает с оценкой [math]yes(Y|x)[/math] для какого-то [math]x[/math]. По построению из [math]A_0 \wedge A_1 \wedge \ldots \wedge A_n[/math] в частности следует, что [math]\forall x (yes(Y | x))[/math], а значит, в этом случае [math]f(\langle M, w \rangle)[/math] оказывается общезначима.

Если же [math]M[/math] не допускает [math]w[/math], то и доказательства для [math]f(\langle M, w \rangle)[/math] существовать не будет. Это вытекает из того факта, что во всём множестве [math]A[/math] присутствует лишь одна формула, содержащая предикат [math]yes[/math][math]\forall x (yes(Y | x))[/math]. Поэтому доказать следование [math]yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)[/math] можно лишь через эту формулу. Для подмены аргументов в предикатах существуют только аксиомы равенства, а [math](S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)[/math] не равна никакой другой формуле вида [math](Y | x)[/math], поэтому от [math]\forall x (yes(Y | x)[/math] не перейти к [math]yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)[/math], а значит, и доказательство [math]f(\langle M, w \rangle)[/math] построить не удастся. Поэтому эта формула не будет общезначимой.

Таким образом, [math]U \le_{m} L[/math], а значит, [math]L[/math] неразрешим, поскольку [math]U[/math] неразрешим.
[math]\triangleleft[/math]

См. также

Источники информации