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

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

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

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

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

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

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

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

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

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

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

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

1) φ → (ψ → φ);

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

3) (φ ∧ ψ)→ φ;

4) (φ ∧ ψ)→ ψ;

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

6) φ → (φ ∨ ψ);

7) φ → (ψ ∨ φ);

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

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

10) φ → φ;.

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

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

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

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

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

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

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

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

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

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

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

Замечание 1. Если существует квазивывод в ИВ формулы φ из формул φ ₁, …, φ _m, то φ выводима в ИВ из формул φ ₁, …, φ _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 применили правило вывода).