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: Research - peer-reviewArticle



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.



Original languageEnglish
JournalJournal of Logic and Computation
Early online date18 Jul 2013
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. 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)

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: Research - peer-reviewArticle

  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: Research - peer-reviewArticle

  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: Research - peer-reviewArticle

  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: Research - peer-reviewArticle

ID: 110577091