Cтраница 4
Теперь условимся, в пределах этой главы, что если мы употребляем слово формула, не указывая конкретного смысла, то это слово можно понимать и в смысле формулы исчисления высказываний, и в смысле формулы исчисления предикатов, которая будет определена в следующей главе, и в арифметическом смысле. [46]
Заметим, что в силу теоремы Бэта об определимости ( см., к примеру, [ Ю ]), если теория Т однозначно определяет сколемовские функции высказывания ( /, то эти функции определимы формулами исчисления предикатов первого порядка сигнатуры а на классе всех Т - алгебр. [47]
Неопровержимость такой формулы исчисления предикатов равносильна непротиворечивости той аксиомы ( соответственно той системы аксиом), которая изображается формулой, получающейся из рассматриваемой формулы в результате замены ее формульных переменных предикатными символами с тем же самым числом аргументов. Если рассматриваемая формула имеет вид конъюнкции предваренных формул, то после замены формульных переменных предикатными символами мы берем каждый ее конъюнктивный член в качестве отдельной аксиомы. [48]
Известно, что для исчисления предикатов первого порядка не существует общего метода установления общезначимости любых формул, т.е. исчисление предикатов первого порядка является неразрешимым. Однако если некоторая формула исчисления предикатов общезначима, то существует процедура для проверки ее общезначимости, т.е. исчисление предикатов можно назвать полу разрешимым. [49]
Для исчисления предикатов первого порядка не существует общего метода установления общезначимости льЗых формул, т.е. исчисление предикатов первого порядка является неразрешимым. Однако если некоторая формула исчисления предикатов общезначима, то существует процедура для проверки ее общезначимости, т.е. исчисление предикатов можно назвать полуразрешимым. Упомянутые выше метод резолюции [ Робинсон, 1965 ] и обратный метод [ Маслов, 1964 ] являются наиболее известными методами доказательства теорем. [50]