presentation
lecturers
registration
program
general information
anterior próximo
 
 
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