Неразрешимость исчисления предикатов первого порядка — различия между версиями
AReunov (обсуждение | вклад) м (→Ссылки) |
AReunov (обсуждение | вклад) |
||
Строка 29: | Строка 29: | ||
Таким образом, <tex>U \le_{m} L</tex>, а значит, <tex>L</tex> неразрешим, поскольку <tex>U</tex> неразрешим. | Таким образом, <tex>U \le_{m} L</tex>, а значит, <tex>L</tex> неразрешим, поскольку <tex>U</tex> неразрешим. | ||
}} | }} | ||
+ | |||
+ | == См. также == | ||
+ | * [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 Разрешимые языки] | ||
== Источники информации == | == Источники информации == |
Версия 02:08, 14 января 2016
Теорема: |
Не существует алгоритма, определяющего по формуле исчисления предикатов первого порядка, является ли она общезначимой. |
Доказательство: |
Обозначим язык всех общезначимых формул универсальный язык m-сводится к . Для этого нужно построить вычислимую функцию , которая принимает на вход пару из машины Тьюринга и слова и возвращает некоторую формулу исчисления предикатов, причём: — общезначимая формула исчисления предикатов первого порядка . Покажем, что
Введём двухместный предикат со следующими аксиомами равенства (для удобства будем использовать инфиксную запись):
Для каждого символа Конфигурацию теперь можно представить следующей формулой (опять же будем использовать инфиксную запись для удобства): заведём константу , для каждого состояния заведём константу . Чтобы специальным образом кодировать ленту, введём две двухместные функции: и , а также одноместную функцию .Заведём множество формул . Для каждого перехода, сдвигающего головку влево, добавим в формулу . Для переходов, сдвигающих головку вправо или оставляющих на месте, аналогичным образом добавим соответствующие формулы в .Также введём предикат и добавим в формулу .Наконец, чтобы предикат равенства был корректно задан, добавим все аксиомы равенства в . Поскольку число функций и предикатов конечно, множество будет конечно. Занумеруем его элементы как .Теперь можно построить формулу :
Заметим, что по построению из следует равенство двух формул, кодирующих любые две конфигурации и , такие что . Поскольку предикат равенства согласован с предикатными символами (в частности с ), то оценка совпадает с оценкой , где — формула, кодирующая некую конфигурацию , что , где — начальная конфигурация, опять же при условии .Если допускает , то , поэтому оценка совпадает с оценкой для какого-то . По построению из в частности следует, что , а значит, в этом случае оказывается общезначима.Если же Таким образом, не допускает , то и доказательства для существовать не будет. Это вытекает из того факта, что во всём множестве присутствует лишь одна формула, содержащая предикат — . Поэтому доказать следование можно лишь через эту формулу. Для подмены аргументов в предикатах существуют только аксиомы равенства, а не равна никакой другой формуле вида , поэтому от не перейти к , а значит, и доказательство построить не удастся. Поэтому эта формула не будет общезначимой. , а значит, неразрешим, поскольку неразрешим. |