Аксиоматические теории. Определения и свойства исчисления высказываний

Исчисление высказываний – это пример аксиоматической теории. ИВ определяется следующим образом:

1. Алфавит ИВ – это высказывательные переменные, скобки: (,) и логические символы и . Любой набор символов алфавита ИВ (даже бессмысленный) – это выражение ИВ.

2. Имеется подмножество выражений, называемое формулами ИВ. Формулы ИВ: а) все высказывательные переменные – это формулы; б) если A и B формулы, то A и A B тоже формулы. Формулы ИВ – это подмножество формул логики высказываний, содержащих только логические символы и .

3. Выделено некоторое подмножество формул, называемое аксиомами ИВ. Каковы бы не были формулы A, B и C, следующие формулы являются аксиомами ИВ:

A1. A (B A);

A2. (A (B C)) ((A B) (A C));

A3. ( B A) (( B A) B).

Выражения A1 – A3 называются схемами аксиом, поскольку каждое из них порождает бесконечное множество аксиом ИВ. Например, формула X (Y X) есть аксиома, полученная по схеме A1, а формула ( A A) (( A A) A) – аксиома ИВ, полученная по схеме A3.

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

Формула T называется теоремой ИВ, если существует вывод, в которой эта формула является последней. Этот вывод называется выводом теоремы T ИВ: T. Слева от символа аксиомы ИВ, теоремы ИВ и то, что получено из них по правилу вывода ИВ, не записывается.

Правило вывода m.p.(modus ponens): если в выводе есть две формулы вида А В и А, то после них в выводе можно писать формулу В. Считается, что формула В получена по правилу m.p. из формул А и А В. Правило записывается так: или А, А В В. Порядок формул А и А В в выводе не важен (A может встретиться в выводе раньше А В, а может и позже), но формулу B нельзя писать раньше, чем А и А В появятся в выводе.

Все аксиомы ИВ – это тавтологии, что можно проверить по их таблице истинности. По правилу m.p. из тавтологий можно получить только тавтологии.

12. Теорема дедукции и два её следствия. Правило modus ponens.

Вывод теоремы A A сложен. Начинаем упрощать (укорачивать) вывод теорем ИВ и следствий из гипотез. Теорема: если Г A и B – любая формула, то Г B A. Доказательство: пусть A1, …, An = A - вывод формулы A из Г. Тогда A1, …, An, A (B A), B A – вывод формулы B A из Г. Здесь An = A, предпоследний шаг вывода получен по схеме аксиомы A1, а формула B A получена по правилу m.p. из двух предпоследних шагов вывода. Теорема доказана.

Теорема о дедукции: Пусть набор гипотез Г (может быть и пустой) и выделенная гипотеза A приводят к B: Г, A B. Тогда Г A B. Доказательство проведём индукцией по n – длине вывода формулы B из Г и A. Пусть B1, …, Bn – это вывод формулы B из Г и A. Делаем первый шаг индукции. При n = 1 B = B1. По определению вывода ИВ возможны три случая: B1 – это аксиома, или формула из множества гипотез Г, или B1 = A = B. Для аксиомы и формулы из Г имеем: Г B1. Согласно только что доказанной теоремы для каждой формулы A Г A B1, т.е. Г A B.

Для B = A формула A B имеет вид A A, что является теоремой ИВ ( A A). Отсюда Г A A. Первый шаг индукции по длине вывода n доказан. Сделаем индуктивное предположение, что если длина вывода формулы B из Г и A меньше n, то теорема о дедукции выполняется. Из этого докажем, что теорема верна и для длины вывода, равного n.

По определению вывода ИВ возможны четыре случая: Bn – это аксиома, или формула из множества гипотез Г, или Bn = A = B, или Bn получена по m.p. из предыдущих шагов вывода Bi и Bj, где i < n и j < n. В первых трёх случаях доказательство проводится как при n = 1. В четвёртом случае либо Bj = Bi Bn, либо Bi = Bj Bn. Ограничимся рассмотрением случая, когда Bj = Bi Bn.

Вывод формулы Bi – это первые i формул из вывода формулы Bn из Г и A. Вывод формулы Bj – это первые j формул из вывода формулы Bn из Г и A. Длины этих выводов меньше n, так как i < n и j < n. Отсюда для формул Bi и Bj работает индуктивное предположение:

(1) Г A Bi;

(2) Г A Bj (Г A (Bi Bj));

по схеме аксиом A2 имеем:

(3) Г (A (Bi Bj)) ((A Bi) (A Bn)), где вместо B подставлена Bi, а вместо C – Bn;

применяя шестое свойство выводимости из гипотез к (2) и (3), получаем:

(4) Г (A Bi) (A Bn);

применяя шестое свойство выводимости из гипотез к (1) и (4), получаем:

(5) Г (A Bn). Теорема о дедукции доказана.