Исчисление предикатов

(Чистое) исчисле́ние предика́тов (первого порядка) - это формальная теория , в которой определены следующие компоненты:

1. Алфавит:

связки основные
  дополнительные
служебные символы   ( , )
кванторы всеобщности
  существования
предметные константы
  переменные
предметные предикаты
  функторы

С каждым предикатом и функтором связано некоторое натуральное число, которое называется арностью, или местностью.

2. Формулы имеют следующий синтаксис:

формула ::= атом

формула
формулаформула
переменнаяформула

переменнаяформула
атом ::= предикатсписок термов
список термов ::= термтермсписок термов
терм ::= константа

переменная

функторсписок термов

При этом необходимо учитывать слелующие контекстные условия: в терме функтор f должен быть n-местным. В атоме (или атомарной формуле) предикат P должен быть n-местным.

Вхождения переменных в атомарную формулу называются свободными. Свободные вхождения переменных в формулах A и B остаются свободными в формулах и . В формулах и формула A как правило имеет свободные вхождения переменной x. Вхождения переменной x в формулы и называются связанными. Вхождения других переменных (отличных от x), которые были свободными в формуле A, остаются свободными и в формулах и . Формула, не содержащая свободных вхождений переменных, называется замкнутой.

3. Аксиомы (логические): любая система аксиом исчисления высказываний, плюс

,

,

где терм t свободен для переменной x в формуле A.

4. Правила вывода:

Modus ponens, ,

где формула A содержит свободные вхождения переменной x, а формула B их не содержит.