Используя понятие формального исчисления, определим исчисление высказываний (ИВ).
Алфавит ИВ состоит из
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 (сведение множества гипотез к одной гипотезе).