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

Question

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?

Answer 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

Answer 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).

Answer 3

I don't know how to write those fancy Bs and those fancy Cs that Mendelson uses in that text. Mendelson has parentheses (deliberately) around all wffs in when talking about the axiom schema, and that makes good sense since it makes substitution for wffs by other wffs just a matter of finding similar symbol patterns. We don't need to infer a meaning and recognize a pattern, we only need to recognize a pattern when you actually write wffs.

Due the correspondence between Mendelson's semantic statement forms and Mendelson's syntactic wffs, wffs have similar properties to statement forms. Mendelson indicates in exercise 1.18 on p. 12 of the fifth edition that instead of writing statement forms as he usually does, that Polish notation can get used, which looks like any prefix notation according to him. The following system has symbols more like the original Polish notation of Lukasiewicz, Meredith, Prior, and other authors whose papers you can read for free via old issues of the Norte Dame Journal of Formal Logic. Due to how Mendelson writes in his Schaum's Outline of Boolean Algebra, it appears that we can faithfully represent Mendelson's intent using bold capital letters instead of fancy capital letters. The following puts each axiom schema of the system in Polish notation that I'll use next to the corresponding axiom schema of Mendelson's system.

  Polish               Mendelson

Ax 1 CbCcb ..................... (B -> (C -> B))

Ax 2 CCbCcdCCbcCbd ... ((B -> (C -> D)) -> ((B -> C) -> (B -> D)))

Ax 3 CCNcNbCCNcbc .....((($\lnot$C) -> ($\lnot$B)) -> ((($\lnot$C) -> B) -> C))

A proof in a system using Polish notation of a certain length implies that a proof in Mendelson's system using Mendelson's notation of the same length can get written.

Axiom Schema                 1  CbCcb
Axiom Schema                 2  CCbCcdCCbcCbd
Axiom Schema                 3  CCNcNbCCNcbc
1 b/CbCcb, c/a               4  CCbCcbCaCbCcb
4 * C1-5                     5  CaCbCcb
2 b/CbCcd, c/Cbc, d/Cbd      6  CCCbCcdCCbcCbdCCCbCcdCbcCCbCcdCbd
6 * C1-7                     7  CCCbCcdCbcCCbCcdCbd
2 b/a, c/b, d/Ccb            8  CCaCbCcbCCabCaCcb
8 * C5-9                     9  CCabCaCcb
5 a/CbCCcbd                  10 CCbCCcbdCbCcb
7 c/Ccb                      11 CCCbCCcbdCbCcbCCbCCcbdCbd
11 * C10-12                  12 CCbCCcbdCbd
9 a/CNcNb, b/CCNcbc, c/d     13 CCCNcNbCCNcbcCCNcNbCdCCNcbc
13 * C3-14                   14 CCNcNbCdCCNcbc
1 b/CCbCCcbdCbd, c/a         15 CCCbCCcbdCbdCaCCbCCcbdCbd
15 * C12-16                  16 CaCCbCCcbdCbd
2 b/a, c/CbCCcbd, d/Cbd      17 CCaCCbCCcbdCbdCCaCbCCcbdCaCbd
17 * C16-18                  18 CCaCbCCcbdCaCbd
18 a/CNcNb, c/Nc, d/c        19 CCCNcNbCbCCNcbcCCNcNbCbc
14 d/b                       20 CCNcNbCbCCNcbc
19 * C20-21                  21 CCNcNbCbc

So, a proof can get written in Mendelson's system in 21 steps if we include the original 3 schema. If we don't, it can get done in exactly 18 steps.