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

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

1. Алфавит:

связки	основные	${\displaystyle \neg ,\to }$
	дополнительные	${\displaystyle \lor ,\land }$
служебные символы		( , )
кванторы	всеобщности	${\displaystyle \forall }$
	существования	${\displaystyle \exists }$
предметные	константы	${\displaystyle a,b,...,a_{1},b_{1},...}$
	переменные	${\displaystyle x,y,...,x_{1},y_{1},...}$
предметные	предикаты	${\displaystyle P,Q,...}$
	функторы	${\displaystyle f,g,...}$

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

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

${\displaystyle \langle }$формула${\displaystyle \rangle }$	::=	${\displaystyle \langle }$атом${\displaystyle \rangle |}$ ${\displaystyle \neg \langle }$формула${\displaystyle \rangle |}$ ${\displaystyle (\langle }$формула${\displaystyle \rangle \to \langle }$формула${\displaystyle \rangle )|}$ ${\displaystyle \forall \langle }$переменная${\displaystyle \rangle \langle }$формула${\displaystyle \rangle |}$ ${\displaystyle \exists \langle }$переменная${\displaystyle \rangle \langle }$формула${\displaystyle \rangle }$
${\displaystyle \langle }$атом${\displaystyle \rangle }$	::=	${\displaystyle \langle }$предикат${\displaystyle \rangle (\langle }$список термов${\displaystyle \rangle )}$
${\displaystyle \langle }$список термов${\displaystyle \rangle }$	::=	${\displaystyle \langle }$терм${\displaystyle \rangle |\langle }$терм${\displaystyle \rangle ,\langle }$список термов${\displaystyle \rangle }$
${\displaystyle \langle }$терм${\displaystyle \rangle }$	::=	${\displaystyle \langle }$константа${\displaystyle \rangle |}$ ${\displaystyle \langle }$переменная${\displaystyle \rangle |}$ ${\displaystyle \langle }$функтор${\displaystyle \rangle (\langle }$список термов${\displaystyle \rangle )}$

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

Вхождения переменных в атомарную формулу называются свободными. Свободные вхождения переменных в формулах A и B остаются свободными в формулах ${\displaystyle \neg A}$ и ${\displaystyle A\to B}$. В формулах ${\displaystyle \forall xA}$ и ${\displaystyle \exists xA}$ формула A как правило имеет свободные вхождения переменной x. Вхождения переменной x в формулы ${\displaystyle \forall xA}$ и ${\displaystyle \exists xA}$ называются связанными. Вхождения других переменных (отличных от x), которые были свободными в формуле A, остаются свободными и в формулах ${\displaystyle \forall xA}$ и ${\displaystyle \exists xA}$. Формула, не содержащая свободных вхождений переменных, называется замкнутой.

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

${\displaystyle P_{1}:\forall xA(x)\to A(t)}$,

${\displaystyle P_{2}:A(t)\to \exists xA(x)}$,

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

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

${\displaystyle {A,A\to B} \over B}$ Modus ponens, ${\displaystyle {\frac {B\to A(x)}{B\to \forall xA(x)}}\ \forall ^{+},{\frac {A(x)\to B}{\exists xA(x)\to B}}\ \exists ^{+}}$,

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