A Finite Model Property for Gödel Modal Logics

Mapping Intimacies ◽

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.

Download Full-text

Simulating polyadic modal logics by monadic ones

Journal of Symbolic Logic ◽

10.2178/jsl/1052669058 ◽

2003 ◽

Vol 68 (2) ◽

pp. 419-462 ◽

Cited By ~ 5

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.

Download Full-text

Products of ‘transitive” modal logics

Journal of Symbolic Logic ◽

10.2178/jsl/1122038925 ◽

2005 ◽

Vol 70 (3) ◽

pp. 993-1021 ◽

Cited By ~ 21

Author(s):

D. Gabelaia ◽

A. Kurucz ◽

F. Wolter ◽

M. Zakharyaschev

Keyword(s):

Open Problem ◽

Modal Logics ◽

Finite Model ◽

Model Property ◽

Finite Model Property ◽

Infinite Depth ◽

Kripke Frames ◽

Complete Extension

AbstractWe solve a major open problem concerning algorithmic properties of products of ‘transitive’ modal logics by showing that products and commutators of such standard logics as K4, S4, S4.1, K4.3, GL, or Grz are undecidable and do not have the finite model property. More generally, we prove that no Kripke complete extension of the commutator [K4, K4] with product frames of arbitrary finite or infinite depth (with respect to both accessibility relations) can be decidable. In particular, if l1 and l2 are classes of transitive frames such that their depth cannot be bounded by any fixed n < ω, then the logic of the class {5ℑ1 × ℑ2 ∣ ℑ1 ∈ l1, ℑ2, ∈ l2} is undecidable. (On the contrary, the product of, say, K4 and the logic of all transitive Kripke frames of depth ≤ n, for some fixed n < ω, is decidable.) The complexity of these undecidable logics ranges from r.e. to co-r.e. and Π11-complete. As a consequence, we give the first known examples of Kripke incomplete commutators of Kripke complete logics.

Download Full-text

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

Journal of Symbolic Logic ◽

10.2178/jsl/1344862160 ◽

2012 ◽

Vol 77 (3) ◽

pp. 729-765 ◽

Cited By ~ 11

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.

Download Full-text

Decidability of interpretability logics ILM0 and ILW*

Logic Journal of IGPL ◽

10.1093/jigpal/jzx027 ◽

2017 ◽

Vol 25 (5) ◽

pp. 758-772 ◽

Cited By ~ 1

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.

Download Full-text

A Sufficient Condition for the Finite Model Property of Modal Logics above K4

Logic Journal of IGPL ◽

10.1093/jigpal/1.1.13 ◽

1993 ◽

Vol 1 (1) ◽

pp. 13-21 ◽

Cited By ~ 9

Author(s):

MICHAEL ZAKHARYASCHEV

Keyword(s):

Modal Logics ◽

Finite Model ◽

Sufficient Condition ◽

Model Property ◽

Finite Model Property

Download Full-text

Finite Kripke models and predicate logics of provability

Journal of Symbolic Logic ◽

10.2307/2274475 ◽

1990 ◽

Vol 55 (3) ◽

pp. 1090-1098 ◽

Cited By ~ 5

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.

Download Full-text