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

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.