Deduction of "Disjunction elimination"

Question

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$

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