(Чистое) исчисле́ние предика́тов (первого порядка) — это формальная теория K{displaystyle {mathcal {K}}}
, в которой определены следующие компоненты:1. Алфавит:
связки | основные | ¬,→{displaystyle neg ,to } |
дополнительные | ∨,∧{displaystyle lor ,land } | |
служебные символы | ( , ) | |
кванторы | всеобщности | ∀{displaystyle forall } |
существования | ∃{displaystyle exists } | |
предметные | константы | a,b,…,a1,b1,…{displaystyle a,b,…,a_{1},b_{1},…} |
переменные | x,y,…,x1,y1,…{displaystyle x,y,…,x_{1},y_{1},…} | |
предметные | предикаты | P,Q,…{displaystyle P,Q,…} |
функторы | f,g,…{displaystyle f,g,…} |
С каждым предикатом и функтором связано некоторое натуральное число, которое называется арностью, или местностью.
2. Формулы имеют следующий синтаксис:
⟨{displaystyle langle } | формула⟩{displaystyle rangle }::= | ⟨{displaystyle langle } ¬⟨{displaystyle neg langle } ∃⟨{displaystyle exists langle } переменная⟩⟨{displaystyle rangle langle }формула⟩{displaystyle rangle } |
атом⟩|{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 langle } переменная⟩|{displaystyle rangle |}⟨{displaystyle langle } функтор⟩(⟨{displaystyle rangle (langle } список термов⟩){displaystyle rangle )} |
константа⟩|{displaystyle rangle |}
При этом необходимо учитывать слелующие контекстные условия: в терме f(t1,…,tn){displaystyle f(t_{1},…,t_{n})}
функтор f должен быть n-местным. В атоме (или атомарной формуле) P(t1,…,tn){displaystyle P(t_{1},…,t_{n})} предикат P должен быть n-местным.Вхождения переменных в атомарную формулу называются свободными. Свободные вхождения переменных в формулах A и B остаются свободными в формулах ¬A{displaystyle neg A}
и A→B{displaystyle Ato B} . В формулах ∀xA{displaystyle forall xA} и ∃xA{displaystyle exists xA} формула A как правило имеет свободные вхождения переменной x. Вхождения переменной x в формулы ∀xA{displaystyle forall xA} и ∃xA{displaystyle exists xA} называются связанными. Вхождения других переменных (отличных от x), которые были свободными в формуле A, остаются свободными и в формулах ∀xA{displaystyle forall xA} и ∃xA{displaystyle exists xA} . Формула, не содержащая свободных вхождений переменных, называется замкнутой.3. Аксиомы (логические): любая система аксиом исчисления высказываний, плюс
P1:∀xA(x)→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)}
,где терм t свободен для переменной x в формуле A.
4. Правила вывода:
A,A→BB{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 ^{+}} ,где формула A содержит свободные вхождения переменной x, а формула B их не содержит.