[Math] Prove $( \lnot C \implies \lnot B) \implies (B \implies C)$ without the Deduction Theorem

formal-proofslogicpropositional-calculus

The issue is Exercise 1.47 (d) in Elliot Mendelson's "Mathematical Logic". The exercise is to prove $(\lnot C\implies\lnot B)\implies(B\implies C)$ by using the three axioms $(A1,A2,A3)$ without using the Deduction theorem (and without any hypothesis).

The axioms are:

$A1: B\implies(C\implies B)$

$A2: (B\implies(C\implies D))\implies((B\implies C)\implies(B\implies D))$
$A3: (\lnot C\implies\lnot B)\implies((\lnot C\implies B)\implies C)$

The only inference rule is MP.

I have a proof but it is long. My proof is based on the proof of Lemma 1.11 (d) which proves $(\lnot C\implies\lnot B)\implies(B\implies C)$ but uses the Deduction Theorem (Proposition 1.9). Then, like Mendelson suggests in exercise 1.49, I apply the process used to prove the Deduction Theorem to the steps. To be precise, I assume $(\lnot C\implies\lnot B)$ as a Hypothesis $H$. If $C_1,C_2,\dots,C_n$ is a proof of $(B\implies C)$ that uses $H$ then stepwise I prove $H\implies C_i$ for $i=1,\dots,n$. The last step is $H\implies C_n$ which is what we want to prove.

This way requires around 4 uses of Axiom1, 4 of Axiom2, 1 Axiom3, and 9 uses of Modus Ponens.

Do I miss a shorter proof?

Best Answer

I'm able to prove it "independently" from the Deduction Theorem, but the proof is quite longer ...

The axioms are :

  1. $F \rightarrow (G \rightarrow F)$

  2. $(F \rightarrow (G \rightarrow H))\rightarrow ((F \rightarrow G) \rightarrow (F \rightarrow H))$

  3. $(\neg G \rightarrow \neg F) \rightarrow ((\neg G \rightarrow F) \rightarrow G)$

For readibility, I'll organize the proof with some preliminary results :

T1 : $P \rightarrow P$

1) $P \rightarrow ((Q \rightarrow P) \rightarrow P)$ --- Ax.1

2) $P \rightarrow (Q \rightarrow P)$ --- Ax.1

3) $(1) \rightarrow ((2) \rightarrow (P \rightarrow P))$ --- Ax.2

4) $P \rightarrow P$ --- from 3), 1) and 2) by Modus Ponens twice.

T2 : $(Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$

1) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- Ax.2

2) $(1) \rightarrow ((Q \rightarrow R) \rightarrow (1))$ --- Ax.1

3) $(Q \rightarrow R) \rightarrow (1)$ --- from 1) and 2) by Modus Ponens

4) $(Q \rightarrow R) \rightarrow (P \rightarrow (Q \rightarrow R))$ --- Ax.1

5) $(3) \rightarrow ((4) \rightarrow ((Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))))$ --- Ax.2

6) $(Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- from 5), 3) and 4) by MP twice.

T3 : $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$

1) $(P \rightarrow Q) \rightarrow (P \rightarrow Q)$ --- T1

2) $(1) \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))$ --- Ax.2

3) $((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)$ --- from 1) and 2) by MP

4) $P \rightarrow ((P \rightarrow Q) \rightarrow P)$ --- Ax.1

5) $(3) \rightarrow ((4) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))$ --- T2

6) $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$ --- from 5), 3) and 4) by MP twice.

T4 : $(P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))$

1) $((P \rightarrow Q) \rightarrow (P \rightarrow R)) \rightarrow ((Q \rightarrow (P \rightarrow Q)) \rightarrow (Q \rightarrow (P \rightarrow R)))$ --- T2

2) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- Ax.2

3) $Q \rightarrow (P \rightarrow Q)$ --- Ax.1

4) $(1) \rightarrow ((2) \rightarrow ((P \rightarrow (Q \rightarrow R)) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R)))))$ --- T2

5) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R)))$ --- from 4), 1) and 2) by MP twice

6) $(3) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R))) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- T3

7) $((3) \rightarrow (Q \rightarrow (P \rightarrow R))) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- from 6) and 3) by MP

8) $(7) \rightarrow ((5) \rightarrow ((P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))))$ --- T2

9) $(P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- from 8), 7) and 5) by MP twice.

Now for the proof :

1) $(\neg C \rightarrow \neg B) \rightarrow ((\neg C \rightarrow B) \rightarrow C)$ --- Ax.3

2) $B \rightarrow (\neg C \rightarrow B)$ --- Ax.1

3) $(\neg C \rightarrow B) \rightarrow ((\neg C \rightarrow \neg B) \rightarrow C)$ --- from 1) and T4 by Modus Ponens

4) $B \rightarrow ((\neg C \rightarrow \neg B) \rightarrow C)$ --- from T2, 3) and 2) by MP twice

5) $(\neg C \rightarrow \neg B) \rightarrow (B \rightarrow C)$ --- from T4 and 4) by MP

Related Question