6. Транзитивность выводимости
Следует отметить ещё одно свойство выводимости, которое тривиально обобщает лемму 2.1. и доказывается совершенно так же.
Лемма 2.3. (Транзитивность выводимости)
Пусть Р
и Q
– два множества формул,
,
.
Тогда
.
7. Теорема о дедукции для исчисления высказываний
Семантическое следование родственно импликации: импликация есть как раз булева функция, выражающая свойство одних высказываний «семантически следовать» из других. Неудивительно поэтому, что импликации родственна и выводимость – синтаксический аналог семантического следования.
Теорема 2.4. (Лемма о дедукции для исчисления высказываний)
Для любого множества формул Р и для любых формул q и r равносильны условия:
(1)
;
(2)
.
Замечание. Вместо
удобно писать P,
q.
В дальнейшем будет использоваться
именно такая запись.
Доказательство.
Импликация
(2)
(1)
тривиальна. Действительно, пусть
– вывод формулы
из набора посылок
Р. Тогда
– вывод формулы r
из набора посылок Р,
q:
формула
– одна из посылок, а формула
есть результат применения правила МР
к формулам
и
.
Доказательство
импликации (1)
(2)
несколько сложнее. Пусть
(*) – вывод формулы r
из набора посылок Р,
q.
Построим, исходя из него вывод формулы
из набора посылок Р.
Сделаем это в несколько шагов.
Шаг 1. Напишем
последовательность формул
(**).
Разумеется, эта последовательность
формул не является выводом. Для того
чтобы сделать её таковым, вставим в неё
ещё некоторые формулы.
Шаг 2. Возможно,
некоторые формулы
просто равны q.
Тогда формула
есть просто формула
,
которая является теоремой исчисления
высказываний. Вставим перед первой
такой формулой её доказательство.
Шаг 3. Возможно,
некоторые формулы
являются аксиомами исчисления высказываний
или посылками из Р.
Вставим перед каждой такой формулой
ещё две:
– посылка или
аксиома;
– аксиома (А1).
Тогда формула
становится
результатом применения к ним правила
МР.
Шаг 4. Возможно,
некоторые формулы
являются результатом применения правила
МР. Тогда существуют номера
,
такие, что
,
,
.
Соответственно, в последовательности
(**) есть формулы
,
,
которые можно использовать для вывода
формулы
.
Вставим перед последней формулой ещё
две формулы:
– аксиома (А2);
– результат
применения правила МР.
Теперь и формула становится результатом применения правила МР.
Заметим, что проведение этих шагов делает формулы последовательности (**) «всё более и более доказанными», а последний шаг просто превращает эту последовательность в вывод.
QED
Замечание.
Практическое
использование импликации (1)
(2)
обычно записывают в виде «дроби»
.
Существует ещё несколько «ходовых»
дробей такого вида, например:
,
,
.
Все они соответствуют утверждениям,
подобным лемме о дедукции (но более
простым) и доказываются с использованием
соответствующих аксиом (каких? как?)
совершенно аналогично доказательству
импликации (2)
(1).
8. Общая картина
Вывод является достаточно адекватным аналогом процесса мышления (и даже может быть основан на неверных посылках ). Теории, построенные на основе различных вариантов выводов, и, соответственно, состоящие из теорем, называются синтаксическими. Основной предмет изучения в математической логике – соотношение между синтаксисом и семантикой.