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

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?

Solution 1:

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

Solution 2:

I'm currently reading Mendelson's text, and this is how I proved exercise 1.47(d). It requires both the results from exercises 1.47(a) and (c), which are previous parts of the same exercise.

Here are the axioms:

(A1) $A\Rightarrow \left(B\Rightarrow A\right)$.

(A2) $\left(A\Rightarrow \left(B\Rightarrow C\right)\right)\Rightarrow\left(\left(A\Rightarrow B\right)\Rightarrow\left(A\Rightarrow C\right)\right)$.

(A3) $\left(\neg B\Rightarrow\neg A\right)\Rightarrow\left(\left(\neg B\Rightarrow A\right)\Rightarrow B\right)$.

The only rule of inference is Modus Ponens:

(MP) $\left\langle A, A\Rightarrow B, B\right\rangle$

The previous results you should have already proven within the same section:

1.47(a) $\mathcal{A}\Rightarrow\mathcal{B}, \mathcal{B}\Rightarrow\mathcal{C}\vdash_{L}\mathcal{A}\Rightarrow\mathcal{C}$.

1.47(c) $\mathcal{A}\Rightarrow\left(\mathcal{B}\Rightarrow\mathcal{C}\right)\vdash_{L}\mathcal{B}\Rightarrow\left(\mathcal{A}\Rightarrow\mathcal{C}\right)$.

Here is the proof of the exercise:

1. $\varphi\Rightarrow\left(\neg\psi\Rightarrow\varphi\right)$, from (A1).

2. $\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\left(\left(\neg\psi\Rightarrow\varphi\right)\Rightarrow\psi\right)$, from (A3).

3. $\left(\neg\psi\Rightarrow\varphi\right)\Rightarrow\left(\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\psi\right)$, from 1.47(c) using 2.

4. $\varphi\Rightarrow\left(\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\psi\right)$, from 1.47(a) using 1. and 3.

5. $\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\left(\varphi\Rightarrow\psi\right)$, from 1.47(c) using 4.

This completes the proof.

It is important to note here that the Deduction Theorem was not used. Though it is unnecessary, you can embed into this proof the proof of 1.47(a) or (c) wherever one of them is used. The Axioms (A1) and (A3) are the only underlying premises justifying the first usage of 1.47(c).