Skip to content

Research at St Andrews

Some remarks on proof-theoretic semantics

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

DOI

Open Access permissions

Open

Abstract

This is a tripartite work. The first part is a brief discussion of what it is to be a logical constant, rejecting a view that allows a particular self-referential “constant” • to be such a thing in favour of a view that leads to strong normalisation results. The second part is a commentary on the flattened version of Modus Ponens, and its relationship with rules of type theory. The third part is a commentary on work (joint with Nissim Francez) on “general elimination rules” and harmony, with a retraction of one of the main ideas of that work, i.e. the use of “flattened” general elimination rules for situations with discharge of assumptions. We begin with some general background on general elimination rules.
Close

Details

Original languageEnglish
Title of host publicationAdvances in Proof-Theoretic Semantics
EditorsThomas Piecha, Peter Schroeder-Heister
PublisherSpringer
Pages79-93
Number of pages15
ISBN (Electronic)9783319226866
ISBN (Print)9783319226859
DOIs
StatePublished - 2016
EventSecond Conference on Proof-Theoretic Semantics - Tübingen, Germany

Publication series

NameTrends in Logic
Volume43
ISSN (Print)1572-6126

Conference

ConferenceSecond Conference on Proof-Theoretic Semantics
CountryGermany
CityTübingen
Period8/03/1310/03/13

    Research areas

  • General elimination rules, Harmony, Strong 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. 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

  4. Cut-elimination, substitution and normalisation

    Dyckhoff, R. 2015 Dag Prawitz on Proofs and Meaning. Wansing, H. (ed.). Springer, p. 163-187 (Outstanding Contributions to Logic; vol. 7)

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

  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: 181527166