Формальное исчисление высказываний

Подробно рассмотрим формальную теорию исчисления высказываний (ИВ). Нашей целью будет обоснование адекватности этой теории, описанной формально в § 1 главы III, неформальной алгебре высказываний, изученной в главе I. Под адекватностью формальной теории её неформальному аналогу понимается доказательство всех основных теорем неформальной теории в соответствующей формальной теории. В частности, будет доказано, что формула доказуема в формальной теории исчисления высказываний тогда и только тогда, когда она тождественно истинна.

1. Свойства выводимости формул.Докажем некоторые основные свойства выводимости формул.

1⁰. Всякая доказуемая формула выводима из любой совокупности формул. В частности, любая аксиома выводима из любой совокупности формул.

Действительно, доказательство формулы является и её выводом из любой совокупности формул, т.к. в нём используются аксиомы и правило вывода modus ponens. Последовательность из одной этой аксиомы является её доказательством.

2⁰. Из любой совокупности выводима любая формула этой совокупности.

В самом деле, если Г = {А₁ , … , А_i , … , А_n }, то последовательность из одной формулы А_i является выводом формулы А_i из совокупности Г.

3⁰. Доказуемая формула выводима из любой совокупности формул.

Действительно, доказательство этой формулы является её выводом из любой конечной совокупности формул.

4⁰. Если существует квазивывод формулы В из совокупности Г, т.е. конечная последовательность формул В₁ , … , В_k = B, каждая формула которой либо выводима из Г, либо получена из двух предыдущих по правилу modus ponens, то формула В выводима из Г.

Нужно просто заметить, что квазивывод расширится до вывода, если вместо каждой выводимой из Г формулы В_i вставить её вывод из совокупности Г.

5⁰. Если Г Ф, то для любой совокупности формул D верно Г, D Ф.

В самом деле, вывод формулы В₁ , … , В_k = B из совокупности Г является её выводом и из расширенной совокупности Г, D .

6⁰. Если Г Ф и Г (Ф ® Y), то Г Y .

Действительно, если В₁ , … , В_k = Ф – вывод формулы Ф, а С₁ , … , С_m = = (Ф ® Y ) – вывод формулы (Ф ® Y ), то В₁ , … , В_k = Ф, С₁ , … , С_m = = (Ф ® Y ), Y – вывод формулы Y, т.к. последняя формула этой цепочки получена из предыдущих Ф и (Ф ® Y) по правилу modus ponens.

Замечание: На самом деле в свойствах 5⁰ и 6⁰ обоснованы правила вывода – расширения посылок и – расширение modus ponens. Теперь ими можно пользоваться при выводе формул, сокращая длину доказательства. Дальнейший ход изложения лишь увеличит количество полезных правил вывода.

2. Теорема о дедукции:Обоснуем доказанные в главе I неформально правила дедукции: .

Теорема (о дедукции).Для формул А, В и произвольной конечной совокупности формул Г (возможно пустой) утверждение Г, А В имеет место тогда и только тогда, когда Г (А ® B).

Доказательство. Вначале докажем “лёгкую” импликацию (Ü). Если верно Г (А ® B), то (по правилу расширения посылок) Г, А (А ® B) и Г, А А (используется 2⁰). Применяя расширение modus ponens, получим Г, А В, что и требовалось.

(Þ) Рассмотрим вывод В₁ , … , В_k = В формулы В из совокупности Г, А . Если k = 1, то этот вывод состоит из одной формулы В и возможны случаи:

а: В – аксиома.Тогда цепочка (B ® (A ® B)), B, (A ® B) будет доказательством формулы (A ® B) и выводом её из совокупности Г. Последняя формула цепочки получена из предыдущих по правилу modus ponens.

б: В – формула совокупности Г, А. Если В = А , то (А ® B) = (A ® A) – доказуемая формула (см. пример доказательства в § 1), которая выводима из любого множества формул по свойству 1⁰. Если же В Î Г, то цепочка (B ® (A ® B)), B, (A ® B) является выводом формулы (A ® B) из Г.

Пусть теперь k > 1 и неверно, что Г (А ® B). Можно считать, что k – наименьшее натуральное число с этим свойством. Таким образом, для любых формул Ф, Y со свойством Г, Ф Y и длиной этого вывода меньше k будет верно Г (Ф ® Y).

В случаях, когда В – аксиома или формула совокупности Г, А применимы использованные ранее для k = 1 аргументы. Значит можно считать, что последняя формула В рассматриваемого вывода получена из двух предыдущих по правилу modus ponens. Итак, среди формул вывода В есть формулы В_i = C, B_j = (C ® B), где i < k, j < k, т.е. Г, А С и Г, А (C ® B) с длинами выводов, меньшими k. Учитывая предположение о минимальности k, получаем Г (А ® C) и Г (А ® (C ® B)). Теперь можно написать квазивывод формулы (А ® B) из множества формул Г :

1· ((A ® (C ® B)) ® ((A ® C) ® (A ® B))) (И2) (А := A, B := C, С := B)

2 ·(A ® (C ® B)) выводима из Г

3 ·((A ® C) ® (A ® B)) МР(1, 2)

4 ·(A ® C)выводима из Г

5 · (A ® B) МР(3, 4)

Теорема о дедукции доказана.

3. Производные правила вывода.Обоснуем некоторые знакомые правила логического вывода. Остальные правила докажите самостоятельно.

Правило перестановки посылок:. Запишем квазивывод формулы (В ® (A ® C)), предполагая, что (А ® (В ® C)) выводима.

1 · Г (А ® (В ® C))дано

2 · Г, А (В ® C) дедукция

3 · Г, А, В С дедукция

4 · Г, В (А ® C) дедукция

5 · Г (В ® (А ® C)) дедукция

Правила силлогизма: .

1 · Г В дано

2 · В С дано

3 · Г, В С расширение посылок

4 · Г (В ® С) дедукция

5 · Г СМР(1, 4)

1 · Г, А В дано

2 · Г (А ® B) дедукция

3 · Г, В С дано

4 · Г (В ® С) дедукция

5 · ((В ® C) ® (A ® (B ® C)))(И1)(A := (B ® C), B := A)

6 · Г (A ® (B ® C)) МР(4, 5)

7 · ((А ® (B ® C)) ® ((A ® B) ® (A ® C))) аксиома (И2)

8 · Г ((A ® B) ® (A ® C)) МР(6, 7)

9 · Г (A ® C) МР(2, 8)

10 · Г, А C дедукция

Правило объединения посылок:.

1 · Г (А ® (В ® С)) дано

2 · Г, А (В ® С) дедукция

3 · ((А ® A) ® ((A ® B) ® (A ® (A Ù B)))) (К3) (A := A =: B, C := B)