5.6 Исчисление высказываний

2. Определяется множество F слов в алфавите A, F ½ S1 Ai

i=1

–формулы (правильно построенные выражения). Это множество задается конструктивно (как правило, индуктивным определением). Множества A и F определяют язык (сигнатуру) теории.

3. Из F выделяется подмножество формул – аксиомы теории.

4. Задаются правила вывода теории. Правило вывода R(F1; : : : ; Fn; G)

–это вычислимое отношение на множестве формул. Если

формулы F1; : : : ; Fn и G находятся в отношении R, то формула G называется непосредственно выводимой из F1; : : : ; Fn

по правилу R.

Часто правило R(F1; : : : ; Fn; G) записывают в виде F1; : : : ; FnR.

G

Формулы F1; : : : ; Fn называются посылками правила R, а

G – его следствием или заключением.

5. Выводом формулы G из формул F1; : : : ; Fn в теории T называется такая последовательность формул ©1; : : : ; ©n; ©n+1; : : : ; ©N , что ©N = G, а любая ©i,(i = 1 : : : ; N) есть либо аксиома, либо

одна из исходных формул F1; : : : ; Fn, либо непосредственно выводима из формул ©1; : : : ; ©i¡1 (или какого-то их подмножества) по одному из правил вывода.

Если существует вывод G из F1; : : : ; Fn, то говорят,что G выводима из F1; : : : ; Fn в теории T . Этот факт обозначают

F1; : : : ; Fn `T G

Если теория T фиксирована, то индекс опускается:

F1; : : : ; Fn ` G

Формулы F1; : : : ; Fn называются гипотезами или посылками вывода. Множество гипотез обозначается ¡ = fF1; : : : ; Fng. Переход в выводе от ©i¡1 к ©i называется i-м шагом вывода.

6. Доказательством формулы G в теории T называется вывод G из пустого множества формул, то есть вывод, в котором в качестве исходных формул используются только аксиомы

`T G

Формула G, для которой существует доказательство называется формулой, доказуемой в теории T , или теоремой теории

T .

Добавление формул к гипотезам не нарушает выводимости. Поэтому, если ` G, то F ` G, и если F1; : : : ; Fn ` G, то

и F1; : : : ; Fn; Fn+1 ` G при любых F и Fn+1. Порядок гипотез несуществен.

Замечания. При изучении формальных теорий рассматриваются два типа высказываний:

1.Высказывания самой теории (теоремы) – формальные объекты определенные ранее.

2.Высказывания о теории (о свойствах теорем, доказательств и т.д.), которые формулируются на языке, внешнем по отношению к теории – метаязыке и называемые метатеоремами.

Интерпретацией формальной теории T в область интерпретации называется функция I : f 7!M, которая каждой формуле формальной теории Т однозначно сопоставляет некоторое содержательное высказывание относительно объектов множества (алгебраической системы) . Это высказывание может быть истинным или ложным (или не иметь истинностного значения). Если соответствующее высказывание является истинным, то говорят, что формула выполняется в данной интерпретации.

Интерпретация I называется моделью множества формул ¡, если все формулы этого множества выполняются в интерпретации I. Интерпретация I называется моделью формальной теории , если все теоремы этой теории выполняются в интерпретации I (то есть все выводимые формулы оказываются истинными в данной интерпретации).

Формальная теория должна опираться на общие логические законы (общезначимые высказывания типа A _ :A или

8xP (x) ! P (y)).

Формальная теория называется полной, если для всякого высказывания A в этой теории

` A или ` :A:

Формальная теория называется непротиворечивой, если в ней не является доказуемой формула

A ^ :A:

Система аксиом непротиворечивой теории называется независимой, если никакая из аксиом не выводима из остальных по правилам вывода теории.

Формальная теория называется разрешимой, если существует алгоритм, который определяет доказуемость для любой формулы теории.

a; b; c; : : : ; p; q; r; : : : ; A; B; C; : : : ; F; G; H; : : : , знаков логических связок

:; ^; _; !; $, скобок, запятых и точек.

2. Формулы (синтаксические правила): a) атом есть формула;

b) если A; B – формулы, то

:A; (A ^ B); (A _ B); (A ! B); (A $ B)

формулы. Внешние скобки обычно опускают.

c) других формул нет (пропозициональными формулами являются лишь символы, построенные в соответствии с правилами a), b))

3.Аксиомы (общезначимые формулы).

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

1. Правило подстановки.

Если A(a) – выводимая формула, содержащая букву a, то выводима и формула A(B), полученная из A заменой всех вхождений a на произвольную формулу B.

2. Правило заключения

Логическим выводом формулы B из формул A1; : : : ; An называется такая последовательность формул

C1 : : : Ck; B;

что каждая формула Ci (i 6 k) является либо аксиомой, либо исходной формулой Aj (Ci = Aj); либо получена из предыдущих формул последовательности по правилам вывода.

Тот факт, что формула B выводима из формул A1; : : : ; An, выражают записью

A1; : : : ; An ` B: (?)

Здесь ` – оператор дедуктивной выводимости; формулы A1; : : : ; An называются гипотезами вывода и обозначаются

¡ = fA1; : : : ; Ang: Тогда (?) есть ¡ ` B:

Дедуктикой D называется конечный набор систем аксиом и правилам вывода. Рассмотрим некоторые из них.

Система аксиом 1.

Эта система аксиом использует только две связки: :; !; при этом сокращается алфавит исчисления.

Другие связки вводятся определениями (как сокращения некоторых формул), а не аксиомами: A _B заменяет :A ! B,

A ^ B – :(A ! :B), A $ B – (A ! B) ^ (B ! A). Аксиомы:

A1. A ! (B ! A);

A2. (A ! (B ! C)) ! ((A ! B) ! (A ! C));

A3. (:A ! :B) ! ((:A ! B) ! A).

Правило вывода одно – Modus Ponens (MP, правило отделения посылки)

A; A ! B

B

Пример 5.21. Показать, что формула a ! a выводима из аксиом.

` a ! a

Пример 5.22. Вывести a ` b ! a.

Из аксиомы 1 (A ! (B ! A)) по правилу МР

a; a ! (b ! a) b ! a

Всякую доказанную в исчислении выводимость вида ¡ ` A, где ¡ – множество формул (гипотез), можно рассматри-

вать как правило вывода A¡ , которое можно добавить к уже имеющимся.

Полученную выводимость A ` B ! A вместе с правилом

A

подстановки можно рассматривать как правило B ! A: если

формула A выводима, то выводима и формула B ! A, где B

– любая формула.

Пример 5.23. Доказать выводимость: a ! b; b ! c ` a ! a ! c.

ло силлогизма).

Система аксиом 2. (Клини, 1952)

1.A ! (B ! A);

2.(A ! B) ! ((A ! (B ! C)) ! (A ! C));

3.A ! (B ! (A ^ B)) — введение ^;

4:(A ^ B) ! A ¾— удаление ^; 5:(A ^ B) ! B

6:A ! (A _ B) ¾— введение _; 7:B ! (A _ B)

8.(A ! C) ! ((B ! C) ! ((A _ B) ! C)) — удаление _;

9.(A ! B)((A ! :B) ! :A) — введение :;

10.::A ! A — удаление :;

11.(A ! B) ! ((B ! A) ! (A $ B)) — введение $;

Эти системы аксиом равносильны в том смысле, что порождают одно и то же множество формул (эти системы аксиом выводятся друг из друга с учетом обозначения связок

^; _).

Пример 5.24. Доказать выводимость: a ! (b ! c); a ^ b ` c

1.a ! (b ! c) Посылка

Система аксиом 3 (Гильберт, Аккерман, 1938) Связки: :; _; (A ! B = :A _ B)

Аксиомы:

1.A _ A ! A;

2.A ! A _ B;

3.A _ B ! B _ A;

4.(B ! C) ! (A _ B ! A _ C).

Правило: A; A ! B (Modus Ponens)

B

Система аксиом 4 (Россер, 1953) Связки: :; ^; (A ! B = :(A ^ :B)): Аксиомы:

1.A ! A ^ A;

2.A ^ B ! A;

3.(A ! B) ! (:(B ^ C) ! :(C ^ A)):

Правило: Modus Ponens. Система аксиом 5 (Никод, 1917) Связка: j (AjB = :A _ :B): Аксиома:

(Aj(BjC))j((Dj(Dj(DjD))j ((EjB)j((AjE)j(AjE))))):

Правило:

A; Aj(BjC)

C

Система натурального вывода

1. A ! B; A ` B удаление импликации, Modus Ponens (правило отделения)

2.A ! B; :B ` :A Modus Tollens (правило отрицания)

3.A; B ` A ^ B введение конъюнкции

4.A ^ B ` A удаление конъюнкции

A ^ B ` A

5.A ` A _ B введение дизъюнкции

6.A _ B; :B ` A удаление дизъюнкции

7.::A ` A удаление отрицания

8.A ! B; B ! C ` A ! C транзитивность импликации (правило силлогизма, цепное правило)

9.A ! B; A ! :B ` :A сведение к абсурду (reductio ad absurdum)

10.A ! B ` :B ! :B правило контрпозиции

11.A _ B; :A ` B A _ B; :B ` A

:A _ B; A ` B

A _ :B; B ` A

A _ B _ C; :A ^ :B ` C

дизъюнктивные силлогизмы (разновидности Modus Tollendo Ponens)

12. A ! B; C ! B; A _ C ` B конструктивная дилемма A ! B; A ! C; :B _ :C ` :A деструктивная дилемма

Свойства отношения выводимости

Теорема 1. a) A1; : : : ; An ` Ai (i = 1; : : : ; n);

Доказательство. Последовательность формул A1; : : : ; An запишем в произвольном порядке, поместив последней формулу Ai:

b) Если

: : : : : : ,

A1; : : : ; An ` Bk, и

B1; : : : ; Bk ` C; то

A1; : : : ; An ` C

Доказательство. В выводе C из B1; : : : ; Bk подставим вместо Bi их выводы из A1; : : : ; An и получим вывод A1; : : : ; An ` C: