Исчисление предикатов 1-го порядка как формальная система

1. Базовые элементы (алфавит) (Т):

· счетное множество предметных переменных Х: х1,х2,х3,…, xn,…;

· конечное (может быть и пустое) или счетное множество предметных констант А: а1,а2,а3,…,an,…;

· конечное (может быть и пустое) множество функциональных букв F: f11,f22,…,flk,…;

· непустое конечное или счетное множество предикатных букв Р: р11,р22,…,рlk…;

· символы исчисления высказываний: ,→,,↔;

· скобки () и запятые;

· символы , .

2. Синтаксические правила S (простые формулы или продукционные формулы).

a) всякий атом есть ППФ;

b) если А и В – ППФ и х - предметная переменная, то каждое из выражений А, А→В, А↔В, А В, А В, что ( x) A, ( x) A есть ППФ (правильно построенная формула или препозиционная формула).

Из элементов алфавита образуются элементы 3 типов:

· термы;

· атомы;

· формулы.

Правила образования терм:

· всякая предметная переменная является термом;

· всякая предметная константа является термом.

Правила образования атомов:

Если P – n -местный предикатный символ, t1,..,t2 - термы, то P (t1,..,t2) –атом (атомарная или простая формула).

Правила образования формул:

· атом есть формула;

· если А и В формулы то (А→В), (А↔В), (А В), (А В), что ( x)(A), ( x)(A) формулы, причем все переменные в этих формулах свободные;

· если А - формула, а x - свободная переменная в А, то ( x)(A) и ( x)(A)-формулы.

3. Аксиомы.

Аксиомы исчисления высказываний.

(A 1) (a a)→ a - закон сокращения;

(A 2) (a →(a b)) - закон расширения;

(A 3) ((a b) → (b a)) - закон коммутативности;

(A 4) ((a→b)→((c→a)→(c→b))) - закон транзитивности.

Добавляются еще 2:

(A 5) xA (x) → A (t), где А (х) есть ППФ и t –терм свободный для x в A (x).

(A 6) A (t)→ xA (x), где А (х) есть ППФ и t –терм свободный для x в A (x).

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

1) все аксиомы выводимы;

2) правило подстановки.

Это правило аналогично правилу подстановки, которое имеет место для исчисления высказываний. Только в данном случае мы будем иметь дело с такими подстановками термов t1,t2,…,tn вместо x1,x2,…,xk в A [ x1,x2,…,xk ]..

3) правило Modus Ponens;

4) правило обобщения (правила связывания квантором общности).

Если ППФ B→A (x) при условии, что B не содержит свободных вхождений х, выводима;

5) правило конкретизации (связывание квантором существования).

Если ППФ A (x)→ B выводится ППФ (теорема) и В не содержит свободных вхождений х, то xA (x)→ B также теорема;

6) если А - теорема, имеющая квантор и/или квантор , то одна связанная переменная в А может быть заменена другой связанной переменой, отличной от всех свободных переменных, одновременно во всех областях действия квантора, и в самом кванторе. Полученная ППФ также является теоремой.