NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

Yury Savateev; Daniyar Shamkanov

doi:10.1017/S1755020319000510

NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

Yury Savateev, Daniyar Shamkanov

Research output: Contribution to journal › Article › peer-review

10 Citations (Scopus)

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 language	English
Pages (from-to)	22-50
Journal	The Review of Symbolic Logic (RSL)
Volume	14
Issue number	1
DOIs	https://doi.org/10.1017/S1755020319000510
Publication status	Published - 29 Jun 2020
Externally published	Yes

Keywords

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

Access to Document

10.1017/S1755020319000510

Cite this

@article{4e2038c3d5644759a50a67ae75b6cf33,

title = "NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC",

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.",

keywords = "non-well-founded proofs, Grzegorczyk logic, cut-elimination, Lyndon interpolation, cyclic proofs",

author = "Yury Savateev and Daniyar Shamkanov",

year = "2020",

month = jun,

day = "29",

doi = "10.1017/S1755020319000510",

language = "English",

volume = "14",

pages = "22--50",

journal = "The Review of Symbolic Logic (RSL)",

issn = "1755-0203",

publisher = "Cambridge University Press",

number = "1",

}

TY - JOUR

T1 - NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

AU - Savateev, Yury

AU - Shamkanov, Daniyar

PY - 2020/6/29

Y1 - 2020/6/29

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

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

KW - non-well-founded proofs

KW - Grzegorczyk logic

KW - cut-elimination

KW - Lyndon interpolation

KW - cyclic proofs

U2 - 10.1017/S1755020319000510

DO - 10.1017/S1755020319000510

M3 - Article

SN - 1755-0203

VL - 14

SP - 22

EP - 50

JO - The Review of Symbolic Logic (RSL)

JF - The Review of Symbolic Logic (RSL)

IS - 1

ER -

NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

Abstract

Keywords

Access to Document

Fingerprint

Cite this