Cut-elimination, substitution and normalisation

Roy Dyckhoff

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

5 Citations (Scopus)
7 Downloads (Pure)


We present a proof (of the main parts of which there is a formal version, checked with the Isabelle proof assistant) that, for a G3-style calculus covering all of intuitionistic zero-order logic, with an associated term calculus, and with a particular strongly normalising and confluent system of cut-reduction rules, every reduction step has, as its natural deduction translation, a sequence of zero or more reduction steps (detour reductions, permutation reductions or simplifications). This complements and (we believe) clarifies earlier work by (e.g.) Zucker and Pottinger on a question raised in 1971 by Kreisel.
Original languageEnglish
Title of host publicationDag Prawitz on Proofs and Meaning
EditorsHeinrich Wansing
ISBN (Electronic)9783319110417, 9783319110417_7
ISBN (Print)9783319110400
Publication statusPublished - 2015

Publication series

NameOutstanding Contributions to Logic
ISSN (Print)2211-2758


  • Intuitionistic logic
  • Minimal logic
  • Sequent calculus
  • Natural deduction
  • Cut-elimination
  • Substitution
  • Normalisation


Dive into the research topics of 'Cut-elimination, substitution and normalisation'. Together they form a unique fingerprint.

Cite this