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

Используя понятие формального исчисления, определим исчисление высказываний (ИВ).

Алфавит ИВ состоит из

1. букв А, В, Q, R, Р и других, возможно с индексами (которые называются пропозициональными переменными},

2. логических символов (связок) ¬, &, v, →,

3. вспомогательных символов (,).

Множество формул ИВ определяется индуктивно:

1. все пропозициональные переменные являются формулами ИВ;

2. если A, B — формулы ИВ, то ¬A, AΛB, AvB, A→B — формулы ИВ;

3. выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов "1" и "2".

Таким образом, любая формула ИВ строится из пропозициональных переменных с помощью связок ¬, Λ, v, →, ~.

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

Аксиомами ИВ являются следующие формулы (для любых формул A,B,C)

1. A→(B→A);

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

3. (AΛB)→A;

4. (AΛB)→B;

5. (A→B)→((A→C)→(A→(BΛC)));

6. A→(AvB);

7. A→(BvA);

8. (A→C)→((B→C)→((AvB)→C));

9. (A→B)→((A→¬B)→¬A);

10. ¬¬A→A.

Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.

Правилом вывода в ИВ является правило заключения {modus ponens): если A и A→B — выводимые формулы, то B — также выводимая формула.

Например, если высказывания АΛВ и АΛВ→(А→С) выводимы, то высказывание А→С также выводимо согласно правилу заключения.

Говорят, что формула G выводима из формул F1,F2,…,Fn (обозначается F1,F2,…,Fn ├G), если существует последовательность формул F1,F2,…,Fk,G, в которой любая формула является либо аксиомой, либо принадлежит списку формул F1,F2,…,Fn (называемых гипотезами), либо получается из предыдущих формул по правилу вывода. Выводимость формулы G из ∅ (обозначается ├G) равносильно тому, что G — теорема ИВ.

Пример. Покажем, что формула A→A выводима в ИВ. Для этого построим вывод данной формулы:

1) в аксиоме 2 заменим B на A→A, C — на A. Получаем аксиому (A→(A→A)) →((A→((A→A)→A)) →(A→A));

2) в аксиоме 1 заменим B на A. Получаем A→(A→A);

3) из 1 и 2 по modus ponens заключаем (A→((A→A)→A))→(A→A);

4) в аксиоме 1 заменяем B на A→A. Получаем A→((A→A)→A);

5) из пп. 3 и 4 по правилу вывода справедливо ├ A→A.

Теорема.

1. Если F1,F2,…,Fn,A,B — формулы ИВ, Г={F1,F2,…,Fn}, Г├A, то Г,B├A. (можно увеличивать число гипотез).

2. Тогда и только тогда F1,F2,…,Fn├A, когда F1ΛF2Λ...ΛFn├A (сведение множества гипотез к одной гипотезе).