7.3. Выводы и доказательства

Посредством правил вывода строятся формальные рассуждения двух видов:

1. Выводы.

2. Доказательства.

Вывод — это не пустая и конечная последовательность формул, каждая из которых является либо посылкой, либо получена из предыдущих формул согласно одному из дедуктивных принципов так, что после применения правил _в и _в все формулы, начиная с последней посылки и вплоть до результата применения данного правила, не используются в дальнейших шагах построения вывода. Выпавшие из дальнейших шагов построения вывода формулы называются исключёнными (замороженными), соответственно исключёнными называются выражаемые такими формулами посылки.

Вывод может быть получен либо из пустого множества замороженных посылок (когда часть посылок оказываются не исключёнными в ходе рассуждения), либо из непустого множества замороженных посылок (когда все посылки оказываются исключёнными в ходе рассуждения). Так, различают собственно вывод — рассуждение, в ходе которого из каких-либо исходных суждений, посылок вывода получается заключение — суждение, логически вытекающее из посылок, и вывод-доказательство.

Доказательство есть вывод из непустого множества неисключенных посылок, при этом последняя формула вывода — это доказанная формула (теорема). Доказать какую-либо формулу, значит вывести её из формул посылок таким образом, чтобы, используя дедуктивные принципы _в или _в, перевести все эти формулы в разряд исключённых.

В целом структура любого вывода может быть представлена последовательностью формул, располагающихся, например, друг под другом. Каждая из формул этой последовательности в исчислении высказываний нумеруется натуральными числами.

• Пример

Если требуется вывести формулу p из посылок pp и p (записывается: pp, p - p, читается: «из посылок pp и p выводимо p», где « - » — знак выводимости), то следует найти и записать такую последовательность формул, в которой множество используемых посылок равно множеству формул pp и p, а последней оказывается именно выводимая формула p:

1. pp — пос.

2. p — пос.

3. p — _и, 1, 2.

Как видно из предложенной записи данной последовательности, напротив каждой формулы указывается основание, по которому она используется в выводе. Первым из двух возможных оснований вывода является то, что данная конкретная формула служит посылкой (соответствующее обозначение — «пос.»). Второе основание заключается в том, что данная конкретная формула получена из предыдущих формул по некоторому правилу вывода (что фиксируется символом применённого правила вывода и номерами формул, к которым оно было применено). Исключённые формулы вывода на каждом его шаге принято обозначать вертикальной чертой, расположенной слева от колонки пронумерованных формул.

В приведённом выше примере вывода нет исключённых формул, но если потребуется обосновать утверждение о выводимости - (p  p)  p, то есть обосновать утверждение о том, что формула ((p  p)  p) является теоремой (осуществить доказательство), мы получим следующую, уже имеющую исключённые формулы последовательность:

_______ ______________

1. p  p — пос. 2. p — пос. 3. p — и, 1, 2. 4. p — в, 2, 3. 5. (p  p)  p — и, 1.

• Пример

Обоснуем также и то, что теоремой является и другая формула закона введения отрицания: (pq)((pq)p). При этом получим схему вывода:

___________ ___________________ ___________________________

1. p  q — пос. 2. p  q — пос. 3. p — пос. 4. q — и, 1, 3. 5. q — и, 2, 3. 6. p — в, 4, 5. 7. (p  q)  p — в, 2, 6. 8. (p  q)  ((p  q)  p) — в, 1, 7.