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 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 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 .

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.

Decidability of interpretability logics ILM0 and ILW*

2017 ◽  
Vol 25 (5) ◽  
pp. 758-772 ◽  
Author(s):  
Luka Mikec ◽  
Tin Perkov ◽  
Mladen Vuković
Keyword(s):  
Open Problem ◽  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Filtration Method ◽  
Finite Model Property ◽  
Missing Link ◽  
Interpretability Logic

Abstract The finite model property is a key step in proving decidability of modal logics. By adapting the filtration method to the generalized Veltman semantics for interpretability logics, we have been able to prove the finite model property of interpretability logic ILM0 w.r.t. generalized Veltman models. We use the same technique to prove the finite model property of interpretability logic ILW* w.r.t. generalized Veltman models. The missing link needed to prove the decidability of ILM0 was completeness w.r.t. generalized Veltman models, which we obtain in this article. Thus, we prove the decidability of ILM0, which was an open problem. Using the same technique, we prove that ILW* is also decidable.

Simulating polyadic modal logics by monadic ones

2003 ◽  
Vol 68 (2) ◽  
pp. 419-462 ◽  
Author(s):  
George Goguadze ◽  
Carla Piazza ◽  
Yde Venema
Keyword(s):  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
First Order Definability

AbstractWe define an interpretation of modal languages with polyadic operators in modal languages that use monadic operators (diamonds) only. We also define a simulation operator which associates a logic Λsim in the diamond language with each logic Λ in the language with polyadic modal connectives. We prove that this simulation operator transfers several useful properties of modal logics, such as finite/recursive axiomatizability, frame completeness and the finite model property, canonicity and first-order definability.

scholarly journals A Finite Model Property for Gödel Modal Logics

2013 ◽  
pp. 226-237 ◽  
Author(s):  
Xavier Caicedo ◽  
George Metcalfe ◽  
Ricardo Rodríguez ◽  
Jonas Rogger
Keyword(s):  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property

The finite model property in tense logic

1995 ◽  
Vol 60 (3) ◽  
pp. 757-774 ◽  
Author(s):  
Frank Wolter
Keyword(s):  
Modal Logics ◽  
Tense Logic ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Negative Results ◽  
Propositional Language ◽  
Positive Results

AbstractTense logics in the bimodal propositional language are investigated with respect to the Finite Model Property. In order to prove positive results techniques from investigations of modal logics above K4 are extended to tense logic. General negative results show the limits of the transfer.

Sign in / Sign up

Export Citation Format

Share Document