Can we prove if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β in L0? The system L0 is defined as follows:
Axioms:
A1 (α → (β → α))
A2 ((α → (β → γ)) → ((α → β) → (α → γ)))
A3 ((¬β → ¬α) → (α → β))
The only rule of inference is Modus Ponens:
MP From α and (α → β) infer β.
In one of my problem sheets, I am told that I am allowed to use the following theorem:
if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β
I am wondering if it is possible to prove this within the system? We've proved the Deduction Theorem, but I don't think its obviously useful here. I want to say something like "either a is true or ¬α is true" but this is not the sort of proof that was given for DT - however, without this sort of reasoning, I'm struggling to see an obvious way of proving the theorem.
Is it provable? And if so, can you point me in the right direction?
Thanks a lot!
 A: Yes, we can, but it's a bit of work! (well, I myself couldn't find any shorter way ...)
First, let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:


*

*$\phi \to \psi$ Premise

*$\psi \to \chi$ Premise

*$\phi$ Premise

*$\psi$ MP 1,3

*$\chi$ MP 2,4
By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$
Now let's prove the general principle that $\neg \phi \vdash (\phi \to \psi)$:


*

*$\neg \phi$ Premise

*$\neg \phi \to (\neg \psi \to \neg \phi)$ A1

*$\neg \psi \to \neg \phi$  MP 1,2

*$(\neg \psi \to \neg \phi) \to (\phi \to \psi)$ A3

*$\phi \to \psi$ MP 3,4
With the Deduction Theorem, this means $\vdash \neg \phi \to (\phi \to \psi)$ (Duns Scotus Law)
Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$


*

*$\neg \phi \to \phi$ Premise

*$\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))$ (Duns Scotus Law)

*$(\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)))$  A2

*$(\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))$  MP 2,3

*$\neg \phi \to \neg (\neg \phi \to \phi)$ MP 1,4

*$(\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi)$ A3

*$(\neg \phi \to \phi) \to \phi$  MP 5,6

*$\phi$ MP 1,7
By the Deduction Theorem, this means $\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)
Using Duns Scotus and the Law of Clavius, we can now show that $ \neg \neg \phi \vdash \phi$:


*

*$\neg \neg \phi$ Premise

*$\neg \neg \phi \to (\neg \phi \to \phi)$ Duns Scotus

*$\neg \phi \to \phi$ MP 1,2

*$(\neg \phi \to \phi) \to \phi$ Law of Clavius

*$\phi$ MP 3,4
By the Deduction Theorem, this also means that $\vdash \neg \neg \phi \to \phi$ (DN Elim)
Now we can prove $\vdash \phi \to \neg \neg \phi$ (DN Intro) as well:


*

*$\neg \neg \neg \phi \to \neg \phi$ (DN Elim)

*$(\neg \neg \neg \phi \to \neg \phi) \to (\phi \to \neg \neg \phi)$ A3

*$\phi \to \neg \neg \phi$ MP 1,2
Now we can derive Modus Tollens: $\phi \to \psi, \neg \psi \vdash \neg \phi$:


*

*$\phi \to \psi$ Premise

*$\neg \psi$ Premise

*$\neg \neg \phi \to \phi$ DN Elim

*$\neg \neg \phi \to \psi$ HS 1,3

*$\psi \to \neg \neg \psi$ DN Intro

*$\neg \neg \phi \to \neg \neg \psi$ HS 4,5

*$(\neg \neg \phi \to \neg \neg \psi) \to (\neg \psi \to \neg \phi)$ A3

*$\neg \psi \to \neg \phi$ MP 6,7

*$\neg \phi$ MP 2,8
By the Deduction Theorem this gives us $\phi \to \psi \vdash \neg \psi \to \neg \phi$ (Contraposition) 
(historical sidenote: if we apply the Deduction Theorem on Contraposition, we get $\vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi)$ , which is one of the axioms used by Frege ... Frege also used DN Intro and DN Elim as axioms, but Lukaciewicz figured out how to derive all these three using A3).
Finally, we can prove $\phi \to \psi, \neg \phi \to \psi \vdash \psi$:


*

*$\phi \to \psi$ Premise

*$\neg \phi \to \psi$ Premise

*$\neg \psi \to \neg \phi$ Contraposition 1

*$\neg \psi \to \psi$ HS 2,3

*$(\neg \psi \to \psi) \to \psi$ Law of Clavius

*$\psi$ MP 4,5
Or, we can apply the Deduction Theorem twice to get it in its conditionalized form:
$\vdash (\phi \to \psi) \to ((\neg \phi \to \psi) \to \psi)$
So yes, this certainly means that if $\vdash \alpha \to \beta$ and $\vdash \neg \alpha \to \beta$, then$\vdash \beta$
