# Showing a Hilbert style axiomatic proof system and a Gentzen natural deduction in sequent style calculus are equivalent

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

An example proof of an equivalence between a Hilbert and a Gentzen natural deduction system in sequent style would help me.

• I've edited it. It was a mistake. – user65526 Jun 28 '17 at 17:40
• You have to define the transform under which they are the same. The main idea of it is that, in ND, a proposition $P$ under the assumptions $A_0, A_1, \dots$ is equivalent to a proposition in Hilbert $A_0 \to (A_1 \to (\dots \to P))$. Then the modus ponens of ND is mechanically different than the modus ponens of Hilbert: it actually translates from ND to Hilbert into nothing. – DanielV Jun 29 '17 at 3:03

## 1 Answer

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.

• Why in the article does it use $\vee$ (which I suppose denotes generalised union) in "One proves a stronger theorem, showing that when $\Gamma$ is finite and $\Delta$ contains at most one formula, the sequent $\Gamma \vdash_{N}\Delta$ is derivable iff $\Gamma \vdash_{H} \vee \Delta$, where $\vee \Delta = M$ if $\Delta = \{ M \}$, and $\vee \emptyset$ = false." ? – user65526 Jun 29 '17 at 9:08
• I would understand this use of $\vee$ if there were more than one formula in the consequent, but this is explicitly ruled out. – user65526 Jun 29 '17 at 9:14
• @user65526 - maybe because in classical logic the consequent $\Delta$ may have more than one element. – Mauro ALLEGRANZA Jun 29 '17 at 12:33
• @user65526: Ah! Now that I actually look at the paper you link to (I thought the link was wrong because page 5 didn't contain anything relevant; but page 7 does!), I see the source of some of your confusion. What it presents as "Gentzen Rules" is not a natural deduction system, but a sequent calculus a la Gentzen's LJ. (Gentzen invented both of these two styles of proof systems, but they are not the same). In this answer I was assuming it was actually a natural deduction system like you said. The overall two-part strategy I suggest will still work, the details I sketched won't. – Henning Makholm Jun 29 '17 at 12:48