Skip to content

Research at St Andrews

Cut-elimination, substitution and normalisation

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

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
Publication statusPublished - 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. Contraction-free sequent calculi in intuitionistic logic: a correction

    Dyckhoff, R., Dec 2018, In : Journal of Symbolic Logic. 83, 4, p. 1680-1682 3 p.

    Research output: Contribution to journalArticle

  2. Indefinite proof and inversions of syllogisms

    Dyckhoff, R., 14 Jul 2018, (Accepted/In press) In : Bulletin of Symbolic Logic. 13 p.

    Research output: Contribution to journalArticle

  3. 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: Contribution to journalArticle

  4. 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)

ID: 181526067