Примеры доказательств в формальном исчислении высказываний

1. А ® A

2. A Ù B ® B Ù A

3.

II. Формальное исчисление предикатов. Алфавитэтой теории – это алфавит исчисления предикатов. Онсостоит из пропозициональных переменных: a, b, c₉₉ , d₃₄₅ , … , объектных переменных: x, y, z₉₉ , t₃₄₅ , … , логических связок: , Ù , Ú , ® , « , предикатных символов: P⁽¹⁾( _ ), Q⁽¹⁾( _ ), … , P⁽²⁾( _ , _ ), Q⁽²⁾( _ , _ ), … , кванторов: " , $ и служебных символов: , и ( , ) .

Правила построения формул исчисления предикатовизвестны:

(Ф1): любая формула исчисления высказываний (от пропозициональных переменных) является формулой исчисления предикатов, в которой нет объектных переменных и кванторов. В этой формуле нет вхождений объектных переменных.

(Ф2): если P⁽ⁿ⁾( _ , … , _ ) – предикатный символ от n переменных и x₁ , … , x_n – объектные переменные, то P⁽ⁿ⁾( x₁ , … , x_n ) – формула исчисления предикатов, в которой все вхождения объектных переменных x₁ , … , x_n свободны, а вхождений других объектных переменных нет.

(Ф3): если A и В – две формулы, то (A Ù B), (A Ú B), (A ® B), (A « B), – тоже формулы, в которых свободны все вхождения объектных переменных, свободные в А или в В, и связаны все вхождения объектных переменных, связанные в А или в В.

(Ф4): если A(x) – формула хотя бы с одним свободным вхождением объектной переменнойx, то выражения (" x A(x)) и ($ x A(x)) – формулы, в которых связаны вхождения всех объектных переменных, связанных в А, а также все вхождения x, и свободны все вхождения объектных переменных, свободные в А, кроме переменной х. При этом формула A(x) называется областью действия квантора.

(Ф5): других формул нет.

Аксиомы формального исчисления предикатовполучаются добавлением ко всем аксиомам формального исчисления высказываний ещё одной группы схем аксиом с кванторами:

Группа аксиом с кванторами:

("): (" x А(x)) ® А(t) , ($): А(t) ® ( $ x А(x))

Здесь t – переменная, отличная от переменной x.

Таким образом, получается 13 схем аксиом, которые на самом деле представляют бесконечное количество аксиом.

Правила выводав формальном исчислении предикатов:

(MP): ,