Система аксиом и правил вывода

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

Алфавит ИВ состоит из букв А,В,Q,R,Р и других, возможно с индексами (которые называются пропозициональными переменными), логических символов (связок), ∧, ∨, →, а также вспомогательных символов (,).

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

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

б)если φ, ψ‑ формулы ИВ, то φ, (φ∧ψ), (φ∨ψ), (φ → ψ) – формулы ИВ;

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

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

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

Подформулой ψ формулы φИВ называется подслово φ, являющееся формулой ИВ.

Под длиной формулы будем понимать число символов, входящих в слово φ.

Аксиомами ИВ являются следующие формулы для любыхформул φ, ψ, χ:

1) φ→(ψ→φ);

2) (φ→ψ)→((φ→(ψ→χ))→(φ→χ));

3) (φ∧ψ)→φ;

4) (φ∧ψ)→ψ;

5) (φ→ψ)→((φ→χ)→(φ→(ψ∧χ)));

6) φ→(φ∨ψ);

7) φ→(ψ∨φ);

8) (φ→χ)→((ψ→x)→((φ∨ψ)→χ));

9) (φ→ψ)→((φ→ψ)→φ);

10) φ→φ.

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

Единственным правилом вывода в ИВ является правило заключения (modusponens): если φ и φ→ψ ‑выводимые формулы, то ψ‑ также выводимая формула. Символически это записывается так:

φ, φ→ψ

ψ

Говорят, что формула φ выводима в ИВ из формул φ₁,…,φ_m (обозначается φ₁,…,φ_m├φ), если существует последовательность формул ψ₁,…,ψ_k,φ,в которой любая формула либо является аксиомой, либо принадлежит списку формул φ₁,…,φ_m,называемых гипотезами, либо получается из предыдущих по правилу вывода. Выводимость формулы φ из (├φ) равносильна тому, что φ‑ теорема ИВ.

Пример 1. Покажем, что ├φ→φ.

Решение. Построим вывод данной формулы:

1)в схеме аксиом 2 ψ заменим на φ→φ,χ на φ. Получаем аксиому (φ→(φ→φ))→((φ→((φ→φ)→φ)→(φ→φ));

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

3)из 1 и 2 по правилу вывода заключаем (φ→((φ→φ)→φ))→(φ→φ);

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

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

Пример 2. Покажем, что φ,ψ├φ ψ

Решение: Построим вывод формул φ ψ из φ и ψ

1) φ (гипотеза);

2) ψ (гипотеза);

3) (φ→φ)→((φ→φ)→(φ→φ ψ)) (схема аксиом);

4) φ→φ (используем формулу из примера 13);

5) ((φ→ψ)→(φ→φ ψ)) (применим правило вывода к пунктам 4,3);

6) ψ→(φ→ψ) (схема аксиом);

7) φ→ψ (применим правило вывода к пунктам 2,6);

8) φ→φ ψ (применим правило вывода к п.п. 7,5);

9) φ ψ (применим правило вывода к п.п. 1,8).

Квазивыводом в ИВ формулы φ из формул φ₁,…,φ_m называется последовательность формул ψ₁,…,ψ_k,φ, в которой любая формула выводима из предыдущих.

Замечание 1. Если существует квазивывод в ИВ формулы φ из формул φ₁,…,φ_m, то φ выводима в ИВ из формул φ₁,…,φ_m.

Пример 3. Покажем, что φ├φ.

Решение. Построим квазивывод формулы φ из формулы φ:

1) φ (гипотеза);

2) (φ→φ)→((φ→φ)→φ) (схема аксиом 9);

3) φ→(φ→φ) (схема аксиом 1);

4) φ→φ (к пп. 1 и 3 применили правило вывода);

5) (φ→φ)→φ (к пп. 4 и 2 применили правило вывода);

6) φ→φ­­­ (по примеру 2 выводимая формула);

7) φ (к пп. 6 и 4 применили правило вывода).