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

Теперь мы несколько уменьшим ограничения, которые были наложены на косвенное доказательство в правиле [II.2] ^min, а именно не будем требовать, чтобы специальное допущение слабого косвенного доказательства непременно входило в доказательство. Иными словами, формулировка нового правила [II.2]^{c n} , которым мы будем пользоваться в этом параграфе и которое мы назовем, за неимением более удачного выражения, правилом построения квазисильного доказательства, получается из формулировки правила [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 производно правило, которое можно назвать удалением дизъюнкции посредством отрицания. Оно имеет следующие четыре схемы:

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

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

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

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

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

Не нашли, что искали? Воспользуйтесь поиском: