Построение исчисления высказываний в виде формальной системы. Понятие формальной системы. Построение исчисления высказываний

Формальная система представляет собой четверку:

P = <V, Ф, A, R>, где

V — алфавит.

Ф — множество правильно построенных формул.

А — аксиомы (при этом А in Ф).

R — правила вывода.

Рассмотрим исчисление высказываний как формальную систему, построенную в 3 шага.

Шаг 1. Определим язык исчисления высказываний. Для этого зададим символы и формулы. Символами исчисления высказываний являются.

1. Латинские буквы a, b,..., z, A, B..., Z и буквы с индексами, штрихами и т.п.

2. Символы ￢ и ∨.

Формулы определяются следующим образом.

1. Буквы является формулами.

2. Если U и V – формулы, то ￢U и ∨UV – формулы.

3. То, что выражение A является формулой, устанавливается несколькими применениями правил 1) и 2).

Это определение можно сформулировать иначе. Буквы считаем формулами шага 1. Назовем формулами шага n все формулы шага n − 1 и формулы ￢U и ∨UV, где U и V формулы шага n − 1. Пусть Fi —множество формул шага i и F = F 1 ∪F 2 ∪.... Выражение A является формулой тогда и только тогда, когда A ∈ F. Мы можем доказывать различные утверждения для формул индукцией по наименьшему шагу n, на котором получена формула.

Шаг 2. Зададим аксиомы исчисления высказываний.

Мы рассмотрим всего лишь один вид аксиомы – пропозициональные аксиомы. Они имеют вид ￢A ∨ A, где A – произвольная формула.

Шаг 3. Зададим 4 правила вывода исчисления высказываний. Они имеют следующий вид, где A, B, C – произвольные формулы.

В исчислении высказываний обычно вместо слова «теорема» употребляется слова «выводимая формула». То, что формула A является выводимой формулой, записывается в виде _ A.

Вместо привычной записи U∨V использовалась запись ∨UV. Хотя в дальнейшем мы применяем запись U ∨ V, но всегда подразумеваем вместо нее запись ∨UV. При определении формулы не использовались скобки. Оказывается, что мы сможем обойтись без употребления скобок. Для наглядности мы будем использовались скобки, например, записывать (A∨B). Однако под этой записью понимаем A ∨ B.

Запись F = A 1 ∨ A 2 ∨... ∨ An подразумевает правостороннюю расстановку скобок, а именно, сборку формулы F в виде F = A 1 ∨ (A 2 ∨... (An− 1 ∨ An)).

При определении формулы мы не использовали также знаки ∧, →, ↔.

Введем следующие определяемые символы →, ∧, ↔

• A → B является обозначением для ￢A ∨ B,

• A ∧ B является обозначением для ￢ (￢A∨ ￢B),

• A ↔ B является обозначением для (A → B) ∧ (B → A).