From the subformula property to cut-admissibility in propositional sequent calculi

Ori Lahav; Yoni Zohar

doi:10.1093/logcom/exy018

Gentzen sequent calculi for some intuitionistic modal logics

Logic Journal of IGPL ◽

10.1093/jigpal/jzz020 ◽

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.

Download Full-text

Contraction-free sequent calculi for intuitionistic logic

Journal of Symbolic Logic ◽

10.2307/2275431 ◽

1992 ◽

Vol 57 (3) ◽

pp. 795-807 ◽

Cited By ~ 151

Author(s):

Roy Dyckhoff

Keyword(s):

Sequent Calculus ◽

Main Idea ◽

Simple Algorithm ◽

Propositional Calculus ◽

Search Tree ◽

Sequent Calculi ◽

Proof Search ◽

Intuitionistic Propositional Calculus ◽

Effective Decision ◽

Subformula Property

Gentzen's sequent calculus LJ, and its variants such as G3 [21], are (as is well known) convenient as a basis for automating proof search for IPC (intuitionistic propositional calculus). But a problem arises: that of detecting loops, arising from the use (in reverse) of the rule ⊃⇒ for implication introduction on the left. We describe below an equivalent calculus, yet another variant on these systems, where the problem no longer arises: this gives a simple but effective decision procedure for IPC.The underlying method can be traced back forty years to Vorob′ev [33], [34]. It has been rediscovered recently by several authors (the present author in August 1990, Hudelmaier [18], [19], Paulson [27], and Lincoln et al. [23]). Since the main idea is not plainly apparent in Vorob′ev's work, and there are mathematical applications [28], it is desirable to have a simple proof. We present such a proof, exploiting the Dershowtiz-Manna theorem [4] on multiset orderings.Consider the task of constructing proofs in Gentzen's sequent calculus LJ of intuitionistic sequents Γ⇒ G, where Γ is a set of assumption formulae and G is a formula (in the language of zero-order logic, using the nullary constant f [absurdity], the unary constant ¬ [negation, with ¬A =defA ⊃ f] and the binary constants &, ∨, and ⊃ [conjunction, disjunction, and implication respectively]). By the Hauptsatz [15], there is an apparently simple algorithm which breaks up the sequent, growing the proof tree until one reaches axioms (of the form Γ⇒ A where A is in Γ), or can make no further progress and must backtrack or even abandon the search. (Gentzen's argument in fact was to use the subformula property derived from the Hauptsatz to limit the size of the search tree. Došen [5] improves on this argument.)

Download Full-text

Semantical Proof of Subformula Property for the Modal Logics K 4.3, KD 4.3, and S4.3

Bulletin of the Section of Logic ◽

10.18778/0138-0680.48.4.01 ◽

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.

Download Full-text