Справка по формальной логике Fitch 6.26

6.26

1.A v (В ^ С)

2.~В v ~C v D

3.-А

4.-AVD (В интро 3)

-5. Б^С

--6. ~ Б

--7. B (союз, устран. 5)

--8. противоречие (противоречие интро 6 и 7)

--9. AVD (противоречие интро)

--10. ~ С

--11. C (конъюнктив. 5)

--12. противоречие (вступление 11 и 12)

--13. AVD (противоречие)

Вы делаете все остальное! Если вы можете получить AVD на втором уровне поддоказательства, вы можете вывести его на первый с помощью дизъюнкции elim. Как только вы это сделаете, остальное должно быть легко!

ОП хотел бы получить официальное доказательство следующего:

Посылка: А ∨ (В ∧ С)

Посылка: ¬B ∨ ¬C ∨ D

Цель: A ∨ D

Первое, что следует отметить, это то, что, хотя вторая посылка выглядит как символизация чего-то, это не действительное предложение. Это всего лишь выражение. Объем связки «∨» неоднозначен. Чтобы сделать это предложение, которое мы можем использовать формально, его нужно переписать как либо

(¬B ∨ ¬C) ∨ D

или как

¬B ∨ (¬C ∨ D)

Чтобы убедиться в этом, попробуйте ввести выражение ¬B ∨ ¬C ∨ D в программу проверки. Можно ли хотя бы начать? Вот что произошло, когда я попытался использовать естественную дедукцию и проверку доказательств , используемые forall x: Calgary Remix :

Основываясь на нашем человеческом понимании связки «∨» как «или», мы могли бы неофициально использовать выражение как оно есть и думать, что мы делаем падежи. Сначала мы рассмотрим случай «¬B», затем случай «¬C», а затем случай D и посмотрим, сможем ли мы достичь цели «A ∨ D» в каждом случае.

Однако, поскольку нам нужно формальное доказательство, мы не можем действовать таким образом. Нам нужно использовать предложения, а не произвольные выражения, какими бы очевидными они для нас ни были, и нам нужно использовать формальные правила для дизъюнкций (то есть «∨») для обоснования каждой строки формального доказательства. Средство проверки доказательств помогает нам убедиться, что мы используем предложения и следуем правилам.

Если мы выберем ~B v (~C v D) в качестве предложения, мы можем получить доказательство, подобное следующему.

Это доказательство показывает способ обработки случаев в обеих посылках путем формального исключения связки «V» с помощью поддоказательств.

Рассмотрим два случая в первой посылке. Я предполагаю, то есть начинаю дополнительное доказательство с «A» в качестве предположения в строке 3 и достигаю желаемой цели в строке 4, и я предполагаю «(B ∧ C)» в строке 5 и достигаю желаемой цели в строке 18. С обе части связки «V» достигают цели, я могу исключить «V» и завершить доказательство. Это исключение отменяет два сделанных мной предположения, представленных двумя поддоказательствами, по одному для каждого случая.

Второй случай выше требует больше строк. Рассмотрим эти детали. Чтобы достичь цели во втором случае, «(B ∧ C)», мне нужно было использовать вторую предпосылку. Я предположил случай «¬B», создав поддоказательство с «¬B» в качестве предположения в строке 7, и достиг цели в строке 9, а я предположил случай «¬C ∨ D» в строке 10 и пришел к заключению в строке. 17. Обратите внимание, что «¬C ∨ D» также является дизъюнкцией, предложением «∨», поэтому мне нужно использовать падежи, то есть поддоказательства, и в нем. Я сделал это в строках с 10 по 17.

Одним из требований в OP было:

Докажите это формально, не используя закон Де Моргана.

Обратите внимание, что я не использовал закон ДеМоргана в приведенном выше доказательстве. Чтобы увидеть, как можно было бы использовать закон ДеМоргана, рассмотрим следующее доказательство с использованием «(¬B ∨ ¬C) ∨ D».

Я это сделал, но доказательство чудовищно длинное. Если кто знает как упростить, буду признателен. Выполнено с редактором корректур Fitch из Стэнфорда :

Я это сделал, но доказательство чудовищно длинное. Если кто знает как упростить, буду признателен. Выполнено с редактором корректур Fitch из Стэнфорда:

Имплиментация Стэнфорда, как известно, раздувает доказательства, но вы довольно много бродили по кругу, вот @Houshalter

 1.|  A v (B & C)             Premise
 2.|_ (~B v ~C) v D           Premise
 3.|  |_ A                    Assumption
 4.|  |  A v D                Or Introduction 3
 5.|  A => A v D              Implication introduction 3,4
 6.|  |_ B & C                Assumption
 7.|  |  B                    And Elimination 6
 8.|  |  C                    And Elimination 6
 9.|  |  |_ ~(A v D)          Assumption
10.|  |  |  B                 Reiteration 7
11.|  |  ~(A v D) => B        Implication Introduction 9,10
12.|  |  |_ ~(A v D)          Assumption
13.|  |  |  C                 Reiteration 8
14.|  |  ~(A v D) => C        Implication Introduction 12,13
15.|  |  |_ ~B v ~C           Assumption
16.|  |  |  |_ ~B             Assumption
17.|  |  |  |  |_ ~(A v D)    Assumption
18.|  |  |  |  |  ~B          Reiteration 16
19.|  |  |  |  ~(A v D) => ~B Implication Introduction 17,18
20.|  |  |  |  ~~(A v D)      Negation Introduction 11,19
21.|  |  |  ~B => ~~(A v D)   Implication Introduction 16,20
22.|  |  |  |_ ~C             Assumption
23.|  |  |  |  |_ ~(A v D)    Assumption
24.|  |  |  |  |  ~C          Reiteration 22
25.|  |  |  |  ~(A v D) => ~C Implication Introduction 23,24
26.|  |  |  |  ~~(A v D)      Negation Introduction 17,28
27.|  |  |  ~C => ~~(A v D)   Implication Introduction 22,29
28.|  |  |  ~~(A v D)         Or Elimination 15,21,27
29.|  |  |  A v D             Negation Elimination 28
30.|  |  ~B v ~C => A v D     Implication Introduction 15,29
31.|  |  |_ D                 Assumption
32.|  |  |  A v D             Or Introduction 31
33.|  |  D => A v D           Implication Introduction 31,32
34.|  |  A v D                Or Elimination 2,30,33
35.|  B & C => A v D          Implication Introduction 6,34
36.|  A v D                   Or Elimination 1,5,36