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

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.

2019 ◽  
Vol 30 (2) ◽  
pp. 549-560 ◽  
Author(s):  
Mikhail Rybakov ◽  
Dmitry Shkatov

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.


1987 ◽  
Vol 52 (2) ◽  
pp. 494-511 ◽  
Author(s):  
Franco Montagna

By Solovay's theorem [16], the modal logic of provability GL gives a complete description of the propositional schemata involving the provability predicate PrPA(x) for Peano arithmetic PA, which are provable in PA. However, many important aspects of provability cannot be fully expressed in terms of PrPA(x). For this reason, many authors have introduced extensions of GL which take account either of Rosser constructions or of other important metamathematical formulas (see, for example, [5], [6], [14], [16], and [19]). In this paper, we concentrate on the modal logic of the provability predicate for finitely axiomatizable subtheories of PA; the interest of this modal logic is based on the following facts. First of all, it provides a modal translation of a very important property of PA, namely the essential reflexiveness. Secondly, in view of Orey's theorem [10] it constitutes a possible approach to the study of interpretability of finite extensions of PA. Indeed, by Orey's theorem PA + θ is interpretable in PA + θ′ iff for every n, and, therefore, relative interpretability of finitely axiomatizable extensions of PA can be expressed by means of the provability predicate for finitely axiomatizable subtheories of PA.In §1, we introduce three modal logics extending GL and discuss their arithmetical interpretations; §2 deals with Kripke semantics for two of these logics. In §3, a theorem on arithmetical completeness is shown, which characterizes the logic of the provability predicate for finitely axiomatizable subtheories of PA; a uniform version of this theorem is proved in §4.


2019 ◽  
Vol 13 (2) ◽  
pp. 416-435 ◽  
Author(s):  
SERGEI P. ODINTSOV ◽  
STANISLAV O. SPERANSKI

AbstractWe shall be concerned with the modal logic BK—which is based on the Belnap–Dunn four-valued matrix, and can be viewed as being obtained from the least normal modal logic K by adding ‘strong negation’. Though all four values ‘truth’, ‘falsity’, ‘neither’ and ‘both’ are employed in its Kripke semantics, only the first two are expressible as terms. We show that expanding the original language of BK to include constants for ‘neither’ or/and ‘both’ leads to quite unexpected results. To be more precise, adding one of these constants has the effect of eliminating the respective value at the level of BK-extensions. In particular, if one adds both of these, then the corresponding lattice of extensions turns out to be isomorphic to that of ordinary normal modal logics.


1986 ◽  
Vol 51 (4) ◽  
pp. 969-980 ◽  
Author(s):  
George Weaver ◽  
Jeffrey Welaish

The following is a contribution to the abstract study of the model theory of modal logics. Historically, individual modal logics have been specified deductively; and, as a result, it has seemed natural to view modal logics as sets of sentences provable in some deductive system. This proof theoretic view has influenced the abstract study of modal logics. For example, Fine [1975] defines a modal logic to be any set of sentences in the modal language L□ which contains all tautologies, all instances of the schema (□(ϕ ⊃ Ψ) ⊃ (□ϕ ⊃ □Ψ)), and which is closed under modus ponens, necessitation and substitution.Here, however, modal logics are equated with classes of “possible world” interpretations. “Worlds” are taken to be ordered pairs (a, λ), where a is a sentential interpretation and λ is an ordinal. Properties of the accessibility relation are identified with those classes of binary relational systems closed under isomorphisms. The origin of this approach is the study of alternative Kripke semantics for the normal modal logics (cf. Weaver [1973]). It is motivated by the desire that modal logics provide accounts of both logical truth and logical consequence (cf. Corcoran and Weaver [1969]) and the realization that there are alternative Kripke semantics for S4, B and M which give identical accounts of logical truth, but different accounts of logical consequence (cf. Weaver [1973]). It is shown that the Craig interpolation theorem holds for any modal logic which has characteristic modal axioms and whose associated class of binary relational systems is closed under subsystems and finite direct products. The argument uses a back and forth construction to establish a modal analogue of Robinson's theorem. The argument for the interpolation theorem from Robinson's theorem employs modal analogues of the Ehrenfeucht-Fraïssé characterization of elementary equivalence and Hintikka's distributive normal form, and is itself a modal analogue of a first order argument (cf. Weaver [1982]).


1980 ◽  
Vol 45 (2) ◽  
pp. 221-236 ◽  
Author(s):  
W. J. Blok

AbstractModal logics are studied in their algebraic disguise of varieties of so-called modal algebras. This enables us to apply strong results of a universal algebraic nature, notably those obtained by B. Jónsson. It is shown that the degree of incompleteness with respect to Kripke semantics of any modal logic containing the axiom □p→P or containing an axiom of the form □mp↔□m+1p for some natural number m is . Furthermore, we show that there exists an immediate predecessor of classical logic (axiomatized by p↔□p) which is not characterized by any finite algebra. The existence of modal logics having immediate predecessors is established. In contrast with these results we prove that the lattice of extensions of S4 behaves much better: a logic extending S4 is characterized by a finite algebra iff it has finitely many extensions and any such logic has only finitely many immediate predecessors, all of which are characterized by a finite algebra.


1992 ◽  
Vol 17 (1-2) ◽  
pp. 99-116
Author(s):  
V. Wiktor Marek ◽  
Miroslaw Truszczynski

Investigations of default logic have been so far mostly concerned with the notion of an extension of a default theory. It turns out, however, that default logic is much richer. Namely, there are other natural classes of objects that might be associated with default reasoning. We study two such classes of objects with emphasis on their relations with modal nonmonotonic formalisms. First, we introduce the concept of a weak extension and study its properties. It has long been suspected that there are close connections between default and autoepistemic logics. The notion of weak extension allows us to precisely describe the relationship between these two formalisms. In particular, we show that default logic with weak extensions is essentially equivalent to autoepistemic logic, that is, nonmonotonic logic KD45. In the paper we also study the notion of a set of formulas closed under a default theory. These objects are shown to correspond to stable theories and to modal logic S5. In particular, we show that skeptical reasoning with sets closed under default theories is closely related with provability in S5. As an application of our results we determine the complexity of reasoning with weak extensions and sets closed under default theories.


2014 ◽  
Vol 7 (3) ◽  
pp. 439-454 ◽  
Author(s):  
PHILIP KREMER

AbstractIn the topological semantics for propositional modal logic, S4 is known to be complete for the class of all topological spaces, for the rational line, for Cantor space, and for the real line. In the topological semantics for quantified modal logic, QS4 is known to be complete for the class of all topological spaces, and for the family of subspaces of the irrational line. The main result of the current paper is that QS4 is complete, indeed strongly complete, for the rational line.


1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani

The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.


10.29007/hgbj ◽  
2018 ◽  
Author(s):  
Nick Bezhanishvili

The method of canonical formulas is a powerful tool for investigating intuitionistic and modal logics. In this talk I will discuss an algebraic approach to this method. I will mostly concentrate on the case of intuitionistic logic. But I will also review the case of modal logic and possible generalizations to substructural logic.


Sign in / Sign up

Export Citation Format

Share Document