# Fitch Formal Logic Help 6.26

6.26

Premise: A v (B ^C)

Premise: ~B v ~C v D

Goal: A v D

Prove it formally without using DeMorgan's Law.

• Can you show us what you've done so far? – virmaior Mar 7 '16 at 2:31
• You should be able to use a state chart showing the possible states and show that ~B v ~C v D => B^C = D – Guill Mar 7 '16 at 19:31
• You need proof by cases, using A v ~A. – Mauro ALLEGRANZA Mar 8 '16 at 9:24
• I'm voting to close this question as off-topic because it seems to be a homework question with no own effort whatsoever shown. – Philip Klöcking Mar 22 '16 at 14:30
• – Mauro ALLEGRANZA Nov 16 '19 at 9:04

6.26

1.A v (B ^C)

2.~B v ~C v D

3.-A

4.-A V D (V intro 3)

-5. B^C

--6. ~B

--7. B (conjunction elim. 5)

--9. A V D (contradiction intro)

--10. ~C

--11. C (conjunction elim. 5)

--13. A V D (contradiction elim)

You do the rest! If you can get A V D on the second level of the subproof, you can bring it to the first by means of disjunction elim. Once you do that, the rest should be easy!

The OP would like a formal proof of the following:

Premise: A ∨ (B ∧ C)

Premise: ¬B ∨ ¬C ∨ D

Goal: A ∨ D

The first thing to note is that although it looks like the second premise is a symbolization of something, it is not a valid sentence. It is only an expression. The scope of the connectives, "∨", is ambiguous. To make this a sentence that we can use formally it needs to be rewritten as either

(¬B ∨ ¬C) ∨ D

or as

¬B ∨ (¬C ∨ D)

To see this try putting the expression ¬B ∨ ¬C ∨ D into a proof checker. Can one even get started? This is what happened when I tried using the natural deduction and proof checker used by forall x: Calgary Remix:

Based on our human understanding of the connective "∨" as "or" we could proceed informally to use the expression as it is and think that we are doing cases. First we would consider the case "¬B", then the case "¬C" and then the case D and see if we can get to the goal "A ∨ D" in each case.

However, since we want a formal proof, we can't proceed in that manner. We need to use sentences, not arbitrary expressions, no matter how obvious they are to us, and we need to use formal rules for disjunctions (that is, "∨") to justify each line of the formal proof. A proof checker helps us verify that we are using sentences and following the rules.

If we choose ~B v (~C v D) as the sentence, we can get a proof like the following.

This proof shows a way to handle the cases in both of the premises by formally eliminating the "V" connective through subproofs.

Consider the two cases in the first premise. I assume, that is, start a subproof with "A" as an assumption on line 3 and reach the desired goal on line 4 and I assume "(B ∧ C)" on line 5 and reach the desired goal on line 18. With both sides of the "V" connective reaching the goal, I can eliminate the "V" and complete the proof. This elimination discharges the two assumptions I made represented by the two subproofs, one for each case.

The second case above required more lines. Let's consider those details. To reach the goal for the second case, "(B ∧ C)", I needed to use the second premise. I assumed the "¬B" case by creating a subproof with "¬B" as an assumption on line 7 and reached the goal on line 9 and I assumed the "¬C ∨ D" case on line 10 and reached the conclusion on line 17. Note that "¬C ∨ D" is also a disjunction, a "∨" sentence, and so I need to use cases, that is, subproofs, on it as well. I did this on lines 10 through 17.

One of the requirements in the OP was:

Prove it formally without using DeMorgan's Law

Note that I did not use DeMorgan's Law in the proof above. To see how DeMorgan's Law might have been used consider the following proof using "(¬B ∨ ¬C) ∨ D".

I did it, but the proof is monstrously long. If anyone knows how to simplify it I would appreciate it. Done with Stanford's Fitch proof editor:

• He asked for a formal proof, and using only the rules of inference in Fitch. If you want an informal proof, you can easily shorten the parts of the proof that are tedious. The general strategy is to prove by contradiction and or elimination. – Houshalter Mar 8 '16 at 15:56
• 1) A v ~A --- assumed for 1st v-elim; 2) A -- assumed 3) A v D -- by v-intro 4) ~A -- assumed 5) A v (B ^C) -- 1st premise: 2nd v-elim; 6) A -- assumed 7) contradiction (4 and 6) 8) D -- by ~-elim 9) A v D -- by v-intro 10) B ^C -- assumed 11) B -- ^-elim 12) C -- ^-elim 13) ~B v (~C v D) -- 2nd premise: 3rd v-elim; 14) ~B -- assumed 15) contradiction (11 and 14) 16) D -- by ~-elim 17) A v D -- by v-intro; 18) ~C v D -- assumed: 4th v-elim; 19) ~C -- assumed 20) contradiction (12 and 19) 21) D -- by ~-elim 22) A v D -- by v-intro; 23) D -- assumed 24) A v D -- by v-intro. 1/2 – Mauro ALLEGRANZA Mar 8 '16 at 16:11

I did it, but the proof is monstrously long. If anyone knows how to simplify it I would appreciate it. Done with Stanford's Fitch proof editor:

Stanford's fitch implimentation notoriously bloats proofs, but you had wandered around in circles quite a bit, there @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
``````