Skip to content

Research at St Andrews

A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–McKinsey–Tarski embedding

Research output: Contribution to journalArticle

DOI

Abstract

It is well-known that intuitionistic propositional logic Int may be faithfully embedded not just into the modal logic S4 but also into the provability logics GL and Grz of Gödel-Löb and Grzegorczyk, and also that there is a similar embedding of Grz into GL. Known proofs of these faithfulness results are short but model-theoretic and thus non-constructive. Here a labelled sequent system Grz for Grzegorczyk logic is presented and shown to be complete and therefore closed with respect to Cut. The completeness proof, being constructive, yields a constructive decision procedure, i.e. both a proof procedure for derivable sequents and a countermodel construction for underivable sequents. As an application, a constructive proof of the faithfulness of the embedding of Int into Grz and hence a constructive decision procedure for Int are obtained.

Close

Details

Original languageEnglish
JournalJournal of Logic and Computation
Early online date18 Jul 2013
DOIs
StatePublished - 2013

    Research areas

  • Sequent calculus, Modal logic, Provability logic, Grzegorczyk logic, Intuitionistic logic, Decision procedures, Labelled deduction

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

Related by journal

  1. Prefix probabilities for linear context-free rewriting systems

    Nederhof, M. J. & Satta, G. 2014 In : Journal of Logic and Computation. 24, 2, p. 331-350 33 p.

    Research output: Contribution to journalArticle

  2. Tree Parsing for Tree-Adjoining Machine Translation

    Buechse, M., Vogler, H. & Nederhof, M. J. 2014 In : Journal of Logic and Computation. 24, 2, p. 351-373 23 p.

    Research output: Contribution to journalArticle

  3. Call-by-value λ-calculus and LJQ

    Dyckhoff, R. & Lengrand, S. Dec 2007 In : Journal of Logic and Computation. 17, 6, p. 1109-1134 26 p.

    Research output: Contribution to journalArticle

  4. Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation

    Dyckhoff, R. & Urban, C. Oct 2003 In : Journal of Logic and Computation. 13, 5, p. 689-706 18 p.

    Research output: Contribution to journalArticle

ID: 110577091