wiki

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

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

1. Алфавит:

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

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

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

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

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

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

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

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

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

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

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

A,A→BB{displaystyle {A,Ato B} over B} ${displaystyle {A,Ato B} over B}$ Modus ponens, B→A(x)B→∀xA(x) ∀+,A(x)→B∃xA(x)→B ∃+{displaystyle {frac {Bto A(x)}{Bto forall xA(x)}} forall ^{+},{frac {A(x)to B}{exists xA(x)to B}} exists ^{+}} ${displaystyle {frac {Bto A(x)}{Bto forall xA(x)}} forall ^{+},{frac {A(x)to B}{exists xA(x)to B}} exists ^{+}}$ ,

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