NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

DOI10.1017/S1755020319000510zbMATH Open1496.03086arXiv1804.00955OpenAlexW3038517329WikidataQ113857267 ScholiaQ113857267MaRDI QIDQ5001550FDOQ5001550

Daniyar Shamkanov, Yury Savateev

Publication date: 22 July 2021

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1804.00955

zbMATH Keywords

cut-eliminationGrzegorczyk logiccyclic proofsnon-well-founded proofsLyndon interpolation

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Cites Work

• The Banach fixed point theorem for ultrametric spaces
• A Fixed Point Theorem in Non-Archimedean Vector Spaces
• The Lyndon property and uniform interpolation over the Grzegorczyk logic
• An introduction to metric semantics: Operational and denotational models for programming and specification languages
• Circular proofs for the Gödel-Löb provability logic
• On modal systems having arithmetical interpretations
• A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding
• Denotational semantics in the cpo and metric approach
• On the Proof Theory of the Modal Logic Grz
• The Lambek calculus with iteration: two variants
• Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
• Cyclic Arithmetic Is Equivalent to Peano Arithmetic
• Reasoning in circles
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (4)

• Title not available (Why is that?)
• A Sound Interpretation of Leśniewski's Epsilon in Modal Logic KTB
• Abstract cyclic proofs
• Abstract cyclic proofs

Recommendations

• Title not available (Why is that?) 👍 👎
• Euclidean hierarchy in modal logic 👍 👎
• The undecidability of the disjunction property of propositional logics and other related problems 👍 👎
• On the Proof Theory of the Modal Logic Grz 👍 👎
• Cut-elimination theorems for some infinitary modal logics 👍 👎
• The disjunction property and Church's thesis in arithmetic with Grzegorczyk logic 👍 👎
• Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs 👍 👎
• On the proof theory of infinitary modal logic 👍 👎
• Cut elimination for the weak modal Grzegorczyk logic via non-well-founded proofs 👍 👎
• Representing any-time and program-iteration by infinitary conjunction 👍 👎

This page was built for publication: NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5001550)