What are the rules for discharging a premise in a Zero-Premise Deduction?

Question

If I have the problem (A → B) v (B → C), is there a way to prove this from no premises without first using Material Implication to convert the statement into ¬(A → B) → (B → C)?

Answer 1

On the surface, this seems like an odd candidate to be a tautology, given that A, B or C could be anything. But once we remember that every truth is implied by any antecedent, and that a false antecedent implies anything, we can see our way clear to proof.

In outline, B or not B can always be derived from no premises in any system with binary truth values (everything being either true or false). In the case B is true, it is implied by everything, including A, no matter what A is. In the case B is false, it implies everything, including C, no matter what C is.

To line it out, step by step:

Start by assuming both B And Not B. This leads to an immediate contradiction so we can derive Not (B And Not B) which simplifies to B Or Not B.

In the case that B, assume A and derive B to yield A implies B. Now that we have A implies B we can immediately yield (A implies B) Or (B implies C) on this half of the disjunction.

On the side of Not B, assume B. If you then assume Not C, you can derive B and Not B to show Not Not C, and therefore that C. Thus, B implies C which takes us to (A implies B) Or (B implies C) on this side of the disjunction as well.

There are, of course, many other equally valid ways to reach the desired result, but this one has the advantage of making it easier to understand why this is a tautology.

Answer 2

You can prove it indirectly as follows (if steps (5) and (8) are acceptable to you, of course).

1 Suppose, for contradiction that: ¬((A → B) ∨ (B → C))

2 Push the negation in with De Morgan: ¬(A → B) ∧ ¬(B → C)

3 ¬(A → B) by conjunction-elimination from (2)

4 ¬(B → C) by conjunction-elimination from (2)

5 ¬(¬A ∨ B) by the meaning of material conditional from (3)

6 (A ∧ ¬B) by De Morgan from (5)

7 ¬B by conjunction-elimination from (6)

8 ¬(¬B ∨ C) by the meaning of material conditional from (4)

9 (B ∧ ¬C) by De Morgan from (8)

10 B by conjunction-elimination from (9)

11 ⊥ from (7) and (10)

Therefore, ¬¬((A → B) ∨ (B → C)) ≡ (A → B) ∨ (B → C).

Answer 3

The proof presented in this answer is similar to the one Chris Sunami presented. It uses the law of the excluded middle (LEM), that is, "B ∨ ¬B" is always true. Consider each of the cases, "B", or , "¬B", and see if one can reach the desired result which is also a disjunction.

For the "B" case, start a subproof assuming "B" on line 1. On line 2 start another subproof assuming "A". Now we already have "B" so we can use reiteration (R) to repeat the assumption from line 1 on line 3. That is all we need for the conditional introduction on line 4. This gives us only half of what we want, but since the other half is connected with a disjunction (∨) we can just introduce a disjunction and add what we want on line 5.

For the "¬B" case, start a subproof assuming "¬B" and then another subproof assuming "B". This leads to a contradiction which is introduced on line 8. Once we have a contradiction we can use explosion (X) to obtain anything we want. We want "C". So we put "C" on line 9. From there using conditional introduction provides the conditional we needed to complete the proof. The disjunction introduction allows line 11 to look like line 5.

With both "B" and "¬B" providing the same result, "(A→B) ∨ (B→C)", we can discharge the assumptions, that is, close the subproofs and reach the desired result.

---

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/