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.

Canonical formulas for K4. Part III: the finite model property

1997 ◽  
Vol 62 (3) ◽  
pp. 950-975 ◽  
Author(s):  
Michael Zakharyaschev
Keyword(s):  
Sufficient Conditions ◽  
Modal Logics ◽  
Point Of View ◽  
Normal Extension ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Modal Reduction ◽  
Canonical Formulas ◽  
General Frames

This paper, a continuation of the series [22, 24], presents two methods for establishing the finite model property (FMP, for short) of normal modal logics containing K4. The methods are oriented mainly to logics represented by their canonical axioms and yield for such axiomatizations several sufficient conditions of FMP. We use them to obtain solutions to two well known open FMP problems. Namely, we prove that• every normal extension of K4 with modal reduction principles has FMP and• every normal extension of S4 with a formula of one variable has FMP.These results are interesting not only from the technical point of view. Actually, they reveal important properties of a quite natural family of modal logics—formulas of one variable and, in particular, modal reduction principles are typical axioms in modal logic. Unfortunately, the technical apparatus developed in this paper is applicable only to logics with transitive frames, and the situation with FMP of extensions of K by modal reduction principles, even by axioms of the form □np → □mp still remains unclear. I think at present this is one of the major challenges in completeness theory.The language of the canonical formulas, introduced in [22] (I'll refer to that paper as Part I), is a way of describing the “geometry and topology” of formulas' refutation (general) frames by means of some finite refutation patterns.

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.

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.

The decidability of normal K5 logics

1981 ◽  
Vol 46 (2) ◽  
pp. 319-328 ◽  
Author(s):  
Michael C. Nagle
Keyword(s):  
Modal Logic ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Kit Fine ◽  
Normal Modal Logic ◽  
Theoretic Proof ◽  
Normal Logic

The literature on modal logic includes a number of general completeness and decidability results. The work of Schiller Joe Scroggs [5], R.A. Bull [1], Kit Fine [2], and Krister Segerberg [6] provide examples.Scroggs showed that the proper extensions of S5 have the finite model property and are axiomatizable. (Harrop [3] then argued that logics having these properties are decidable.) Bull extended Scroggs' result by showing that the normal extensions of S4.3 have the finite model property. Fine subsequently provided a model-theoretic proof of Bull's result and also proved the axiomatizability of these logics. In a different direction Segerberg proved that every normal logic containing the characteristic axioms of Lewis' systems S4 and S5 is decidable.The present paper is in this tradition. We extend the results of Scroggs and Segerberg by showing that every normal modal logic containing the S5 axiom has the finite model property, is axiomatizable, and thus is decidable.

Canonical formulas for K4. Part II: Cofinal subframe logics

1996 ◽  
Vol 61 (2) ◽  
pp. 421-449 ◽  
Author(s):  
Michael Zakharyaschev
Keyword(s):  
Completeness Theorem ◽  
Modal Logics ◽  
Closed Domain ◽  
Finite Model ◽  
Modal Formula ◽  
Finite Model Property ◽  
Canonical Formulas ◽  
Image Position ◽  
Almost All ◽  
General Frames

This paper is a continuation of Zakharyaschev [25], where the following basic results on modal logics with transitive frames were obtained:• With every finite rooted transitive frame and every set of antichains (which were called closed domains) in two formulas α (, , ⊥) and α(, ) were associated. We called them the canonical and negation free canonical formulas, respectively, and proved the Refutability Criterion characterizing the constitution of their refutation general frames in terms of subreduction (alias partial p-morphism), the cofinality condition and the closed domain condition.• We proved also the Completeness Theorem for the canonical formulas providing us with an algorithm which, given a modal formula φ, returns canonical formulas α(i, i), ⊥), for i = 1,…, n, such thatif φ is negation free then the algorithm instead of α(i, i, ⊥) can use the negation free canonical formulas α(i, i). Thus, every normal modal logic containing K4 can be axiomatized by a set of canonical formulas.In this Part we apply the apparatus of the canonical formulas for establishing a number of results on the decidability, finite model property, elementarity and some other properties of modal logics within the field of K4.Our attention will be focused on the class of logics which can be axiomatized by canonical formulas without closed domains, i.e., on the logics of the formAdapting the terminology of Fine [11], we call them the cofinal subframe logics and denote this class by . As was shown in Part I, almost all standard modal logics are in .

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.

Small substructures and decidability issues for first-order logic with two variables

2012 ◽  
Vol 77 (3) ◽  
pp. 729-765 ◽  
Author(s):  
Emanuel Kieroński ◽  
Martin Otto
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Equivalence Relations ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
Surrounding Structure ◽  
Small Model ◽  
Exponential Size

AbstractWe study first-order logic with two variables FO2 and establish a small substructure property. Similar to the small model property for FO2 we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO2 under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO2 has the finite model property and is complete for non-deterministic exponential time, just as for plain FO2. With two equivalence relations, FO2 does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO2 is undecidable.

Sign in / Sign up

Export Citation Format

Share Document