I have at my disposal Modus Ponens (MP) and the three axioms:

  • A1: $(\alpha\to(\beta\to\alpha))$,
  • A2: $((\alpha\to(\beta \to\gamma))\to ((\alpha\to\beta)\to(\alpha\to\gamma)))$,
  • A3: $(((\lnot\beta)\to(\lnot\alpha))\to(((\lnot\beta)\to\alpha)\to\beta))$.

I'm trying to prove the Disjunction elimination: $$ \{\alpha\lor\beta,\alpha\to \gamma,\beta\to \gamma\}\vdash \gamma. $$

$\lor$ is not part of the alphabet I use, the deduction actually is: $$ \{((\neg\alpha)\to\beta),\alpha\to \gamma,\beta\to \gamma\}\vdash \gamma. $$

The deduction should be something like

\begin{array}{rl|l} \hline 1:&((\neg\alpha)\to\beta) & Premiss\\ 2:&\beta\to \gamma&Premiss\\ 3:&((\neg\alpha)\to\gamma)&1,2\ H.S.\\ 4:&(\alpha \to \gamma)&Premiss\\ 5:&\gamma& 3,4 [?]\\ \hline \end{array}

Where H.S. is Hypothetical Syllogism, a deduction that I have already proven.

The rule $[?]$, that I have to prove, correspond to $$ \{\alpha\to\beta,(\neg\alpha)\to\beta\}\vdash \beta.\tag{*} $$

(*) looks quite simple, but after hours no way to get it.

For information I have, if needed, proven other results, that I could reuse:

  • $\vdash\alpha\to\alpha$,
  • Hypothetical Syllogism: $\{\alpha\to\beta,\beta\to\gamma\}\vdash\alpha\to\gamma$,
  • $\vdash(\lnot\alpha\to\alpha)\to\alpha$,
  • $\vdash\alpha\lor\lnot\alpha$,
  • $\{\alpha\to(\beta\to\gamma),\beta\}\vdash\alpha\to\gamma$,
  • $\vdash(\neg\neg\alpha)\to\alpha$.
  • Negation introduction: $\{(\alpha\to\beta),(\alpha\to \neg\beta)\}\vdash \neg \alpha$.
  • Negation elimination: $\{\neg \alpha\}\vdash (\alpha\to \beta)$.
  • Double negative elimination: $\neg \neg \alpha\vdash \alpha$.
  • Conjunction introduction: $\{\alpha,\beta\}\vdash (\alpha\land \beta)$.

EDIT Additional known results:

  • $\neg\neg\alpha\vdash\alpha$
  • $\{\alpha,\neg\alpha\}\vdash\neg\beta$
  • $\{\alpha,\neg\alpha\}\vdash\beta$
  • Conjunction elimination, only $\alpha\land\beta\vdash\beta$
  • Disjunction introduction, only $\beta\vdash\alpha\lor\beta$
  • $\begingroup$ It seems easier to me prove modus tollens, which will allow you to do contraposition, i.e. $\neg \alpha \rightarrow \gamma$ is the same as $\neg \gamma \rightarrow \alpha$. Then you do not need your rule $(*)$. Furthermore, modus tollens would probably help you prove $(*)$: If you know $\neg \beta \rightarrow \neg \alpha$ and $\neg \beta \rightarrow \alpha$, then $\neg \beta$ would lead to a contradiction. $\endgroup$
    – mrp
    Apr 26, 2018 at 11:51
  • $\begingroup$ @mrp The proof of modus tollens would be also nice to have, sadly I wasn't able to derive it until now $\endgroup$ Apr 26, 2018 at 13:22
  • $\begingroup$ @LiPo Ha! I was in the middle or writing my answer, the first step was the derivation of Modus Tollens! With that, so you're almost there! $\endgroup$
    – Bram28
    Apr 26, 2018 at 13:24

1 Answer 1


Assuming you are allowed to use the Deduction Theorem:

Let's first prove Modus Tollens: $\varphi \rightarrow \psi, \neg \psi \vdash \neg \varphi$:

  1. $\varphi \rightarrow \psi$ Premise
  2. $\neg \psi$ Premise
  3. $\neg \psi \rightarrow (\neg \neg \varphi \rightarrow \neg \psi)$ A1
  4. $\neg \neg \varphi \rightarrow \neg \psi$ MP 2,3
  5. $\neg \neg \varphi \rightarrow \varphi$ Double Negation Elimination
  6. $\neg \neg \varphi \rightarrow \psi$ H.S. 1,5
  7. $(\neg \neg \varphi \rightarrow \neg \psi) \rightarrow ((\neg \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi)$ A3
  8. $(\neg \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi$ MP 4,7
  9. $\neg \varphi$ MP 6,8

With the Deduction Theorem, this gives us Contraposition: $\varphi \rightarrow \psi \vdash \neg \psi \rightarrow \neg \varphi$

And now we can show $\varphi \rightarrow \psi, \neg \varphi \rightarrow \psi \vdash \psi$:

  1. $\varphi \rightarrow \psi$ Premise
  2. $\neg \varphi \rightarrow \psi$ Premise
  3. $\neg \psi \rightarrow \neg \varphi$ Contraposition 1
  4. $\neg \psi \rightarrow \neg \neg \varphi$ Contraposition 2
  5. $(\neg \psi \rightarrow \neg \neg \varphi) \rightarrow ((\neg \psi \rightarrow \neg \varphi) \rightarrow \psi)$ A3
  6. $(\neg \psi \rightarrow \neg \varphi) \rightarrow \psi$ MP 4,5
  7. $\psi$ MP 3,6
  • $\begingroup$ wow! thank you! $\endgroup$ Apr 26, 2018 at 13:39
  • $\begingroup$ @LiPo You're welcome! It's just a matter of creating a library of all these Lemma's. Creating them is a pain, but once you have them, proofs get easier and easier :) $\endgroup$
    – Bram28
    Apr 26, 2018 at 13:42

You must log in to answer this question.

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