Исчисление предикатов. Выше были рассмотрены исчисления логики высказываний, в частности классическое исчисление

Выше были рассмотрены исчисления логики высказываний, в частности классическое исчисление. Любое логическое исчисление должно включать:

• Алфавит (совокупность используемых символов)
• Синтаксические правила построения формул
• Аксиомы (общезначимые формулы)
• Правила вывода производных формул по аксиомам.

Рассмотрим отличия исчисления предикатов первого порядка от исчислений высказываний. Аксиомы исчисления высказываний преобразуются в аксиомы исчисления предикатов путем замены α Þ α(х), то есть логическая переменная α заменяется предикатом α(х). Кроме того, вводятся две новые аксиомы:

" (х) α(х) ® α(у),

α (у) ® $ (х) α(х).

Множество правил вывода включает:

Правило Modus Ponens,

и правила введения кванторов

α ® b ├ α ® " (х) b(х),

α ® b ├ $ (х) α (х) ® b.

Существуют также и неклассические исчисления предикатов первого порядка. Они могут строиться на дополнении множества аксиом специфическими для данной предметной области общезначимыми формулами. Также могу использоваться следующие правила вывода:

Исключение квантора общности " (х) α(х) ├ α(х | А),

Исключение квантора существования $ (х) α (х) ├ α(х | А),

Введение квантора существования α (А) ├ $ (х) α(х | А).

Здесь α(х) – произвольная формула логики предикатов, имеющая связанную квантором переменную х, α(х | А) – формула α(х), в которой все вхождения переменной х заменены на константу А.