В логике предикатов вывод определяется так же, как и в исчислении высказываний и секвенции имеют тот же синтаксис. Аксиомы тоже определяются так же, как в логике высказываний. Все правила вывода логики высказываний – правила введения и удаления для пропозициональных связок, правила противоречия и сведения к противоречию – включены в множество правил вывода логики предикатов, с метапеременными для формул понимаемыми теперь как предикатные формулы. В дополнение, есть четыре новых правил вывода: правила введения и удаления для кванторов.
Правила для кванторов всеобщности
|
|
||||||||||||||||
|
где v не является свободной |
где t является |
||||||||||||||||
|
переменной для любой формулы в G |
подстановочным для v в F(v) |
||||||||||||||||
Корректность и полнота логики предикатов
Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.
Теорема корректности. Если существует вывод замкнутой формулы F из множества формул G, тогда G влечёт F.
Теорема полноты. Для любой замкнутой формулы F и любого множества предложений G, если G влечёт F, то существует вывод F из некоторого подмножества G.
Полнота логики предикатов для случая счётного G и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.
Функциональные символы и равенство: синтаксис
Наше наиболее общее понятие сигнатуры определяется следующим образом.
(Сигнатура, константы). Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.
(Терм). Возьмём сигнатуру s, не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если
каждая объектная константа принадлежит X,
каждая объектная переменная принадлежит X,
для каждой функциональной константы h арности n (n > 0) и любой строки t1, … , tn, если t1, … , tn принадлежит X, тогда также принадлежит h(t1, … , tn).
Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения.*
В логике первого порядка существуют три типа атомарных формул:
пропозициональные константы,
строки вида R(t1, … , tn) где R – предикатная константа арности n (n > 0) и t1, …, tn – термы,
строки вида (t1 = t2), где t1, t2 – термы.
Взяв в качестве множества атомарных формул данное множество, мы получаем, что определение формул (первого порядка) совпадает с определением предикатных формул в начале этой части.
Для любых термов t1 и t2, t1 № t2 обозначает формулу ¬(t1 = t2).