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.

Explicit Provability and Constructive Semantics

2001 ◽  
Vol 7 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Sergei N. Artemov
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Modal Logics ◽  
Combinatory Logic ◽  
Underlying Structure ◽  
Intuitionistic Propositional Logic ◽  
Intuitionistic Modal Logics

AbstractIn 1933 Gödel introduced a calculus of provability (also known as modal logicS4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logicLPof propositions and proofs and show that Gödel's provability calculus is nothing but the forgetful projection ofLP. This also achieves Gödel's objective of defining intuitionistic propositional logicIntvia classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics forIntwhich resisted formalization since the early 1930s.LPmay be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus.

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 Semantical Proof of Subformula Property for the Modal Logics K 4.3, KD 4.3, and S4.3

2019 ◽  
Vol 48 (4) ◽  
Author(s):  
Daishi Yazaki
Keyword(s):  
Sequent Calculus ◽  
Modal Logics ◽  
Finite Model ◽  
Inference Rules ◽  
Sequent Calculi ◽  
Model Property ◽  
Finite Model Property ◽  
Subformula Property

The main purpose of this paper is to give alternative proofs of syntactical and semantical properties, i.e. the subformula property and the nite model property, of the sequent calculi for the modal logics K4.3, KD4.3, and S4.3. The application of the inference rules is said to be acceptable, if all the formulas in the upper sequents are subformula of the formulas in lower sequent. For some modal logics, Takano analyzed the relationships between the acceptable inference rules and semantical properties by constructing models. By using these relationships, he showed Kripke completeness and subformula property. However, his method is difficult to apply to inference rules for the sequent calculi for K4.3, KD4.3, and S4.3. Lookinglosely at Takano's proof, we nd that his method can be modied to construct nite models based on the sequent calculus for K4.3, if the calculus has (cut) and all the applications of the inference rules are acceptable. Similarly, we can apply our results to the calculi for KD4.3 and S4.3. This leads not only to Kripke completeness and subformula property, but also to finite model property of these logics simultaneously.

scholarly journals The Method of Socratic Proofs Meets Correspondence Analysis

2019 ◽  
Vol 48 (2) ◽  
pp. 99-116
Author(s):  
Dorota Leszczyńska-Jasion ◽  
Yaroslav Petrukhin ◽  
Vasilyi Shangin
Keyword(s):  
Correspondence Analysis ◽  
Boolean Functions ◽  
Propositional Logic ◽  
Sequent Calculus ◽  
Sequent Calculi ◽  
Classical Propositional Logic ◽  
Logic Of Questions ◽  
Proof Systems

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic (i.e. pertaining to the logic of questions) calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for the method of Socratic proofs. Correspondence analysis is Kooi and Tamminga's technique for designing proof systems. In this paper it is used to consider sequent calculi with non-branching (the only exception being the rule of cut), invertible rules for the negation fragment of classical propositional logic and its extensions by binary Boolean functions.

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 Proof theory for quantified monotone modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 478-506
Author(s):  
Sara Negri ◽  
Eugenio Orlandelli
Keyword(s):  
Proof Theory ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Completeness Proof ◽  
First Order ◽  
Constant Domains ◽  
Normal Modal Logics ◽  
Order Extension

Abstract This paper provides a proof-theoretic study of quantified non-normal modal logics (NNML). It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut.

Sign in / Sign up

Export Citation Format

Share Document