Can anyone point me to a proof that a given Hilbert style axiomatisation of intuitionistic propositional logic ($H$) and a given natural deduction formulation of intuitionistic logic in sequent style ($N$) are equivalent, in the following sense?
- for all formulas, $M$, $\hspace{0.3cm} \Gamma \vdash_{H} M$ iff $\Gamma \vdash_N M$ is derivable, where $\Gamma$ is finite and $M$ contains at most one formula.
My interest in this question comes from wanting to prove $THEOREM \thinspace 2.3$ in
- Matt Fairtlough and Michael Mendler, Propositional Lax Logic (1997): THEOREM 2.3, page 7.
An example proof of an equivalence between a Hilbert and a Gentzen natural deduction system in sequent style would help me.
You'll want to prove separately that $\Gamma \vdash_H M$ implies $\Gamma \vdash_N M$ and vice versa. Each of these cases can be done by induction on the structure of the proof tree (or by the length of a proof, if your $H$ represents proofs as flat sequences of formulae rather than trees).
The direction ${\vdash_H} \Rightarrow {\vdash_N}$ is easy, since the only inference rule in $H$ is modus ponens, which is also a rule of $N$ (usually called $\to$-elimination in that setting). So all you really have to do is to show that each (instance of a) logical axiom of $H$ can be proved in $N$.
For the direction ${\vdash_N} \Rightarrow {\vdash_H}$, most of the cases are easy. The inference rules of $N$ that don't add anything to the $\Gamma$s can simply be replaced by local derivations of $H$. For example, for $\land$-introduction $$ \frac{\Gamma\vdash_N M \qquad \Gamma\vdash_N K}{\Gamma \vdash_N M\land K} \,{\land I} $$ show once and for all that $$ \vdash_H M \to ( K \to M \land K ) $$ for all $M$ and $K$ -- usually this is immediate because that is an axiom of the Hilbert system, but for some systems a bit of proofwork will be needed. Then every application of $\land I$ can be replaced by this proof and two applications of MP after the premises have been translated to $\vdash_H$ by the induction hypothesis.
The main case in a typical natural deduction system (for propositional calculus) where this will not work is $\to$-introduction. Here, exactly what you need to make the case go through is the deduction theorem for $\vdash_H$, which hopefully you have proved already for its own sake.
The $\lor$-elimination rule in its most common formulation will require a combination of these approaches. Apply the deduction theorem to the two premises that extend $\Gamma$, and then show that $$ \vdash_H (K\lor L)\to((K\to M)\to((L\to M)\to M)) $$ and apply MP three times.