Слабое косвенное доказательство

Здесь мы расширим исчисление положительной логики добавлением правилa [II.2]^min построения слабого косвенного доказательства.

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

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

строится согласно следующему предписанию. На любом шаге построения можно написать:

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

1а) формулу С ¢, полученную из С стиранием первого слева знака отрицания^[11], в качестве допущения слабого косвенного доказательства.

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

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

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

Слабое косвенное доказательство — это частный случай косвенного доказательства, характеризующийся следующими ограничительными условиями:

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

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

косвенного доказательства является наличие допущения слабого косвенного доказательства.

Так, в примере на с. 73 лишь (III) является слабым косвенным доказательством.

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

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

Рассмотрим некоторые теоремы и производные правила, которые можно установить в минимальной логике.

Т13. (А ® В) ® ((А ® ~ В) ® ~ А).

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

1) А ® В допущ.;

2) А ~ В допущ.;

3) А допущ. слаб. косв. док.;

4) В МП (3, 1);

5) ~ В МП (3, 2);

Пртврч.: 4, 5.

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

Т14. А ® ~~ А — обратный закон двойного отрицания.

Заметим, что (прямой) закон двойного отрицания— ~~ А ® А нельзя доказать ни в минимальной, ни в конструктивной логике (система конструктивной логики рассматривается в § 5 данной главы).

Т15. ~~~ А ® ~А.

Т16. ~ (А Ù ~ А) — закон противоречия.

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

1) А Ù ~ А допущ. слаб. косв. док.;

2) А УК (1);

3) ~ А УК (1);

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

Обращаем внимание на то, что это — косвенное доказательство нулькратной импликации и поэтому в него не вводится других допущений, кроме специального допущения косвенного доказательства.

Т17. (А ® В) ® (~ В ® ~ А).

Т18. (А ® ~ В) ® (В ® ~ А).

Относительно Т17, Т18 производно правило модус толленс, имеющее две схемы:

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

Т19. ~(А Ù В)® (А ® ~ В).

Т20. ~(А Ù В)® (В ® ~ А).

Относительно Т19, Т20 производно правило, имеющее две схемы. Его мы будем называть удалением отрицания конъюнкции:

Т21. ~ А ® ~(А Ù В).

Т22. ~ В ® ~(А Ù В).

Относительно Т21, Т22 производно правило, которое можно назвать введением отрицания конъюнкции:

Т23. (~ А Ú~ B) ® ~(А Ù В).

Т24. (А ® B) ® ((A ® C) ® ((~ B Ú ~ C) ® ~ А)).

Относительно Т24 производно правило простой деструктивной дилеммы

Дил₃ А ® B A ® C ~ B Ú ~ C.

~ А

Данное правило позволяет из двух импликаций с одинаковым антецедентом и из дизъюнкции отрицаний их консеквентов вывести отрицание антецедента этих импликаций.

Т25. (A ® C) ® ((B ® D) ® ((~ C Ú ~ D) ® (~ A Ú ~ B))).

Относительно Т25 производно правило сложной деструктивной дилеммы

Дил₄. A ® CB ® D ~ C Ú ~ D,

~ A Ú ~ B

которое означает, что из двух импликаций и дизъюнкции отрицаний их консеквентов следует дизъюнкция отрицаний их антецедентов.

Т26. ~ А ® (А ® ~ В).

Т27. ~ А ® (~ В ® ~(А Ú В)).

Относительно Т27 производно правило введения отрицания дизъюнкции

Т28. ~(А Ú В)® ~А.

Т29. ~(А Ú В)® ~В.

Т30. ~(А Ú В)® (~ А Ù ~В).

Относительно Т28, Т29 производно правило, которое можно назвать правилом удаления отрицания дизъюнкции:

Т31. ~~(А Ú В)—двойное отрицание закона исключенного третьего. Сам же закон исключенного третьего недоказуем в минимальной логике.

Т32. ~(А Ú В)«(~ А Ù ~В).

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

Часть 1. ~(А Ú В)® (~ А Ù ~В) р. д. ф., Т30.

Часть 2. (~ A Ù ~ B) ® ~ (A Ú B).

1) ~ A Ù ~ B допущ.;

2) ~ А УК (1);

3) ~ В

~ (А Ú В) ВОД (2, 3).

Т33. (А Ù ~В) ® ~(А ® В).

На этом мы заканчиваем обзор теорем и производных правил минимальной логики.

Упражнения.

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

I.1. ((N ® O) ® ((N Ù O) ® P) ® ~(N Ù P)) ® ~ N.

1) N ® O;

2) (N Ù O) ® P;

3) ~(N Ù P);

4) N;

5) O;

6) N Ù O;

7) P;

8) N Ù P.

I.2. ((F ® ~ G) ® (~ F ® (H ® ~ G)) ® ((~ I Ú ~ H) ® ~~ G) ® ~ I) ® ~ H.

1) F ® ~ G;

2) ~ F ® (H ® ~ G);

3) (~ I Ú ~ H) ® ~~ G;

4) ~ I;

5) H;

6) ~ I Ú ~ H;

7) ~~ G;

8) ~ F;

9) H ® ~ G;

10) ~ G;

11) ~ (~ I Ú ~ H).

I.3. (I ® J) ® (I Ú (~~ K Ù ~~ J)) ® (L ® ~ K) ® ~ (I Ù J) ® ~ (L Ù J).

1) I ® J;

2) I Ú (~~ K Ù ~~ J);

3) L ® ~ K;

4) ~(I Ù J);

5) L Ù J;

6) L;

7) J;

8) ~ K;

9) ~ I;

10) ~~ K Ù ~~ J;

11) ~~ K.

II. Докажите формулу, используя правило построения слабого косвенного доказательства:

1) (S ® T) ® (~ T Ù ~ U) ® ~ S;

2) ~ (K Ù L) ® (K ® L) ® ~ K;

3) ((K ® L) ® M) ® ((~ M Ù ~ (L ® K) ® ~ (K ® L);

4) ((W Ù X) ® (Y Ù Z)) ® ~ ((W Ù X) Ù (Y Ù Z)) ® ~ (W Ù X);

5) ((Q ® R) ® (R ® S) ® ~ S) ® (~ Q Ù ~ R);

6) ((T ® U) ® (V Ú ~ U) ® (~ V Ù ~ W)) ® ~ T;

7) (((~ M Ù ~ N) ® (O ® N)) ® (N ® M) ® ~ M)) ® ~ O.

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