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

Эта статья находится в разработке!

Теорема:

Не существует алгоритма, определяющего по формуле исчисления предикатов первого порядка, является ли она общезначимой.

Доказательство:

[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]x = y[/math] вместо [math]=(x, y)[/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 \& 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 \& \ldots \& 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 \& \ldots \& 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]\triangleleft[/math]