(Чистое) исчисле́ние предика́тов (первого порядка) - это формальная теория , в которой определены следующие компоненты:
1. Алфавит:
связки | основные | |
дополнительные | ||
служебные символы | ( , ) | |
кванторы | всеобщности | |
существования | ||
предметные | константы | |
переменные | ||
предметные | предикаты | |
функторы |
С каждым предикатом и функтором связано некоторое натуральное число, которое называется арностью, или местностью.
2. Формулы имеют следующий синтаксис:
формула | ::= | атом формула |
атом | ::= | предикатсписок термов |
список термов | ::= | термтермсписок термов |
терм | ::= | константа переменная |
При этом необходимо учитывать слелующие контекстные условия: в терме функтор f должен быть n-местным. В атоме (или атомарной формуле) предикат P должен быть n-местным.
Вхождения переменных в атомарную формулу называются свободными. Свободные вхождения переменных в формулах A и B остаются свободными в формулах и . В формулах и формула A как правило имеет свободные вхождения переменной x. Вхождения переменной x в формулы и называются связанными. Вхождения других переменных (отличных от x), которые были свободными в формуле A, остаются свободными и в формулах и . Формула, не содержащая свободных вхождений переменных, называется замкнутой.
3. Аксиомы (логические): любая система аксиом исчисления высказываний, плюс
,
,
где терм t свободен для переменной x в формуле A.
4. Правила вывода:
Modus ponens, ,
где формула A содержит свободные вхождения переменной x, а формула B их не содержит.