Cтраница 2
Таким образом, если две формулы исчисления предикатов ( не содержащие свободных индивидных переменных и формульных переменных без аргументов) равносильны в смысле опровер-жимости, то и соответствующие им системы аксиом в разрешенном виде будут равносильными в отношении непротиворечивости. [16]
Поэтому результат, что каждая доказуемая формула исчисления предикатов общезначима для любой непустой предметной области, не принадлежит метаматематике. Он относится скорее к тому, что можно назвать теоретико-множественной логикой предикатов ( Гильберт - Бернайс [ 1934, стр. [17]
Покажем, что если в формуле исчисления предикатов 91 заменить любую часть эквивалентной фор-мулой и если полученное вследствие этой замены выражение 91 также является формулой и содержит вес-свободные предметные переменные формулы 91, то 91 и 91 эквивалентны. [18]
Отношение эквивалентности может быть выражено формулами исчисления предикатов. [19]
Как и формулы исчисления высказываний, формулы исчисления предикатов делятся на три класса: общезначимые формулы, которые истинны при всех интерпретациях, невыполнимые, которые ложны при всех интерпретациях, и нейтральные ( или просто выполнимые), которые истинны только при некоторых интерпретациях. В противоположность тому, что имело место для исчисления высказываний, эти три класса не являются рекурсивными: не существует детерминированного алгоритма, который определял бы, к какому классу принадлежит произвольная формула исчисления предикатов. Вполне естественно, что формула исчисления предикатов выполнима, если она истинна хотя бы при одной интерпретации. [20]
Теперь мы рассмотрим все правила образования формул исчисления предикатов и докажем, что они переводят формулы, которым соответствуют выводимые формулы исчисления высказываний, в формулы, которым также соответствуют выводимые формулы исчио ления высказываний. [21]
Действительно, пусть ( Е - какая-либо формула исчисления предикатов. Тогда для формулы 1 S можно построить некоторую дедуктивно равную ей сколемовскую нормальную форму, причем эту форму можно выбрать так, чтобы она не содержала свободных индивидных переменных. [22]
Заметим также, что при изучении выполнимости формул исчисления предикатов формульные переменные без аргументов могут быть исключены. [23]
Мы видим, что наличие кванторов в формуле исчисления предикатов никак не сказывается на формуле, которая ей поставлена в соответствие. Формулам 93 ( я), / х й ( х) и 3 33 ( А:) ставится в соответствие одна и та же формула. Из этого закона соответствия следует, что формулы, которые мы ставим в соответствие формулам исчисления предикатов, являются формулами исчисления высказываний. Для элементарных формул исчисления предикатов это непосредственно ясно. Составляя из элементарных формул произвольную формулу исчисления предикатов, мы применяем операции 3 и 4, описанные в § 1 ( стр. [24]
Отсюда следует, что операция 2 также преобразует формулы исчисления предикатов в эквивалентные формулы. [25]
Наконец, аналогичным образом строятся и истолковываются и формулы многосортного исчисления предикатов 2 - й ступени. [26]
Теорема 1.12. Любое конечное или счетное выполнимое множество формул исчисления предикатов допускает конечную или счетную модель. [27]
Поэтому каждая нормальная форма, приспособленная для исследования опровержимости формул исчисления предикатов, дает нам некоторую нормальную форму, приспособленную для исследования непротиворечивости символьно разрешенных систем аксиом, так что для каждой символьно разрешенной системы аксиом можно указать такую систему аксиом специального вида, которая эквивалентна исходной в отношении непротиворечивости. [28]
В силу доказанной таким образом теоремы Левенгейма общее понятие выполнимости формул исчисления предикатов может быть заменено в математическом отношении весьма удобным понятием выполнимости в области натуральных чисел. [29]
Теоретико-доказательственным двойником этой теоремы является утверждение о том, что всякая формула исчисления предикатов в отношении выводимости равносильна некоторой бинарной формуле. Для доказательства этой теоремы можно, как это и сделал Эрбран, преобразовать с помощью критериев опровержимости доказательство теоремы Левенгейма в финитное доказательство соответствующей теоремы теории доказательств. [30]