logo
практикум по мат

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

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

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

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

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

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

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

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

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

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

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

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

1) φ→(ψ→φ);

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

  1. (φ∧ψ)→φ;

  2. (φ∧ψ)→ψ;

  3. (φ→ψ)→((φ→χ)→(φ→(ψ∧χ)));

  4. φ→(φ∨ψ);

  5. φ→(ψ∨φ);

  6. (φ→χ)→((ψ→x)→((φ∨ψ)→χ));

  7. (φ→ψ)→((φ→¬ψ)→¬φ);

  8. ¬¬φ→φ.

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

Единственным правилом вывода в ИВ является правило заключения (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 применили правило вывода);

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

  1. ¬φ→¬φ ­­­ (теорема ИВ по примеру 2);

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