3. Правило вывода

Закончив обсуждение аксиоматики, перейдём к правилам вывода. В исчислении высказываний такое правило всего одно, оно называется modus ponens. Его обычно записывают в форме

(МР) .

Фактически оно является тернарным отношением на множестве формул, но эту формальность можно отдельно не обсуждать, поместив её «внутри» определений формального вывода и теоремы.

4. Доказательство. Теорема

Определение 2.2. (1) Последовательность формул называется доказательством, или, точнее – доказательством формулы , если формула есть либо аксиома, либо формула q, такая, что такие, что , (это и есть использование правила (МР)).

(2) Формула, имеющая доказательство, называется теоремой исчисления высказываний.

Пример. Покажем, что для любой формулы p формула является теоремой. Её доказательством может, например, служить следующая последовательность:

( ) (частный случай аксиомы (А1));

( ) (частный случай аксиомы (А2));

( ) (следует из , и правила (МР));

( ) (частный случай аксиомы (А1));

( ) (следует из , и правила (МР)).

Замечания. (1) В приведённом рассуждении р является формульной переменной. Соответственно, выше написаны гораздо более содержательные вещи, чем просто формулы и доказательство, именно: схемы формул и схема доказательства. Конкретное доказательство формулы для каждой данной формулы q получается, если подставить её вместо формульной переменной р в указанную схему.

(2) Теорема имеет совсем тривиальный вид. Тем не менее, её доказательство отнюдь не просто придумать! К сожалению, это – характерная для рассматриваемого предмета трудность (вдохновляющая на некоторую мыслительную деятельность ).

5. Вывод. Выводимость

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

Определение 2.3. (1) Пусть – некоторый набор формул. Элементы множества Р принято называть посылками. Последовательность формул называется выводом формулы из набора Р, если формула есть либо аксиома, либо посылка, либо формула q, такая, что такие, что , .

(2) В описанной ситуации говорят, что формула выводима из набора Р и пишут: .

(3) Формула d является теоремой тогда и только тогда, когда . Обычно символ принято опускать и писать более коротко: .

Лемма 2.1. Пусть – вывод формулы из набора посылок Р. Тогда если все элементы Р суть теоремы, то и формула также является теоремой.

Доказательство. Вывод тривиально превращается в доказательство: достаточно вместо посылки вставить доказательство теоремы .

QED

Замечание. Однако вполне возможно, что среди посылок встречаются формулы, не являющиеся ни теоремами, ни даже тавтологиями. Понятие вывода от этого не теряет своей осмысленности. У множества формул, которые можно получить как результат таких «незаконных доказательств», даже есть свой наглядный смысл: в него могут входить только те высказывания, которые получаются, если подставлять вместо пропозициональных переменных не «какие попало» наборы простых высказываний, а только такие, которые не делают ложной ни одну использованную посылку. Можно сказать, что вывод – это «условное» доказательство (в противовес доказательству обычному, «безусловному»), а его результат – «условная тавтология». Сделанное соображение крайне важно, и в дальнейшем будет сильно обобщено, поэтому полезно оформить его в виде определения.

Определение 2.4. Пусть Р – множество формул, q – формула. Если любой набор значений переменных, обращающий все формулы множества Р в истины, обращает в истину и q, то говорят, что q семантически следует из Р и пишут .

Использование этого определения позволяет уточнить замечание.

Теорема 2.2. (оправданность аксиоматизации)

.

Доказательство. Индукция по длине вывода, т.е. по количеству формул в выводе. Если длина вывода равна 1, то его единственная формула – либо аксиома (которая является тавтологией), либо посылка (которая тривиально истинна на любом наборе значений, на котором истинны все посылки). Поэтому в этом случае утверждение тривиально. Тем самым база доказана.

Пусть длина вывода равна n, сам вывод есть и для любого известно, что . Если – аксиома или посылка, всё снова так же, как в случае с базой. Осталось рассмотреть случай, когда есть результат применения правила МР. Значит, и . По индукционному предположению и . Соответственно, если на данном наборе аргументов все посылки истинны, то на нём истинны и формулы r и . Следовательно, на этом наборе аргументов истинна и формула q (так как при истинном значении r единственный способ сделать импликацию истинной – это сделать истинной формулу q).

QED