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

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

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