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

ID: 181526067

Top