§ 5. Квазисильное косвенное доказательство

Теперь мы несколько уменьшим ограничения, которые были наложены на косвенное доказательство в правиле [II.2]^min, а именно не будем требовать, чтобы специальное допущение слабого косвенного доказательства непременно входило в доказательство. Иными словами, формулировка нового правила [II.2]^cn, которым мы будем пользоваться в этом параграфе и которое мы назовем, за неимением более удачного выражения, правилом построения квазисильного доказательства, получается из формулировки правила [II.2]^min заменой всюду прилагательного «слабый» прилагательным «квазисильный» и вычеркиванием из второй части правила [II.2]^min слов, выделенных там курсивом, т. е. «формулу С'».

В примере на с. 73 (III), (IV) являются квазисильными доказательствами, причем (III) есть в то же время и слабое косвенное доказательство.

Легко понять, что любое слабое косвенное доказательство является одновременно и квазисильным, но обратное, вообще говоря, неверно. Заметим также, что квазисильное косвенное доказательство есть частный случай косвенного доказательства, полученного в результате ограничения п. 1а правила [II. 2]. Это ограничение состоит в том, что при построении квазисильного косвенного доказательства запрещается вводить отрицание консеквента доказываемой кратной импликации.

Логическая система, имеющая в качестве основных правил: правило [I] логического следования, правило [II.1] построения прямого доказательства и правило [II.21^cn построения квазисильного косвенного доказательства, представляет собой одно из исчислений конструктивной логики.

Рассмотрим некоторые ее специфические теоремы и производные правила.

Т34. А  (~А  В).

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

1. А допущ.;

2. ~А допущ.;

Пртврч.: 1, 2.

Относительно Т34 производно правило, называемое правилом удаления отрицания:

УО	А ~А.
	В

На первый взгляд, данное правило кажется «парадоксальным». Это объясняется тем, что в обычных рассуждениях оно применяется или неявно (например, в составе более сложных правил), или на промежуточных стадиях рассуждения (в частности, при отбрасывании некоторых случаев, как невозможных, в тех доказательствах, которые строятся по схеме правила PC).

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

Т35. (A  B)  (~A  B).

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

Случай 1. А  (~А  В) р.д.ф., Т34.

Случай 2. В  (~А  В) р. д. ф., Т35.

Т36. (A  B)  (~B  A).

Т37. (~A  B)  (~A  B).

Т38. (A  ~B)  (B  A).

Относительно Т35, Т36, Т37 и Т38 производно правило, которое можно назвать удалением дизъюнкции посредством отрицания. Оно имеет следующие четыре схемы:

	A  B ~A,	A  B ~B,
	B	A
УД/О
	~A  B A,	A  ~B B.
	B	A

Это правило позволяет из дизъюнкции и формулы, противоречащей одному из ее членов, получить другой ее член. Правило УД/О известно в традиционной логике под названием «модус толлендо поненс».¹³

Часто логику высказываний, которая в нашем изложении представлена полной системой N, называют классической логикой высказываний. Несмотря на то, что существуют теоремы классической логики, не доказуемые в конструктивной (в частности, закон исключенного третьего A  ~ А, закон двойного отрицания ~~А  А), конструктивная логика связана с классической рядом интересных соотношений, свидетельствующих в пользу того, что в известном смысле конструктивная логика не беднее логическими средствами, чем классическая. Так, согласно результату В. И. Гливенко (1929), в конструктивной логике высказываний для любой теоремы классической логики высказываний можно доказать ее двойное отрицание; при этом все теоремы классической логики высказываний, начинающиеся знаком отрицания, доказуемы и в конструктивной логике высказываний.

Известно также, что любая теорема классического исчисления высказываний, содержащая из пропозициональных связок лишь , ~, доказуема в конструктивном исчислении высказываний. Этот результат был получен К. Геделем (1933). Существуют и другие интересные взаимоотношения между классической и конструктивной логикой, они детально исследованы Н. А. Шаниным.¹⁴

Конструктивная логика, как самостоятельная логическая система, имеет свою семантику. Ее возникновение связано с особым, конструктивным пониманием математических объектов, согласно которому математические объекты являются результатами процессов построения, и принятием такого способа мышления, который позволяет выявить специфические черты этих конструктивных объектов. Указанному требованию, в частности, не удовлетворяют классические (сильные) косвенные доказательства,¹⁵ так как с их помощью в математике доказываются так называемые чистые теоремы существования. В то же время, согласно конструктивному пониманию, существование объекта с данными свойствами считается доказанным, когда указывается способ потенциально осуществимого построения объекта с данными свойствами.¹⁶

Конструктивная логика своим развитием во многом обязана трудам таких советских ученых, как А. Н. Колмогоров, В. Г. Гливенко, А. А. Марков, Н. А. Шанин и др.