Equivalence of Deductive System $L_0$ and the Sequent Calculus Let $\mathcal{L}_0=\mathcal{L}[\{\neg, \rightarrow\}]$. Define the system $L_0$ as follows:
An axiom of $L_0$ is any formula of $\mathcal{L}_0$ of the form


*

*(A1) $(\alpha \rightarrow ( \beta \rightarrow \alpha))$

*(A2) $((\alpha \rightarrow ( \beta \rightarrow \gamma) \rightarrow ((\alpha \rightarrow \beta) \rightarrow ( \beta \rightarrow \gamma)))$

*(A3) $((\neg \beta \rightarrow \neg \alpha ) \rightarrow (\alpha \rightarrow \beta))$


The only rule of inference in $L_0$ is modus ponens, i.e. from $\alpha$ and $(\alpha \rightarrow \beta)$ infer $\beta$.

A formula of $\mathcal{L}_0$, $\phi$, is provable from a set of formulas $\Gamma$ in the system $SQ$, if there exists a finite sequence of sequents where each follows from the next according to the following set of rules:


*

*(Ass) If $\psi \in \Delta$, we infer $\Delta \vdash_{SQ} \psi$

*(MP) If $\Delta \vdash_{SQ} \psi$ and $\Delta ' \vdash_{SQ} (\psi \rightarrow \phi)$  then infer $\Delta \cup \Delta ' \vdash_{SQ} \phi$

*(DT) If $\Delta \cup \{\psi \} \vdash_{SQ} \chi$ we infer $\Delta \vdash_{SQ} (\psi \rightarrow \chi)$

*(PC) If $\Delta \cup \{ \neg \psi \} \vdash_{SQ} \chi$ and $\Delta ' \cup \{ \neg \psi \} \vdash_{SQ} \neg \chi$ infer that $\Delta \cup \Delta ' \vdash_{SQ} \psi$





Prove that the systems $SQ$ and $L_0$ are equivalent, i.e. that $\Gamma \vdash_{L_0} \phi$ iff $\Gamma \vdash_{SQ} \phi$.


Ideally the legwork for this has been done elsewhere, in which case a link will be gratefully received. 
Is the idea then to show that $\emptyset \vdash_{SQ} (A1)$, $\emptyset \vdash_{SQ} (A2)$, $\emptyset \vdash_{SQ} (A3)$ and that $SQ$ somehow implies (MP) in $L_0$, and then to do the reverse, i.e. show that $L_0$ proves each of the sequents of $SQ$? I don't quite see how that would be formalised.
 A: I suppose there is a mistake; your (A2) must be :

$(α→(β→γ)) \rightarrow ((α→β)→(α→γ))$.

From $SQ$ to $\mathsf L_0$ we have :
(A1)
1) --- $\alpha, \beta \vdash \alpha$ --- by (Ass)
2) --- $\alpha \vdash \beta \rightarrow \alpha$ --- from 1) by (DT)
3) --- $\vdash \alpha \rightarrow (\beta \rightarrow \alpha)$ --- from 2) by (DT).
(A2)
1) --- $\alpha \rightarrow (\beta \rightarrow \gamma) \vdash \alpha \rightarrow (\beta \rightarrow \gamma)$ --- by (Ass)
2) --- $\alpha \vdash \alpha $ --- by (Ass)
3) --- $\alpha, \alpha \rightarrow (\beta \rightarrow \gamma) \vdash \beta \rightarrow \gamma$ --- from 1), 2) by (MP)
4) --- $\alpha \rightarrow \beta \vdash \alpha \rightarrow \beta $ --- by (Ass)
5) --- $\alpha, \alpha \rightarrow \beta \vdash \beta $ --- from 2), 4) by (MP)
6) --- $\alpha, \alpha \rightarrow \beta, \alpha \rightarrow (\beta \rightarrow \gamma) \vdash \gamma$ --- from 3), 5) by (MP)
7) --- $\alpha \rightarrow \beta, \alpha \rightarrow (\beta \rightarrow \gamma) \vdash \alpha \rightarrow \gamma$ --- from 6) by (DT)
8) --- $\alpha \rightarrow (\beta \rightarrow \gamma) \vdash (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma)$ --- from 7) by (DT)
9) --- $\vdash (\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma))$ --- from 8) by (DT).
(A3)
1) --- $\lnot \beta \rightarrow \lnot \alpha \vdash \lnot \beta \rightarrow \lnot \alpha$ --- by (Ass)
2) --- $\lnot \beta \vdash \lnot \beta$ --- by (Ass)
3) --- $\lnot \beta, \lnot \beta \rightarrow \lnot \alpha \vdash \lnot \alpha$ --- from 1), 2) by (MP)
4) --- $\alpha, \lnot \beta \vdash \alpha$ --- by (Ass)
5) --- $\alpha, \lnot \beta \rightarrow \lnot \alpha \vdash \beta$ --- from 4), 5) by (PC)
6) --- $\lnot \beta \rightarrow \lnot \alpha \vdash \alpha \rightarrow \beta$ --- from 5) by (DT)
7) --- $\vdash (\lnot \beta \rightarrow \lnot \alpha) \rightarrow (\alpha \rightarrow \beta$) --- from 6) by (DT).
The only rule of inference of $\mathsf L_0$ is modus ponens; we derive it from (MP) simply with $\Delta = \Delta' = \emptyset$.
