§ 6. Сильное (классическое) косвенное доказательство

Сначала мы рассмотрим ситуацию, которая возникает, когда к описанной в предыдущем параграфе логической системе конструктивной логики добавляется еще одно правило следования, называемое правилом двойного отрицания. Оно представлено фигурой

ДО	А.
	А

Новую логическую систему, полученную добавлением ДО к списку I правил следования конструктивного исчисления высказываний из § 5 обозначим посредством N^cs. Мы говорили, что в системе N правило [II. 1] построения прямого доказательства избыточно.¹⁷ Но в системе N^cs аналогичное положение не имеет места, чем она выгодно отличается от равнообъемной, как увидим ниже, системы N.

Прежде чем приступить к установлению равнообъемности систем N^cs и N, покажем, что в системе N имеет место следующая теорема — закон двойного отрицания.

Т39. ~~А  А.

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

1. ~~А допущ.;

2. ~ А допущ. косв. док.;

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

Поэтому в системе N производно правило ДО системы N^cs.

Установление равнообъемности указанных систем N и N^cs сводится, очевидно, к доказательству следующих предложений.

Лемма 1. Любое доказательство в системе N^cs можно преобразовать в одноименное доказательство¹⁸ в системе N.

Лемма 2. Любое доказательство в системе N можно преобразовать в одноименное доказательство в системе N^cs.

Покажем сначала, что имеет место лемма 1. Рассмотрим произвольное доказательство D в системе N^cs. Предположим, что доказательства, непосредственно предшествующие D, уже преобразованы в одноименные доказательства в системе N.

Для D возможны два случая.

Случай 1. D не содержит применения правила ДО. В этом случае D и есть требуемое доказательство в системе N.

Случай 2. D содержит применение правила ДО. Так как ДО производно в N, то, устраняя его применения из D уже известным нам способом,¹⁹ мы получим требуемое доказательство в системе N.

Прежде чем приступить к установлению леммы 2, введем понятие сильного (классического) косвенного доказательства. Косвенное доказательство называется сильным, если при его построении непременно вписывается отрицание консеквента доказываемой кратной импликации.

Так, в примере на с. 74 (V) является единственным сильным косвенным доказательством.

Для большей ясности мы приводим

[II. 2]° Правило построения сильного косвенного доказательства.

Сильное косвенное доказательство формулы

A₁  (A₂  ... (А_n  С) ...) (*)

строится согласно следующему предписанию:

1. одну из формул A₁, A_{2, …,} А_n в качестве допущения;

la) формулу ~С в качестве допущения сильного косвенного доказательства;

2) формулу, следующую из ранее написанных формул, по одному из правил логического следования;

3) ранее доказанную формулу.

Сильное косвенное доказательство формулы (*) считается построенным, если в соответствии с пп. 1 —3, включая и п. 1а, получена последовательность формул, содержащая формулу ~С, пару противоречащих формул и оканчивающаяся одной из формул данной пары.

Таким образом, выявляется следующая классификация доказательств в системе N. Доказательства подразделяются на прямые и косвенные, а последние в свою очередь делятся на квазисильные и сильные.

Покажем теперь, что имеет место лемма 2. Пусть D — произвольное доказательство в системе N. В предположении, что все доказательства, непосредственно предшествующие D, уже преобразованы в одноименные доказательства в системе N^cs, рассмотрим следующие случаи:

Случай 1. D есть прямое доказательство. Данный случай тривиален, так как D совпадает с требуемым доказательством в системе N^cs.

Случай 2. D есть квазисильное косвенное доказательство. И этот случай тривиален по той же причине.

Случай 3. D есть сильное косвенное доказательство. В этом случае мы поступаем так. Очевидно, что ничто не препятствует считать доказательство D формулы (*) квазисильным доказательством формулы

A₁  (A₂  ... (А_n  С) ...) (**)

в системе N^cs.

Беря (**) в качестве ранее доказанной формулы, мы строим требуемое доказательство D' в системе N^cs формулы (*):

A₁  (A₂  ... (А_n  С) ...).

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

1)	A1	допущ.;
2)	A2	допущ.;
	…	допущ.;
	…	допущ.;
	…	допущ.;
п)	Аn	допущ.;
п+1)	A1 (A2 ... (Аn С) ...)	р.д.ф.;
n+2)	~~С	МП' (1, 2,... п; п+1);
	С	ДО (n+2).

Таким образом, на основании лемм 1 и 2 можно считать установленным следующее предложение.

Теорема 1. Системы N и N^cs равнообъемны (эквиваленты).

Из этой теоремы непосредственно следует, что правило [II.2]° построения сильного косвенного доказательства производно в системе N^cs.

Пример. Пользуясь методом, содержащимся в доказательстве леммы 2, перестроим доказательство (V) в системе N, приведенное в примере на с. 74 в одноименное доказательство в N^cs. Сначала надо преобразовать все предшествующие ему доказательства. Но (V) предшествует элементарное квазисильное доказательство (III), которое согласно случаю 2 совпадает с требуемым. Далее мы рассматриваем (V) как квазисильное доказательство в системе N^cs формулы

((р  q)  p)  ~~р.

Требуемое окончательное доказательство в системе N^cs приводится ниже:

((р  q)  p)  ~~р.

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

1. (p  q)  p допущ.;

2. ((p  q)  p)  ~~р р.д.ф.;

3. ~~р МП (1,2);

p ДО (3).

В качестве дальнейших логических теорем системы N (или, что то же, системы N^cs) мы предлагаем читателю в порядке упражнения установить следующие:

Т40. А  ~А закон исключенного третьего.

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

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

Т43. ~(А  В)  ((A  C)  ((~В  С)  С)).

Т44. ~(А  В)  (~А  ~В).

Т45. (А  В)  ~(А  ~В).

Т46. (А  В)  ((А  В)  В).

Т47. ( А  В)  (~А  В).

Т48. (А  В)  (~А  ~В).

Т49. (А  В)  ~(~ А  ~В).

Т50. (А  В)  (~А  В).

Т51. (А  В)  ~(~А  ~В).

Рассмотрев систему N, мы раскрыли ее иерархическую структуру, т. е. выявили в составе этой системы ряд подсистем, находящихся в отношении последовательного подчинения, или субординации.

Начав рассмотрение с системы положительной (позитивной) логики — будем обозначать ее посредством N^pos, — мы перешли, добавив к N^pos правило [II. 2]^min построения слабого косвенного доказательства, к системе минимальной логики, обозначив ее через N^min. Далее, заменив в N^min правило [II.2]^min более общим правилом [II. 2]^cn построения квазисильного косвенного доказательства, мы получили систему конструктивной логики, обозначив ее N^cn. Система N^cn в нашем рассмотрении уже непосредственно подчинена полной системе N.

Субординация рассмотренных систем представляет собой естественную логическую иерархию, которую можно рассматривать в качестве абстрактной модели развития форм логических умозаключений (рассуждений). Так, переход от N^pos к N^min является переходом от форм умозаключений, лежащих в основе прямых доказательств, к формам умозаключений, в которых, кроме прямых, осуществляются и так называемые слабые косвенные доказательства.

Дальнейшие переходы представляют нарастание «степеней косвенности» форм умозаключений.

В данной иерархии можно было бы выделить еще одну, в известном смысле, предельную логическую систему, именно ту подсистему системы N^pos, которая из правил [I] следования имеет лишь МП, а в качестве правила построения доказательства—правило [II.1] построения прямого доказательства. Системы, равнообъемные указанному фрагменту системы N^pos, называются исчислениями положительной (позитивной) импликации.

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

Упражнения:

I. Систему Слупецкого — Борковского для логики высказываний можно получить, заменив в системе N правило УД следующим:

А  В ~А,

В

а правило [II.2] — его частным случаем—правилом [II.2]°. Требуется доказать, что система N равнообъемна системе Слупецкого — Борковского.

II. Показать, что:

1) система, получаемая добавлением к N^min правила УО, равнообъемна системе N^cn;

2) система, получаемая добавлением к N^min правила ДО, равнообъемна системе N.

III. Показать, что:

1) система, получаемая добавлением к N^pos правил ВО, УО, равнообъемна системе N^cn;

2) система, получаемая добавлением к N^pos правил ВО, ДО равнообъемна системе N.

IV. Показать, что система, имеющая правила [I] логического следования и правило [II.2]° построения сильного косвенного доказательства, равнообъемна системе N.