§ 3. Чисто прямое доказательство

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

Перейдем к рассмотрению теорем и производных правил положительной логики.

Т2. A₁  (A₂  ... (А_n  A_i)...), где i = l, 2, .... п.

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

A_i допущ.

Как видно, оно состоит из единственной формулы, которая входит в Т2 в качестве антецедента и потому согласно п. 1 правила [II. 1] вписывается в доказательство в качестве допущения. Но так как данная формула совпадает с формулой, входящей в Т2 также и в качестве консеквента, то полученная последовательность из одной формулы А_i, согласно [II. 1], является доказательством формулы Т2.

Частными случаями Т2 являются следующие теоремы:

Т3. А  (В А).

Т4. А  А.

По-видимому, невозможно придумать более тривиальную теорему, чем Т2 или ее частные случаи. Тем не менее, трудно представить без них строгое построение логической теории. Они, как мы увидим, играют весьма существенную роль в обосновании принципов логики.

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

Т5. (А  (В  С))  ((А  В)  (А  С)).

Т6. А  (В  (А  В)).

Т7. (А  В)  А.

Т8. (А  В)  В.

Т9. (А  С)  ((В  С)  ((А  В)  С)).

Т10. А  (А  В).

T11. В  (А  В).

Т12. (А  С)  ((В  D)  ((А  В)  (С  D))).

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

	А  С	допущ.;
	В  D	допущ.;
	А  В	допущ.;
	С (С  D)	р.д.ф., Т10;
	D  (С  D)	р.д. ф., Т11;
	А  (С  D)	Сил. (1, 4);
	В  (С  D)	Сил. (2, 5);
	С  D	УД (3, 6, 7).

Относительно Т12 производно правило

Дил2	А  В A  C B  D,
	C  D

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

Нахождение доказательств логических теорем существенно облегчается применением следующих двух производных правил построения доказательства. Первое из них называется: доказательство по частям (сокращенно: ДЧ), а второе— доказательство разбором случаев (сокращенно: PC).

Правило ДЧ формулируется так: для того чтобы доказать формулу вида

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

достаточно построить

1) доказательство формулы

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

(часть 1) и

2) доказательство формулы

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

(часть 2).

Данное правило легко обосновывается с помощью правила [II. 1] построения прямого доказательства и правил УК и МП. Действительно, если построены доказательства формул (**) и (***), то, делая последние строками нового доказательства согласно п. 3 правила [II. 1], введя в качестве допущений формулы A₁, A₂, ..., А_n согласно п. 1 этого же правила и пользуясь далее п. 3 правила [II. 1], мы с помощью МП' получаем формулы C₁, С₂, из которых в свою очередь по ВК выводим формулу

С₁  С₂

Получением данной формулы мы завершаем построение требуемого доказательства формулы (*).

Согласно ДЧ нахождение доказательства формулы вида

А  В

сводится к построению доказательств следующих двух импликаций (прямой):

А  В

и (обратной)

В  А,

так как А  В является по определению конъюнкцией этих импликаций, т. е.

(А  В)  (В  А).

Правило PC формулируется следующим образом: для того чтобы доказать формулу вида

A₁  (A₂  ... (А_k  ((B₁  B₂)  С))...), (*)

достаточно построить

1) доказательство формулы

A₁  (A₂  ... (А_k  (B₁  С))...), (**)

(случай 1) и

2) доказательство формулы

A₁  (A₂  ... (А_k  (B₂  С))...), (***)

(случай 2).

Очевидно, что обоснование правила PC должно состоять в указании способа построения доказательства формулы (*) при условии, что ранее построены доказательства формул (**), (***). В самом деле, используя правило [II. 1], мы пишем формулы (**), (***) в качестве ранее доказанных и A₁, A₂, ..., А_k в качестве допущений. Затем по МП' мы получаем формулы

B₁  C,

B₂  С,

и, введя в качестве еще одного допущения формулу

B₁  B₂,

по правилу УД пишем формулу

С.

Получением этой формулы завершается построение требуемого доказательства формулы (*).

Эвристическая ценность правил ДЧ, PC состоит в том, что они позволяют сводить задачу на поиск доказательства к более простым задачам. Правило ДЧ (соответственно PC) можно применять последовательно, разбивая вводимые в рассмотрение части (случаи) в свою очередь на подчасти (подслучаи) и т. д. Правила ДЧ и PC можно также применять совместно, комбинируя их друг с другом, как это иллюстрируется ниже.

Пример. Пользуясь правилами ДЧ и PC докажем следующую формулу:

(p  (q  r))  ((p  q)  (p  r)).

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