NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

Yury Savateev, Daniyar Shamkanov

Research output: Contribution to journalArticlepeer-review

Abstract

We present a sequent calculus for the Grzegorczyk modal logic Grz allowing cyclic and other non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs. As an application, we establish the Lyndon interpolation property for the logic Grz proof-theoretically.
Original languageEnglish
Pages (from-to)22-50
JournalThe Review of Symbolic logic
Volume14
Issue number1
DOIs
Publication statusPublished - 29 Jun 2020
Externally publishedYes

Keywords

  • non-well-founded proofs
  • Grzegorczyk logic
  • cut-elimination
  • Lyndon interpolation
  • cyclic proofs

Fingerprint

Dive into the research topics of 'NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC'. Together they form a unique fingerprint.

Cite this