4
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ I've edited it. It was a mistake. $\endgroup$
    – user65526
    Jun 28, 2017 at 17:40
  • $\begingroup$ 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. $\endgroup$
    – DanielV
    Jun 29, 2017 at 3:03
  • $\begingroup$ I just saw this question - it might be worth noting that I have a formal proof in Coq of the equivalence for one particular formulation of each (though in that case it's for intuitionistic propositional logic, but doing the same thing for classical propositional logic should be very similar). github.com/dschepler/coq-sequent-calculus/blob/master/Hilbert.v and look at the result ND_hilbert_equiv at the end. $\endgroup$
    – Daniel Schepler
    Feb 17, 2021 at 21:44

1 Answer 1

Reset to default
4
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ 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." ? $\endgroup$
    – user65526
    Jun 29, 2017 at 9:08
  • $\begingroup$ I would understand this use of $\vee$ if there were more than one formula in the consequent, but this is explicitly ruled out. $\endgroup$
    – user65526
    Jun 29, 2017 at 9:14
  • $\begingroup$ @user65526 - maybe because in classical logic the consequent $\Delta$ may have more than one element. $\endgroup$
    – Mauro ALLEGRANZA
    Jun 29, 2017 at 12:33
  • $\begingroup$ @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. $\endgroup$
    – hmakholm left over Monica
    Jun 29, 2017 at 12:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .