170
правок
Изменения
Новая страница: «<div style="background-color: #ABCDEF; font-size: 16px; font-weight: bold; color: #000000; text-align: center; padding: 4px; border-style: solid; border-width: 1p...»
<div style="background-color: #ABCDEF; font-size: 16px; font-weight: bold; color: #000000; text-align: center; padding: 4px; border-style: solid; border-width: 1px;">Эта статья находится в разработке!</div>
<includeonly>[[Категория: В разработке]]</includeonly>
{{Теорема
|statement=
Не существует алгоритма, определяющего по формуле исчисления предикатов первого порядка, является ли она общезначимой.
|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>f(\langle M, w \rangle) \in L \iff M</tex> попадает в допускающее состояние <tex>Y</tex> на входе <tex>w</tex>.
Введём двухместный предикат <tex>=</tex> со следующими аксиомами равенства (для удобства будем писать <tex>x = y</tex> вместо <tex>=(x, y)</tex>):
* <tex>\forall x (x = 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>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>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>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>.
}}
<includeonly>[[Категория: В разработке]]</includeonly>
{{Теорема
|statement=
Не существует алгоритма, определяющего по формуле исчисления предикатов первого порядка, является ли она общезначимой.
|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>f(\langle M, w \rangle) \in L \iff M</tex> попадает в допускающее состояние <tex>Y</tex> на входе <tex>w</tex>.
Введём двухместный предикат <tex>=</tex> со следующими аксиомами равенства (для удобства будем писать <tex>x = y</tex> вместо <tex>=(x, y)</tex>):
* <tex>\forall x (x = 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>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>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>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>.
}}
