Skip to content

Research at St Andrews

Cut-elimination, substitution and normalisation

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


Open Access permissions



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
StatePublished - 2015

Publication series

NameOutstanding Contributions to Logic
ISSN (Print)2211-2758

    Research areas

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Intuitionistic decision procedures since Gentzen

    Dyckhoff, R. 5 May 2016 Advances in Proof Theory. Kahle, R., Strahm, T. & Studer, T. (eds.). Birkhäuser Basel, p. 245-267 (Progress in Computer Science and Applied Logic; vol. 28)

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

  2. POSIX lexing with derivatives of regular expressions (proof pearl)

    Ausaf, F., Dyckhoff, R. & Urban, C. 2016 Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Blanchette, J. C. & Merz, S. (eds.). Springer, p. 69-86 18 p. (Lecture Notes in Computer Science; vol. 9807)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  3. Some remarks on proof-theoretic semantics

    Dyckhoff, R. 2016 Advances in Proof-Theoretic Semantics. Piecha, T. & Schroeder-Heister, P. (eds.). Springer, p. 79-93 15 p. (Trends in Logic; vol. 43)

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

  4. Geometrisation of first-order logic

    Dyckhoff, R. & Negri, S. Jun 2015 In : Bulletin of Symbolic Logic. 21, 2, p. 123–163 41 p.

    Research output: Contribution to journalArticle

  5. Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators

    Dyckhoff, R., Sadrzadeh, M. & Truffaut, J. Nov 2013 In : ACM Transactions on Computational Logic. 14, 4, 38 p., 34

    Research output: Contribution to journalArticle

ID: 181526067