Используя понятие формального исчисления, определим исчисление высказываний (ИВ).
Алфавит ИВ состоит из букв x,y,z,u,v, возможно с индексами (которые называются пропозициональными переменными), логических символов (связок) ¬, ∧, ∨, →, а также вспомогательных символов (, ).
Множество формул ИВ определяется индуктивно:
а) все пропозициональные переменные являются формулами ИВ;
б) если φ, ψ ‑ формулы ИВ, то ¬φ, (φ∧ψ), (φ∨ψ), (φ → ψ) – формулы ИВ;
в) выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов "а" и "б".
Таким образом, любая формула ИВ строится из пропозициональных переменных с помощью связок ¬, ∧, ∨, →.
В дальнейшем при записи формул будем опускать некоторые скобки, используя те же соглашения, что и в предыдущей главе.
Подформулой ψ формулы φ ИВ называется подслово φ, являющееся формулой ИВ.
Под длиной формулы будем понимать число символов, входящих в слово φ.
Аксиомами ИВ являются следующие формулы для любых формул φ, ψ, χ ИВ:
1) φ→(ψ→φ);
2) (φ→ψ)→((φ→(ψ→χ))→(φ→χ));
3) (φ∧ψ)→φ;
4) (φ∧ψ)→ψ;
5) (φ→ψ)→((φ→χ)→(φ→(ψ∧χ)));
6) φ→(φ∨ψ);
7) φ→(ψ∨φ);
8) (φ→χ)→((ψ→x)→((φ∨ψ)→χ));
9) (φ→ψ)→((φ→¬ψ)→¬φ);
10) ¬¬φ→φ.
Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.
Единственным правилом вывода в ИВ является правило заключения (modus ponens): если φ и φ→ψ ‑ выводимые формулы, то ψ ‑ также выводимая формула. Символически это записывается так:
Говорят, что формула φ выводима в ИВ из формул φ1,…,φm (обозначается φ1,…,φm⊢φ), если существует последовательность формул ψ1,…,ψk,φ, в которой любая формула либо является аксиомой, либо принадлежит множеству формул {φ1,…,φm}, называемых гипотезами, либо получается из предыдущих по правилу вывода. Выводимость формулы φ из (⊢φ) равносильна тому, что φ ‑ теорема ИВ или доказуемая формула ИПΣ.
Пример 1. Покажем, что ⊢φ→φ.
Решение. Построим вывод данной формулы:
1) (φ→(φ→φ))→((φ→((φ→φ)→φ)→(φ→φ)) (схема аксиом 2);
2) φ→(φ→φ) (схема аксиом 1);
3) (φ→((φ→φ)→φ))→(φ→φ) (к пп. 2 и 1 применили правило вывода);
4) φ→((φ→φ)→φ) (схема аксиом 1);
5) φ→φ (к пп. 4 и 3 применили правило вывода).
Квазивыводом в ИВ формулы φ из формул φ1,…,φm называется последовательность формул ψ1,…,ψk,φ, в которой любая формула , либо принадлежит множеству формул {φ1,…,φm}, либо выводима из предыдущих.
Замечание 1. Если существует квазивывод в ИВ формулы φ из формул φ1,…,φm, то φ выводима в ИВ из формул φ1,…,φm.
Пример 2.Покажем, что φ,ψ⊢φ ψ.
Решение: Построим квазивывод формул φ ψ из φ и ψ:
1) φ (гипотеза);
2) ψ (гипотеза);
3) (φ→φ)→((φ→φ)→(φ→φ ψ)) (схема аксиом 5);
4) φ→φ (теорема ИВ по примеру 1);
5) ((φ→ψ)→(φ→φ ψ)) (к пп. 4 и 3 применили правило вывода);
6) ψ→(φ→ψ) (схема аксиом);
7) φ→ψ (к пп. 2 и 6 применили правило вывода);
8) φ→φ ψ (к пп. 7 и 5 применили правило вывода);
9) φ ψ (к пп. 1 и 8 применили правило вывода).
Пример 3. Покажем, что φ⊢¬¬φ.
Решение. Построим квазивывод формулы ¬¬φ из формулы φ:
1) φ (гипотеза);
2) (¬φ→φ)→((¬φ→¬φ)→¬¬φ) (схема аксиом 9);
3) φ→(¬φ→φ) (схема аксиом 1);
4) ¬φ→φ (к пп. 1 и 3 применили правило вывода);
5) (¬φ→¬φ)→¬¬φ (к пп. 4 и 2 применили правило вывода);
6) ¬φ→¬φ (теорема ИВ по примеру 2);
7) ¬¬φ (к пп. 6 и 4 применили правило вывода).