I wish for a formal proof for $\vdash\neg\alpha\rightarrow(\alpha\rightarrow\beta)$ which doesn't use deduction theorem.

I use the standard axiomatic system:



$(\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow \beta)$

Using axiom 2 we get: $$(\neg\alpha \rightarrow((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta)))\rightarrow((\neg\alpha \rightarrow(\neg\beta\rightarrow\neg\alpha))\rightarrow(\neg\alpha\rightarrow(\alpha\rightarrow\beta)))$$

which is very promising casue the second expresion is axiom 1, and the expression:$(\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta)$ can be proved using deduction theorem in the next manner:

$1. \neg\beta\rightarrow \neg \alpha$ assumption

$2.\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta))$ $A2$

$3. (\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow\beta)$ $A3$

$4. (\neg\beta\rightarrow\alpha)\rightarrow\beta) $ by MP $1$ from $3$

$5. (\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow(\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta))$ $A1$

$6. (\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta))$ MP by 4

$7. ((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta))$ MP 6 from 2

$8.(\alpha\rightarrow(\neg \beta\rightarrow \alpha) $ A1

$9. \alpha\rightarrow \beta$ MP 7 using 8

I was trying to reverse the proof by seduction theorem using the method by which the Deduction Theorem is proved. So, I need to prove $\neg\beta \rightarrow \neg\alpha \rightarrow (step(i))$ when $step(i)$ is each of the step in the proof demonstrated above. Doing so (as you may see below) lead me to the next conclusion:

if one proves : $((\neg\beta \rightarrow\neg\alpha)\rightarrow((\alpha\rightarrow(\neg\beta\rightarrow\alpha))\rightarrow(\alpha \rightarrow\beta))) \rightarrow(((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow(\neg\beta\rightarrow\alpha)))\rightarrow((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta)))$

The second expression can be proved by using 2 times Axiom 1.

For the first expression which I'm stuck in, I tried to prove: $(\alpha\rightarrow(\neg\beta\rightarrow\alpha))\rightarrow(\alpha \rightarrow\beta))$ And then using Axiom 1 , but I realized that's can't be proved without assumption cause it is not a tautology! the first expression is Axiom 1 so it is tautology, then in case $\alpha\rightarrow\beta$ is not True ($\alpha = T, \beta = F)$ we get a False statement.

Maybe I took the wrong path? is it another way to solve it? Also, it is worth to mention that this question comes from previous attempt for an other proof I am still trying to make (and I think, this proof is the key for the other):Formally proving $p\wedge q \rightarrow p$

Reversing the Deduction theorem usage:

$1^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow(\neg\beta\rightarrow \neg \alpha)$ . The same pattern as to prove $\alpha \rightarrow \alpha$

$2^*.\vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow (\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta)))$ Prooving a formula of the pattern $\gamma\rightarrow Axiom$ can be done by using Axiom1.

$3^*.\vdash (\neg\beta\rightarrow \neg \alpha)\rightarrow ((\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow\beta))$ same pattern as $2^*$

$4^*. \vdash (\neg\beta\rightarrow \neg \alpha)\rightarrow ((\neg\beta\rightarrow\alpha)\rightarrow\beta)) $ This is an Axiom3 pattern.

$5^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow ((\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow(\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)))$ same pattern as $2^*$ $\gamma \rightarrow Axiom$

$6^*.\vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow ( (\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)))$ MP by 4 This is the formula which I don't succeed to prove.

$7^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow (((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta)))$ MP 6 from 2

$8^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow((\alpha\rightarrow(\neg \beta\rightarrow \alpha)) $ A1

$9^*. \vdash (\neg\beta\rightarrow \neg \alpha)\rightarrow (\alpha\rightarrow \beta)$ MP 7 using 8

  • $\begingroup$ The proof of the deduction theorem is constructive. If you know the proof, then it is a straightforward to convert any theorem using the deduction theorem to one that doesn't use it. $\endgroup$
    – DanielV
    May 3 '18 at 0:50
  • $\begingroup$ Can you substitute wffs for propositional variables in theorems or only make such substitutions in the axioms? $\endgroup$ May 3 '18 at 3:09
  • $\begingroup$ @DanielV In order to do so, I need to prove $\neg\beta\rightarrow \neg\alpha \rightarrow step(i) $ for each step in the proof I showed for $\neg\beta\rightarrow\neg\alpha \vdash \beta \rightarrow \alpha$ and this is exactly what I did, and that is how I came to the last axiom 2 expression which I can't figure out. $\endgroup$ May 3 '18 at 3:41
  • $\begingroup$ @DougSpoonwood I'm sorry but I don't understand what is the meaning of substituting with theorems? May you please give an example? $\endgroup$ May 3 '18 at 3:43
  • $\begingroup$ The way to "solve" this type of problem is simple and boring: start with an easy derivation with the DT (see page 39 ) and then apply the procedure used in the proof of the DT to eliminate the application of the DT (see page 37 ). $\endgroup$ May 3 '18 at 6:41


As said, the proof is simple and (very) boring.

We have to start from the derivation using DT (see e.g. Mendelson ) an "expurgate" the calls to DT: we have to do it one-by-one.

Thus, starting from the derivation $\lnot B, B \vdash C$ we have firstly to produce the new derivation $\lnot B \vdash B \to C$.

I'll follow Mendelson's original derivation :

1') $\lnot B$ --- Hyp

3') $\vdash B \to (\lnot C \to B)$ --- Ax.1

4') $\vdash B \to (\lnot B \to (\lnot C \to \lnot B))$ --- derived from the suitable Ax.1 : $\vdash (\lnot B \to (\lnot C \to \lnot B)) \to [B \to (\lnot B \to (\lnot C \to \lnot B))]$ with Ax.1 and mp

5') $B \to \lnot B$ --- derived from Ax.1 : $\lnot B \to (B \to \lnot B)$ with 1') and mp

6') $B \to (\lnot C \to \lnot B)$ --- derived from Ax.2 with 4') and 5') by mp twice

7') $\vdash [B \to ((\lnot C \to \lnot B) \to ((\lnot C \to B) \to C))] \to [(B \to (\lnot C \to \lnot B)) \to (B \to ((\lnot C \to B) \to C))] \text { --- Ax.2}$

8') $\vdash B \to ((\lnot C \to \lnot B) \to ((\lnot C \to B) \to C))$ --- derived from Ax.3 with suitable Ax.1 and mp

9') $\vdash (B \to (\lnot C \to \lnot B)) \to (B \to ((\lnot C \to B) \to C))$ --- derived 7') and 8') by mp

10') $B \to ((\lnot C \to B) \to C)$ --- derived from 9') and 6') by mp

11') $B \to C$ --- derived from Ax.2 with 3') and 10') by mp twice.

  • $\begingroup$ Thanks! it took me an hour to fully formalize it!! Now I need to do the same for $(\neg\beta \rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta)$ =DD $\endgroup$ May 3 '18 at 13:14

My answer is: $$\begin{array}{r|ll} 1 & \neg\alpha\rightarrow(\neg\beta\rightarrow\neg\alpha) & Ax. 1\\ 2 & (\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta) & Ax. 3\\ 3 & (\neg\alpha\rightarrow(\neg\beta\rightarrow\neg\alpha))\rightarrow(((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta))\rightarrow(\neg\alpha\rightarrow(\alpha\rightarrow\beta))) & Ax. 2\\ 4 & ((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta))\rightarrow(\neg\alpha\rightarrow(\alpha\rightarrow\beta)) & 1,3,MP\\ 5 & \neg\alpha\rightarrow(\alpha\rightarrow\beta) & 2,4,MP \end{array}$$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.