Неразрешимость исчисления предикатов первого порядка — различия между версиями
AReunov (обсуждение | вклад) |
AReunov (обсуждение | вклад) |
||
| Строка 41: | Строка 41: | ||
* [http://en.wikipedia.org/wiki/First-order_logic Wikipedia {{---}} First-order logic] | * [http://en.wikipedia.org/wiki/First-order_logic Wikipedia {{---}} First-order logic] | ||
| + | [[Категория: Теория формальных языков]] | ||
[[Категория: Теория вычислимости]] | [[Категория: Теория вычислимости]] | ||
| + | [[Категория: Примеры неразрешимых задач]] | ||
Версия 17:42, 14 января 2016
| Теорема: |
Не существует алгоритма, определяющего по формуле исчисления предикатов первого порядка, является ли она общезначимой. |
| Доказательство: |
|
Обозначим язык всех общезначимых формул — общезначимая формула исчисления предикатов первого порядка. Покажем, что универсальный язык m-сводится к . Для этого нужно построить вычислимую функцию , которая принимает на вход пару из машины Тьюринга и слова и возвращает некоторую формулу исчисления предикатов, причём:
Введём двухместный предикат со следующими аксиомами равенства (для удобства будем использовать инфиксную запись):
Для каждого символа заведём константу , для каждого состояния заведём константу . Чтобы специальным образом кодировать ленту, введём две двухместные функции: и , а также одноместную функцию . Конфигурацию теперь можно представить следующей формулой (опять же будем использовать инфиксную запись для удобства): Заведём множество формул . Для каждого перехода, сдвигающего головку влево, добавим в формулу . Для переходов, сдвигающих головку вправо или оставляющих на месте, аналогичным образом добавим соответствующие формулы в . Также введём предикат и добавим в формулу . Наконец, чтобы предикат равенства был корректно задан, добавим все аксиомы равенства в . Поскольку число функций и предикатов конечно, множество будет конечно. Занумеруем его элементы как . Теперь можно построить формулу :
Заметим, что по построению из следует равенство двух формул, кодирующих любые две конфигурации и , такие что . Поскольку предикат равенства согласован с предикатными символами (в частности с ), то оценка совпадает с оценкой , где — формула, кодирующая некую конфигурацию , что , где — начальная конфигурация, опять же при условии . Если допускает , то , поэтому оценка совпадает с оценкой для какого-то . По построению из в частности следует, что , а значит, в этом случае оказывается общезначима. Если же не допускает , то и доказательства для существовать не будет. Это вытекает из того факта, что во всём множестве присутствует лишь одна формула, содержащая предикат — . Поэтому доказать следование можно лишь через эту формулу. Для подмены аргументов в предикатах существуют только аксиомы равенства, а не равна никакой другой формуле вида , поэтому от не перейти к , а значит, и доказательство построить не удастся. Поэтому эта формула не будет общезначимой. Таким образом, , а значит, неразрешим, поскольку неразрешим. |
