scholarly journals From free algebras to proof bounds

10.29007/md5x ◽  
2018 ◽  
Author(s):  
Silvio Ghilardi
Keyword(s):  
Search Space ◽  
Correspondence Theory ◽  
Finite Model ◽  
Free Algebras ◽  
Joint Work ◽  
Finite Model Property ◽  
Classical Correspondence ◽  
Morphic Image ◽  
Specific Rule ◽  
Subformula Property

(This is joint work with Nick Bezhanishvili).In the first part of our contribution, we review and compare existing constructions of finitely generated free algebras in modal logic focusing on step-by-step methods. We discuss the notions of step algebras and step frames arising from recent investigations, as well as the role played by finite duality.In the second part of the contribution, we exploit the potential of step frames for investigating proof-theoretic aspects. This includes developing a method which detects when a specific rule-based calculus Ax axiomatizing a given logic L has the so-called bounded proof property. This property is a kind of an analytic subformula property limiting the proof search space. We prove that every finite conservative step frame for Ax is a p-morphic image of a finite Kripke frame for L iff Ax has the bounded proof property and L has the finite model property. This result, combined with a `step version' of the classical correspondence theory turns out to be quite powerful in applications.

Canonical formulas for K4. Part I: Basic results

1992 ◽  
Vol 57 (4) ◽  
pp. 1377-1402 ◽  
Author(s):  
Michael Zakharyaschev
Keyword(s):  
Fundamental Result ◽  
Normal Extension ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Canonical Formulas ◽  
Morphic Image ◽  
Normal Logic ◽  
A New Technique ◽  
Almost All

This paper presents a new technique for handling modal logics with transitive frames, i.e. extensions of the modal system K4. In effect, the technique is based on the following fundamental result, to be obtained below in §3.Given a formula φ, we can effectively construct finite frames 1, …, n which completely characterize the set of all transitive general frames refuting φ. More exactly, an arbitrary general frame refutes φ iff contains a (not necessarily generated) subframe such that (1) i, for some i ϵ {1, …, n}, is a p-morphic image of (after Fine [1985] we say is subreducible to i), (2) is cofinal in , and (3) every point in that is not in does not get into “closed domains” which are uniquely determined in i, by φ.This purely technical result has, as it turns out, rather unexpected and profound consequences. For instance, it follows at once that if φ determines no closed domains in the frames 1, …, n associated with it, then the normal extension of K4 generated by φ has the finite model property and so is decidable. Moreover, every normal logic axiomatizable by any (even infinite) set of such formulas φ also has the finite model property. This observation would not possibly merit any special attention, were it not for the fact that the class of such logics contains almost all the standard systems within the field of K4 (at least all those mentioned by Segerberg [1971] or Bull and Segerberg [1984]), all logics containing S4.3, all subframe logics of Fine [1985], and a continuum of other logics as well.

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.

Logics containing K4. Part II

1985 ◽  
Vol 50 (3) ◽  
pp. 619-651 ◽  
Author(s):  
Kit Fine
Keyword(s):  
General Result ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Completeness Result ◽  
Morphic Image ◽  
Elementary Condition

This paper establishes another very general completeness result for the logics within the field of K4. With each finite transitive frame ℭ we may associate a formula — Bℭ which validates just those frames ℑ in which ℭ is not in a certain sense embeddable (to be exact, ℭ is not the p-morphic image of any subframe of ℑ. By a subframe logic we mean the result of adding such formulas as axioms to K4. The general result is that each subframe logic has the finite model property.There are a continuum of subframe logics and they include many of the standard ones, such as T, S4, S4.3, S5 and G. It turns out that the subframe logics are exactly those complete for a condition that is closed under subframes (any subframe of a frame satisfying the condition also satisfies the condition). As a consequence, every logic complete for a condition closed under subframes has the finite model property.It is ascertained which of the subframe logics are compact. It turns out that the compact logics are just those whose axioms express an elementary condition. Tests are given for determining whether a given axiom expresses an elementary condition and for determining what it is in case it does.In one respect the present general completeness result differs from most of the others in the literature. The others have usually either been what one might call logic based or formula based. They have usually either been to the effect that all of the logics containing a given logic are complete or to the effect that all logics whose axioms come from a given syntactically characterized class of formulas are complete. The present result is, by contrast, what one might call frame based. The axioms of the logics to be proved complete are characterized most directly in terms of their connection with certain frames.

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 A Modified Subformula Property for the Modal Logic S4.2

2019 ◽  
Vol 48 (1) ◽  
Author(s):  
Mitio Takano
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Interpolation Property ◽  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Cut Rule ◽  
Finite Model Property ◽  
Axiom A ◽  
Subformula Property

The modal logic S4.2 is S4 with the additional axiom ◊□A ⊃ □◊A. In this article, the sequent calculus GS4.2 for this logic is presented, and by imposing an appropriate restriction on the application of the cut-rule, it is shown that, every GS4.2-provable sequent S has a GS4.2-proof such that every formula occurring in it is either a subformula of some formula in S, or the formula □¬□B or ¬□B, where □B occurs in the scope of some occurrence of □ in some formula of S. These are just the K5-subformulas of some formula in S which were introduced by us to show the modied subformula property for the modal logics K5 and K5D (Bull Sect Logic 30(2): 115–122, 2001). Some corollaries including the interpolation property for S4.2 follow from this. By slightly modifying the proof, the finite model property also follows.

Canonical rules

2009 ◽  
Vol 74 (4) ◽  
pp. 1171-1205 ◽  
Author(s):  
Emil Jeřábek
Keyword(s):  
Alternative Proof ◽  
Finite Model ◽  
Consequence Relations ◽  
Model Property ◽  
Finite Model Property ◽  
Admissible Rules ◽  
Superintuitionistic Logics ◽  
Canonical Formulas ◽  
Global Consequence

AbstractWe develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (unitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property.

On the Modal μ-Calculus Over Finite Symmetric Graphs

2015 ◽  
Vol 65 (4) ◽  
Author(s):  
Giovanna D’Agostino ◽  
Giacomo Lenzi
Keyword(s):  
Lower Bound ◽  
Upper Bound ◽  
Satisfiability Problem ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Symmetric Graphs ◽  
Trivial Consequence

AbstractIn this paper we consider the alternation hierarchy of the modal μ-calculus over finite symmetric graphs and show that in this class the hierarchy is infinite. The μ-calculus over the symmetric class does not enjoy the finite model property, hence this result is not a trivial consequence of the strictness of the hierarchy over symmetric graphs. We also find a lower bound and an upper bound for the satisfiability problem of the μ-calculus over finite symmetric graphs.

On simple, weak and strong models of propositional calculi

1973 ◽  
Vol 74 (1) ◽  
pp. 1-9 ◽  
Author(s):  
Ronald Harrop
Keyword(s):  
Simple Model ◽  
Propositional Calculus ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Finite Structure ◽  
Propositional Calculi ◽  
Simple Models

In this paper we will be concerned primarily with weak, strong and simple models of a propositional calculus, simple models being structures of a certain type in which all provable formulae of the calculus are valid. It is shown that the finite model property defined in terms of simple models holds for all calculi. This leads to a new proof of the fact that there is no general effective method for testing, given a finite structure and a calculus, whether or not the structure is a simple model of the calculus.

scholarly journals On the Decidability of Intuitionistic Tense Logic without Disjunction

2020 ◽  
Author(s):  
Fei Liang ◽  
Zhe Lin
Keyword(s):  
Proof Theory ◽  
Tense Logic ◽  
Heyting Algebras ◽  
Finite Model ◽  
Algebraic Proof ◽  
Model Property ◽  
Algebraic Models ◽  
Finite Axiomatizability ◽  
Finite Model Property ◽  
Modal Operators

Implicative semi-lattices (also known as Brouwerian semi-lattices) are a generalization of Heyting algebras, and have been already well studied both from a logical and an algebraic perspective. In this paper, we consider the variety ISt of the expansions of implicative semi-lattices with tense modal operators, which are algebraic models of the disjunction-free fragment of intuitionistic tense logic. Using methods from algebraic proof theory, we show that the logic of tense implicative semi-lattices has the finite model property. Combining with the finite axiomatizability of the logic, it follows that the logic is decidable.

Sign in / Sign up

Export Citation Format

Share Document