Deduction of "Disjunction elimination"

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

• $\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$
• 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.
– mrp
Apr 26, 2018 at 11:51
• @mrp The proof of modus tollens would be also nice to have, sadly I wasn't able to derive it until now Apr 26, 2018 at 13:22
• @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! Apr 26, 2018 at 13:24

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
• wow! thank you! Apr 26, 2018 at 13:39
• @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 :) Apr 26, 2018 at 13:42