|
|
 |
 |
 |
|
 |
|
Revisiting Zucker's work on the correspondence
between cut-elimination and normalisation
Zucker showed in [1] that given the usual mapping from
sequent proofs to natural deduction proofs there is a close
correspondence between cut-elimination and normalisation in
the {&,->,forall}-fragment of intuitionistic logic. He claimed
that this correspondence fails if the connectives v and exists
are included. This is because in his setting the cut-elimination
procedure is not strongly normalising for v and exists. We shall
present a cut-elimination procedure which is strongly normalising
for all connectives and then show the correspondence with
normalisation for the fragment that includes exists, i.e. the
{&,->,forall,exists}-fragment. We also detail why the correspondence
fails for the v-connective, even if both our normalisation and cut-
elimination procedures are strongly normalising. Since we use term
annotations for sequent and natural deduction proofs, our arguments
are much simpler in comparison with Zucker's work.
[1] Zucker: The correspondence between cut-elimination and
normalisation, Annals of Mathematical Logic 7 (1974), pages 1-112
|
|
|
|
 |
|
 |