Bimodal logics for extensions of arithmetical theories

1996 ◽  
Vol 61 (1) ◽  
pp. 91-124 ◽  
Author(s):  
Lev D. Beklemishev
Keyword(s):  
Decision Procedures ◽  
Modal Logics ◽  
Kripke Semantics ◽  
Recursively Enumerable ◽  
Propositional Constants ◽  
Bimodal Logics ◽  
Natural Classes

AbstractWe characterize the bimodal provability logics for certain natural (classes of) pairs of recursively enumerable theories, mostly related to fragments of arithmetic. For example, we shall give axiomatizations, decision procedures, and introduce natural Kripke semantics for the provability logics of (IΔ0 + EXP, PRA); (PRA, IΣn); (IΣm, IΣn) for 1 ≤ m < n; (PA, ACA0); (ZFC, ZFC + CH); (ZFC, ZFC + ¬CH) etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants.

Non-finitely axiomatisable two-dimensional modal logics

2012 ◽  
Vol 77 (3) ◽  
pp. 970-986 ◽  
Author(s):  
Agi Kurucz ◽  
Sérgio Marcelino
Keyword(s):  
Modal Logics ◽  
Two Dimensional ◽  
Recursively Enumerable ◽  
Bimodal Logics

AbstractWe show the first examples of recursively enumerable (even decidable) two-dimensional products of finitely axiomatisable modal logics that are not finitely axiomatisable. In particular, we show that any axiomatisation of some bimodal logics that are determined by classes of product frames with linearly ordered first components must be infinite in two senses: It should contain infinitely many propositional variables, and formulas of arbitrarily large modal nesting-depth.

scholarly journals Recursive enumerability and elementary frame definability in predicate modal logic

2019 ◽  
Vol 30 (2) ◽  
pp. 549-560 ◽  
Author(s):  
Mikhail Rybakov ◽  
Dmitry Shkatov
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
The Other ◽  
Kripke Semantics ◽  
First Order ◽  
Elementary Class ◽  
Recursive Enumerability ◽  
Kripke Frames ◽  
Recursively Enumerable ◽  
The Relationship

Abstract We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On one hand, it is well known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e. a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous examples are known of predicate modal logics, based on ‘natural’ propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplete. This raises the question of whether every Kripke complete, recursively enumerable predicate modal logic can be characterized by an elementary class of Kripke frames. We answer this question in the negative, by constructing a normal predicate modal logic which is Kripke complete, recursively enumerable, but not complete with respect to an elementary class of frames. We also present an example of a normal predicate modal logic that is recursively enumerable, Kripke complete, and not complete with respect to an elementary class of rooted frames, but is complete with respect to an elementary class of frames that are not rooted.

Algorithmic properties of first-order modal logics of finite Kripke frames in restricted languages

2020 ◽  
Vol 30 (7) ◽  
pp. 1305-1329 ◽  
Author(s):  
Mikhail Rybakov ◽  
Dmitry Shkatov
Keyword(s):  
Possible Worlds ◽  
Modal Logics ◽  
Finite Frames ◽  
First Order ◽  
Kripke Frames ◽  
Finite Frame ◽  
Recursively Enumerable ◽  
Finite Set ◽  
Individual Variables ◽  
Natural Classes

Abstract We study the effect of restricting the number of individual variables, as well as the number and arity of predicate letters, in languages of first-order predicate modal logics of finite Kripke frames on the logics’ algorithmic properties. A finite frame is a frame with a finite set of possible worlds. The languages we consider have no constants, function symbols or the equality symbol. We show that most predicate modal logics of natural classes of finite Kripke frames are not recursively enumerable—more precisely, $\varPi ^0_1$-hard—in languages with three individual variables and a single monadic predicate letter. This applies to the logics of finite frames of the predicate extensions of the sublogics of propositional modal logics $\textbf{GL}$, $\textbf{Grz}$ and $\textbf{KTB}$—among them, $\textbf{K}$, $\textbf{T}$, $\textbf{D}$, $\textbf{KB}$, $\textbf{K4}$ and $\textbf{S4}$.

Modal Nonmonotonic Logic with Restricted Application of the Negation as Failure to Prove Rule1

1991 ◽  
Vol 14 (3) ◽  
pp. 355-366
Author(s):  
Mirosław Truszczynski
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
Nonmonotonic Logic ◽  
Kripke Semantics ◽  
Negation As Failure ◽  
The Family ◽  
Nonmonotonic Modal Logics ◽  
Nonmonotonic Logics

In the paper we study a family of modal nonmonotonic logics closely related to the family of modal nonmonotonic logics proposed by McDermott and Doyle. For a modal logic S and a fixed collection of formulas X we introduce the notion of an ( S, X)-expansion. We restrict to modal logics which have a complete Kripke semantics. We study the properties of ( S, X)-expansions and show that in many respects they are analogous to the properties of S-expansions in nonmonotonic modal logics of McDermott and Doyle.

scholarly journals On the multi-dimensional modal logic of substitutions

2019 ◽  
Vol 56 (4) ◽  
pp. 454-481
Author(s):  
Tarek Sayed Ahmed ◽  
Mohammad Assem Mahmoud
Keyword(s):  
Amalgamation Property ◽  
Modal Logics ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Semantics ◽  
Infinite Dimensions ◽  
Finite Axiomatizability ◽  
First Order ◽  
Abstract Entities ◽  
Omitting Types

Abstract We prove completeness, interpolation, decidability and an omitting types theorem for certain multi-dimensional modal logics where the states are not abstract entities but have an inner structure. The states will be sequences. Our approach is algebraic addressing varieties generated by complex algebras of Kripke semantics for such logics. The algebras dealt with are common cylindrification free reducts of cylindric and polyadic algebras. For finite dimensions, we show that such varieties are finitely axiomatizable, have the super amalgamation property, and that the subclasses consisting of only completely representable algebras are elementary, and are also finitely axiomatizable in first order logic. Also their modal logics have an N P complete satisfiability problem. Analogous results are obtained for infinite dimensions by replacing finite axiomatizability by finite schema axiomatizability.

Sign in / Sign up

Export Citation Format

Share Document