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

Материал из Википедии — свободной энциклопедии

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

1. Алфавит:

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

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

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

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

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

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