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?

  • 3
    $\begingroup$ And the Axioms are... $\endgroup$ Dec 15, 2014 at 18:42
  • 4
    $\begingroup$ As your question stands, it can only be answered by people who remember Mendelson's axioms exactly, or have his book within immediate reach. I actually own a copy of the book, but it is not next to me at the moment, so I'll have to bow out. If you were to quote the axioms in your question, you would increase the number of potential responders vastly. $\endgroup$ Dec 15, 2014 at 18:51
  • 1
    $\begingroup$ One of the goals of good question writing is to make your questions self-contained. In this context, it means you should include the actual axioms and not just a reference to a book many of us may not have $\endgroup$
    – Alan
    Dec 15, 2014 at 18:51
  • 3
    $\begingroup$ @Doug: No, that is definitely not Mendelson's axioms. Like most other non-robots, he uses infix connectives such that human beings actually have a chance of grasping the formulas he write. $\endgroup$ Dec 15, 2014 at 18:59
  • 1
    $\begingroup$ @HenningMakholm You're right those aren't Mendelson's axioms, but I don't recall the script he uses, and I'm not even sure I know how to LaTex that script up here, so he hasn't asked for anything provable in Mendelson's system if you want to stick to definitions like that. Also, the user probably isn't using Mendelson's script either. And I am human being and other people who use Polish notation are also. I have no idea why you write in such a way as if I were not one. $\endgroup$ Dec 15, 2014 at 19:01

3 Answers 3


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

  • $\begingroup$ None of those preliminary results are necessary. So, I'm not sure what you meant by "need" here. $\endgroup$ Dec 17, 2014 at 18:21
  • $\begingroup$ I counted 16 uses of modus ponens. $\endgroup$ Dec 19, 2014 at 12:25
  • 3
    $\begingroup$ @Mauro You are awesome. To take the time to write this out to help other people is really great. $\endgroup$
    – samthebest
    Mar 22, 2016 at 20:04
  • $\begingroup$ This is great, but if I ever try writing all these steps in the exam I will probably answer only that question :) $\endgroup$ Oct 30, 2018 at 16:15
  • 1
    $\begingroup$ @samthebest - the answer is T4 above. $\endgroup$ May 21, 2019 at 14:50

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


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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .