Skip to content

Research at St Andrews

Cut-elimination, substitution and normalisation

Research output: Research - peer-reviewChapter (peer-reviewed)

DOI

Open Access permissions

Open

Abstract

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.
Close

Details

Original languageEnglish
Title of host publicationDag Prawitz on Proofs and Meaning
EditorsHeinrich Wansing
PublisherSpringer
Pages163-187
ISBN (Electronic)9783319110417, 9783319110417_7
ISBN (Print)9783319110400
DOIs
StatePublished - 2015

Publication series

NameOutstanding Contributions to Logic
PublisherSpringer
Volume7
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. Analyticity, balance and non-admissibility of Cut in Stoic Logic

    Bobzien, S. & Dyckhoff, R. 20 Apr 2018 In : Studia Logica. First Online, 23 p.

    Research output: Research - peer-reviewArticle

  2. 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: Research - peer-reviewChapter (peer-reviewed)

  3. 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: ResearchConference contribution

  4. 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: Research - peer-reviewChapter (peer-reviewed)

ID: 181526067