Semantical Approach to Cut Elimination and Subformula Property in Modal Logic

2015 ◽  
pp. 1-15 ◽  
Author(s):  
Hiroakira Ono
Keyword(s):  
Modal Logic ◽  
Cut Elimination ◽  
Subformula Property

A cut-free Gentzen-type system for the modal logic S5

1980 ◽  
Vol 45 (1) ◽  
pp. 67-84 ◽  
Author(s):  
Masahiko Sato
Keyword(s):  
Modal Logic ◽  
Natural Number ◽  
Decision Procedure ◽  
Type System ◽  
Point Of View ◽  
Usual Sense ◽  
Cut Elimination ◽  
Strict Sense ◽  
Theoretic Point ◽  
Subformula Property

The modal logic S5 has been formulated in Gentzen-style by several authors such as Ohnishi and Matsumoto [4], Kanger [2], Mints [3] and Sato [5]. The system by Ohnishi and Matsumoto is natural, but the cut-elimination theorem in it fails to hold. Kanger's system enjoys cut-elimination theorem, but, strictly speaking, it is not a Gentzen-type system since each formula in a sequent is indexed by a natural number. The system S5+ of Mints is also cut-free, and its cut-elimination theorem is proved constructively via the cut-elimination theorem of Gentzen's LK. However, one of his rules does not have the so-called subformula property, which is desirable from the proof-theoretic point of view. Our system in [5] also enjoys the cut-elimination theorem. However, it is also not a Gentzen-type system in the strict sense, since each sequent in this system consists of a pair of sequents in the usual sense.In the present paper, we give a Gentzen-type system for S5 and prove the cut-elimination theorem in a constructive way. A decision procedure for S5 can be obtained as a by-product.The author wishes to thank the referee for pointing out some errors in the first version of the paper as well as for his suggestions which improved the readability of the paper.

Gentzen sequent calculi for some intuitionistic modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 596-623
Author(s):  
Zhe Lin ◽  
Minghui Ma
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Intuitionistic Propositional Logic ◽  
Propositional Language ◽  
Intuitionistic Modal Logics ◽  
Subformula Property ◽  
Gentzen Sequent Calculus

Abstract Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond ,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond ,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS

2019 ◽  
Vol 13 (4) ◽  
pp. 720-747
Author(s):  
SERGEY DROBYSHEVICH ◽  
HEINRICH WANSING
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Axiom System ◽  
Modal Logics ◽  
Cut Elimination ◽  
Proof Systems ◽  
Image Position ◽  
Axiomatic Extension

AbstractWe present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing (2010) and Odintsov & Wansing (2017), as well as the modal logic KN4 with strong implication introduced in Goble (2006). In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown.

Gentzen's Proof Systems: Byproducts in a Work of Genius

2012 ◽  
Vol 18 (3) ◽  
pp. 313-367 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Central Component ◽  
Cut Elimination ◽  
Complete Class ◽  
Tree Form ◽  
Proof Systems ◽  
Set Up ◽  
Logical Calculi ◽  
Subformula Property

AbstractGentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934–35. The calculus has half rules, half “groundsequents,” and does not allow full cut elimination. Nevertheless, a translation from LI to LIG in the published thesis gives a subformula property for a complete class of derivations in LIG. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus.

scholarly journals New New Modification of the Subformula Property for a Modal Logic

2020 ◽  
Author(s):  
Mitio Takano
Keyword(s):  
Modal Logic ◽  
Natural Extension ◽  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Additional Axiom ◽  
Subformula Property

A modified subformula property for the modal logic KD with the additional axiom $\Box\Diamond(A\vee B)\supset\Box\Diamond A\vee\Box\Diamond B$ is shown. A new modification of the notion of subformula is proposed for this purpose. This modification forms a natural extension of our former one on which modified subformula property for the modal logics K5, K5D and S4.2 has been shown (Bull Sect Logic 30:115--122, 2001 and 48:19--28, 2019). The finite model property as well as decidability for the logic follows from this.

scholarly journals THE LOGIC OF RESOURCES AND CAPABILITIES

2018 ◽  
Vol 11 (2) ◽  
pp. 371-410 ◽  
Author(s):  
MARTA BÍLKOVÁ ◽  
GIUSEPPE GRECO ◽  
ALESSANDRA PALMIGIANO ◽  
APOSTOLOS TZIMOULIS ◽  
NACHOEM WIJNBERG
Keyword(s):  
Algebraic Theory ◽  
Cut Elimination ◽  
Disjunction Property ◽  
Resources And Capabilities ◽  
The One ◽  
Key Aspects ◽  
Planning Problems ◽  
Mutually Independent ◽  
Structural Proof Theory ◽  
Subformula Property

AbstractWe introduce the logic LRC, designed to describe and reason about agents’ abilities and capabilities in using resources. The proposed framework bridges two—up to now—mutually independent strands of literature: the one on logics of abilities and capabilities, developed within the theory of agency, and the one on logics of resources, motivated by program semantics. The logic LRC is suitable to describe and reason about key aspects of social behaviour in organizations. We prove a number of properties enjoyed by LRC (soundness, completeness, canonicity, and disjunction property) and its associated analytic calculus (conservativity, cut elimination, and subformula property). These results lay at the intersection of the algebraic theory of unified correspondence and the theory of multitype calculi in structural proof theory. Case studies are discussed which showcase several ways in which this framework can be extended and enriched while retaining its basic properties, so as to model an array of issues, both practically and theoretically relevant, spanning from planning problems to the logical foundations of the theory of organizations.

scholarly journals Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic

Studia Logica ◽  
2021 ◽  
Author(s):  
Martín Figallo
Keyword(s):  
Modal Logic ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
The Other ◽  
Cut Elimination ◽  
Modal Algebras ◽  
General Method

AbstractThe tetravalent modal logic ($${\mathcal {TML}}$$ TML ) is one of the two logics defined by Font and Rius (J Symb Log 65(2):481–518, 2000) (the other is the normal tetravalent modal logic$${{\mathcal {TML}}}^N$$ TML N ) in connection with Monteiro’s tetravalent modal algebras. These logics are expansions of the well-known Belnap–Dunn’s four-valued logic that combine a many-valued character (tetravalence) with a modal character. In fact, $${\mathcal {TML}}$$ TML is the logic that preserves degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $${\mathcal {TML}}$$ TML and the algebras is not so good as in $${{\mathcal {TML}}}^N$$ TML N , but, as a compensation, it has a better proof-theoretic behavior, since it has a strongly adequate Gentzen calculus (see Font and Rius in J Symb Log 65(2):481–518, 2000). In this work, we prove that the sequent calculus given by Font and Rius does not enjoy the cut-elimination property. Then, using a general method proposed by Avron et al. (Log Univ 1:41–69, 2006), we provide a sequent calculus for $${\mathcal {TML}}$$ TML with the cut-elimination property. Finally, inspired by the latter, we present a natural deduction system, sound and complete with respect to the tetravalent modal logic.

Subformula property in many-valued modal logics

1994 ◽  
Vol 59 (4) ◽  
pp. 1263-1273 ◽  
Author(s):  
Mitio Takano
Keyword(s):  
Sequent Calculus ◽  
Kripke Model ◽  
Modal Logics ◽  
Cut Elimination ◽  
Accessibility Relation ◽  
Cut Rule ◽  
Modal Model ◽  
The Many ◽  
Fitting In ◽  
Subformula Property

Fitting, in [1] and [2], investigated two families of many-valued modal logics. The first, which is somewhat familiar in the literature, is that of the logics characterized using a many-valued version of the Kripke model (binary modal model in his terminology) with a two-valued accessibility relation. On the other hand, those logics which are characterized using another many-valued version of the Kripke model (implicational modal model), with a many-valued accessibility relation, form the second family. Although he gave a sequent calculus for each of these logics, it is far from having the cut-elimination property (CEP) or the subformula property. So we will give a substitute for his system enjoying the subformula property, though it is not of ordinary sequent calculus but of the many-valued version of sequent calculus initiated by Takahashi [7] and Rousseau [3].The author, unaware of the deduction systems with CEP, had given in [8] and [9], after Rousseau [4], the deduction systems for the intuitionistic many-valued logics which enjoy CEP only for a certain restricted class of proofs. Then in [10], he gave for three-valued modal logics the ones with CEP, but these systems have a rule of inference which is unnecessary if the Cut rule is present. Why are we particular about CEP? The author's answer is that a cut-free proof is easy to examine since it is composed solely of subformulas of the formulas which form its conclusion. In this direction, the author has given, for modal logics with the Brouwerian axiom [11], the ones without CEP which nevertheless enjoy the subformula property. This paper is a sequel to the study in [11].

scholarly journals A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs

2016 ◽  
Vol 45 (1) ◽  
Author(s):  
George Tourlakis
Keyword(s):  
Cut Elimination ◽  
Disjunction Property ◽  
Axiom Schema ◽  
First Order ◽  
Kripke Structures ◽  
Order Extension ◽  
Subformula Property

Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations.  In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complexproofs in [2,8]).

scholarly journals NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

2020 ◽  
pp. 1-29
Author(s):  
YURY SAVATEEV ◽  
DANIYAR SHAMKANOV
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Interpolation Property ◽  
Cut Elimination

Abstract We present a sequent calculus for the Grzegorczyk modal logic $\mathsf {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 $\mathsf {Grz}$ proof-theoretically.

Sign in / Sign up

Export Citation Format

Share Document