Формализованное исчисление высказываний

части из совокупности всех тавтологий алгебры высказываний и разные

правила, по которому из одних формул можно получать новые.
В зависимости от выбора системы аксиом получаются различные аксиоматизации алгебры высказываний.
Общим для них является одно и то же множество теорем  это совокупность всех тавтологий алгебры высказываний.

алгебре
высказываний, подобный строгому построению геометрии
на

основе некоторой системы аксиом, например, системы
Евклида. Этот подход состоит в следующем:
Из всех ТИ- формул алгебры высказываний выделяется
некоторая часть. Формулы из этой части объявляются
аксиомами. Определяется некоторое правило, по которому
из одних формул можно получать новые. Правило
определяется так, чтобы по нему из аксиом могут быть
получены все тавтологии алгебры высказываний, то есть
тавтологии алгебры высказываний оказываются теоремами
аксиоматической теории исчисления высказываний

следующие:
A, B, X1, X2,  высказывательные (логические) переменные;

, →  логические связки;
( , )  скобки.
Первоначальным понятием является также понятие формулы,
которая определяется индуктивным образом:
1. Каждая высказывательная переменная является формулой.
2. Если F1 и F2  формулы, то выражения F1→ F2 также
являются формулами.
3. Других формул нет.

A3.

Правило вывода. Modus ponens ( MP правило заключения):
Здесь A и B  любые формулы.

Так как связки Ù, Ú не участвуют в аксиомах, их надо
определить: A Ù B означает
A Ú B означает

множества
формул T называется такая конечная

последовательность
B1, B2, …, Bs формул, каждая из которых является либо
аксиомой, либо формулой из T, либо получена из двух
предыдущих формул этой последовательности по правилу MP,
а последняя формула Bs совпадает с F (Bs  F).
Говорят в таком случае, что формула F выводима из T и
пишут: T | F. Элементы T называются гипотезами или
посылками вывода.
Если формула F выводима из системы аксиом, то пишут:
|F (говорят, что F есть теорема или F - доказуема).

→ A)); ( из A1 , если

G = A → A, F=A).

2. ((A→ ((A → A) → A))→ ((A→ (A → A ))→ (A→A)));
(из A2 , где F = H = A, G = A → A).

3. ((A→ (A → A ))→ (A→A))); (из 1 и 2 по правилу MP).

4. A→ (A → A ); ( из A1 , если G = F = A ).

A → A ; (из 3 и 4 по правилу MP).

и F формула.
1) Если T | F и T

 H, то H | F.
2) T | F  когда в T найдется такое конечное подмножество
H, что H | F.
3) Если T | F для любой формулы F из множества H, и
H | G, то T | G.
Доказательство. Свойство 1) выражает очевидный факт:
если формула F выводима из множества посылок T, то она
будет выводима и из всякого множества, получающегося
добавлением к T новых посылок.

A→C
1. (B→ C) → (A→ (B → C));

( из A1).
2. (B→ C); (посылка).
3. (A→ (B → C)); (из 1 и 2 по правилу MP).
4. (A→ (B → C)) → ((A→ B) → (A→ C)) ( из A2).
5. (A→ B) → (A→ C) (из 3 и 4 по правилу MP).
6. A→ B; (посылка).
7. A→ C; (из 5 и 6 по правилу MP).

В исчислении высказываний импликация сильно связана с
выводимостью.

справедливы следующие выводимости:
a) F →G, G →H |F

→ H;
b) F →(G →H), G | F → H.
Доказательство пункта a):
Из F →G, G →H, F |H. Это следует из вывода:
F →G, G →H, F, G, H ( по правилу MP).
По теореме дедукции получаем a).
Выводимость формулы F → H в b) аналогична.

→ B и обратно.
Пусть F1, F2,…, Fn 

вывод B из T, A, Fn B. Индукцией
по i (1 ≤ i≤ n ) покажем, что T | A → Fi.
Пусть i=1. Возможны 3 случая:
1. Пусть F1  аксиома. Тогда вывод: F1, F1→(A → F1), A → F1,
получаем |A → F1 .
2. Пусть F1T. Тогда вывод: F1, F1→(A → F1), A → F1 ,
получаем T|A → F1.
3. Пусть F1 A. Тогда используем теорему: | F1→ F1, поэтому
получаем |A → F1.
В любом случае T |A → F1 (Начало индукции доказано).

< n. Докажем это для Fn B.
Возможны 4 случая:

либо Fn  аксиома, либо Fn  T,
либо Fn  A , либо Fn получена по правилу MP из Fi и Fk, причем i, k < n и T | A →(Fi → Fn).
Для случаев 13 имеем T | A → Fn аналогично как при i=1.
Для случая 4 имеем: T | A → Fi и вывод T | A → (Fi → Fn).
Объединяя эти выводы и используя аксиому A2 и MP, можно
доказать T | A → Fn. Но Fn  B, то есть T | A → B.
Обратно:T | A → B. Дополним этот вывод гипотезой A. По правилу MP A, A → B |B, поэтому: T, A |B.

являются теоремами исчисления высказываний:
a)

б)

в) г)

д) е)

ж)

, получим:


2) Из формулы 1:

3) Из (1), (2) и Т2 (b):

4) Из A1:

5) Из (4), (3) и Т2 (a):

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

исчисление высказываний).

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

 некоторое множество формул):
введение импликации:

введение коньюнкции:

введение дизьюнкции:

введение отрицания:

Доказательство a): следует из теоремы дедукции.

 некоторое множество формул):
удаление импликации:

удаление коньюнкции

удаление дизьюнкции

удаление отрицания

Доказательство a): следует из правила MP.