Finite Kripke models and predicate logics of provability

1990 ◽  
Vol 55 (3) ◽  
pp. 1090-1098 ◽  
Author(s):  
Sergei Artemov ◽  
Giorgie Dzhaparidze
Keyword(s):  
Modal Logic ◽  
Kripke Model ◽  
Finite Model ◽  
Kripke Models ◽  
Model Property ◽  
Logical Formula ◽  
Finite Model Property ◽  
Modal Predicate Logics ◽  
The One ◽  
Arithmetical Interpretation

AbstractThe paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic:If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that PA ⊬ fR.This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding “the predicate part” as a specific addition to the standard Solovay construction.

scholarly journals Derivational modal logic of real line with difference modality

10.29007/7gcx ◽  
2018 ◽  
Author(s):  
Andrey Kudinov
Keyword(s):  
Modal Logic ◽  
Real Line ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Finite Axiomatization

We study derivational modal logic of real line with difference modality and prove that it has finite model property but does not have finite axiomatization.

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.

scholarly journals NNIL-formulas revisited: Universal models and finite model property

2020 ◽  
Author(s):  
Julia Ilin ◽  
Dick de Jongh ◽  
Fan Yang
Keyword(s):  
Direct Proof ◽  
Finite Model ◽  
Kripke Models ◽  
Model Property ◽  
Finite Model Property ◽  
Universal Models ◽  
Heyting Arithmetic ◽  
First Results

Abstract NNIL-formulas, introduced by Visser in 1983–1984 in a study of $\varSigma _1$-subsitutions in Heyting arithmetic, are intuitionistic propositional formulas that do not allow nesting of implication to the left. The first results about these formulas were obtained in a paper of 1995 by Visser et al. In particular, it was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. Recently, Bezhanishvili and de Jongh observed that NNIL-formulas are also reflected by the colour-preserving monotonic maps of Kripke models. In the present paper, we first show how this observation leads to the conclusion that NNIL-formulas are preserved by arbitrary substructures not necessarily satisfying the topo-subframe condition. Then, we apply it to construct universal models for NNIL. It follows from the properties of these universal models that NNIL-formulas are also exactly the formulas that are reflected by colour-preserving monotonic maps. By using the method developed in constructing the universal models, we give a new direct proof that the logics axiomatized by NNIL-axioms have the finite model property.

An incomplete decidable modal logic

1984 ◽  
Vol 49 (2) ◽  
pp. 520-527 ◽  
Author(s):  
M. J. Cresswell
Keyword(s):  
Modal Logic ◽  
Possible Worlds ◽  
Order Theory ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
General Frame ◽  
Propositional Modal Logic ◽  
Modal Systems ◽  
Modal Propositional Logic

The most common way of proving decidability in propositional modal logic is to shew that the system in question has the finite model property. This is not however the only way. Gabbay in [4] proves the decidability of many modal systems using Rabin's result in [8] on the decidability of the second-order theory of successor functions. In particular [4, pp. 258-265] he is able to prove the decidability of a system which lacks the finite model property. Gabbay's system is however complete, in the sense of being characterized by a class of frames, and the question arises whether there is a decidable modal logic which is not complete. Since no incomplete modal logic has the finite model property [9, p. 33], any proof of decidability must employ some such method as Gabbay's. In this paper I use the Gabbay/Rabin technique to prove the decidability of a finitely axiomatized normal modal propositional logic which is not characterized by any class of frames. I am grateful to the referee for suggesting improvements in substance and presentation.The terminology I am using is standard in modal logic. By a frame is understood a pair 〈W, R〉 in which W is a class (of “possible worlds”) and R ⊆ W2. To avoid confusion in what follows, a frame will henceforth be referred to as a Kripke frame. By contrast, a general frame is a pair 〈, Π〉 in which is a Kripke frame and Π is a collection of subsets of W closed under the Boolean operations and satisfying the condition that if A is in Π then so is R−1 “A. A model on a frame (of either kind) is obtained by adding a function V which assigns sets of worlds to propositional variables. In the case of a general frame we require that V(p) ∈ Π.

A Modal Logic for Similarity Relations in Pawlak Knowledge Representation Systems

1991 ◽  
Vol 15 (1) ◽  
pp. 61-79
Author(s):  
Dimiter Vakarelov
Keyword(s):  
Modal Logic ◽  
Knowledge Representation ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
Similarity Relations ◽  
Representation Systems ◽  
Knowledge Representation Systems

One of the main results of the paper is a characterization of certain kind similarity relations in Pawlak knowledge representation systems by means of first order sentences. As an application we obtain a complete finite axiomatization of the corresponding poly modal logic, called in the paper MLSim. It is proved that MLSim possesses finite model property and is decidable.

scholarly journals STABLE CANONICAL RULES

2016 ◽  
Vol 81 (1) ◽  
pp. 284-315 ◽  
Author(s):  
GURAM BEZHANISHVILI ◽  
NICK BEZHANISHVILI ◽  
ROSALIE IEMHOFF
Keyword(s):  
Modal Logic ◽  
Finite Model ◽  
Consequence Relations ◽  
Model Property ◽  
Consequence Relation ◽  
Finite Model Property ◽  
Normal Modal Logic

AbstractWe introduce stable canonical rules and prove that each normal modal multi-conclusion consequence relation is axiomatizable by stable canonical rules. We apply these results to construct finite refutation patterns for modal formulas, and prove that each normal modal logic is axiomatizable by stable canonical rules. We also define stable multi-conclusion consequence relations and stable logics and prove that these systems have the finite model property. We conclude the paper with a number of examples of stable and nonstable systems, and show how to axiomatize them.

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

10.29007/vgh2 ◽  
2018 ◽  
Author(s):  
Xavier Caicedo ◽  
George Metcalfe ◽  
Ricardo Rodriguez ◽  
Jonas Rogger
Keyword(s):  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
Gödel Logic ◽  
Np Completeness ◽  
Kripke Frames ◽  
The One

A new semantics with the finite model property is provided and used to establish decidability for Gödel modal logics based on (crisp or fuzzy) Kripke frames combined locally with Gödel logic. A similar methodology is also used to establish decidability, indeed co-NP-completeness, for a Gödel S5 logic that coincides with the one-variable fragment of first-order Gödel logic.

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.

scholarly journals TOPOLOGICAL COMPLETENESS OF LOGICS ABOVE S4

2015 ◽  
Vol 80 (2) ◽  
pp. 520-566 ◽  
Author(s):  
GURAM BEZHANISHVILI ◽  
DAVID GABELAIA ◽  
JOEL LUCERO-BRYAN
Keyword(s):  
Modal Logic ◽  
Binary Tree ◽  
Finite Model ◽  
Scott Topology ◽  
Model Property ◽  
Topological Semantics ◽  
Finite Model Property ◽  
Normal Modal Logic ◽  
General Frame ◽  
Image Position

AbstractIt is a celebrated result of McKinsey and Tarski [28] that S4 is the logic of the closure algebra Χ+ over any dense-in-itself separable metrizable space. In particular, S4 is the logic of the closure algebra over the reals R, the rationals Q, or the Cantor space C. By [5], each logic above S4 that has the finite model property is the logic of a subalgebra of Q+, as well as the logic of a subalgebra of C+. This is no longer true for R, and the main result of [5] states that each connected logic above S4 with the finite model property is the logic of a subalgebra of the closure algebra R+.In this paper we extend these results to all logics above S4. Namely, for a normal modal logic L, we prove that the following conditions are equivalent: (i) L is above S4, (ii) L is the logic of a subalgebra of Q+, (iii) L is the logic of a subalgebra of C+. We introduce the concept of a well-connected logic above S4 and prove that the following conditions are equivalent: (i) L is a well-connected logic, (ii) L is the logic of a subalgebra of the closure algebra $\xi _2^ + $ over the infinite binary tree, (iii) L is the logic of a subalgebra of the closure algebra ${\bf{L}}_2^ + $ over the infinite binary tree with limits equipped with the Scott topology. Finally, we prove that a logic L above S4 is connected iff L is the logic of a subalgebra of R+, and transfer our results to the setting of intermediate logics.Proving these general completeness results requires new tools. We introduce the countable general frame property (CGFP) and prove that each normal modal logic has the CGFP. We introduce general topological semantics for S4, which generalizes topological semantics the same way general frame semantics generalizes Kripke semantics. We prove that the categories of descriptive frames for S4 and descriptive spaces are isomorphic. It follows that every logic above S4 is complete with respect to the corresponding class of descriptive spaces. We provide several ways of realizing the infinite binary tree with limits, and prove that when equipped with the Scott topology, it is an interior image of both C and R. Finally, we introduce gluing of general spaces and prove that the space obtained by appropriate gluing involving certain quotients of L2 is an interior image of R.

Sign in / Sign up

Export Citation Format

Share Document