Back and forth constructions in modal logic: An interpolation theorem for a family of modal logics

1986 ◽  
Vol 51 (4) ◽  
pp. 969-980 ◽  
Author(s):  
George Weaver ◽  
Jeffrey Welaish
Keyword(s):  
Modal Logic ◽  
Logical Consequence ◽  
Logical Truth ◽  
Interpolation Theorem ◽  
Modal Logics ◽  
Kripke Semantics ◽  
Direct Products ◽  
Possible World ◽  
Relational Systems ◽  
Modal Analogue

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

Liberated Brouwerian Modal Logic

Dialogue ◽  
1974 ◽  
Vol 13 (3) ◽  
pp. 505-514 ◽  
Author(s):  
Charles G. Morgan
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
Possible World ◽  
Modal Systems ◽  
Relationship Of ◽  
The Relationship

In an attempt to “purify” logic of existential presuppositions, attention has recently focused on modal logics, where one usually assumes that at least one possible world exists. Systems very analogous to some of the standard modal systems have been developed which drop this presupposition. We will here treat the removal of the existential assumption from Brouwerian modal logic and discuss the relationship of the system so derived to other modal systems.

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.

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.

Provability in finite subtheories of PA and relative interpretability: a modal investigation

1987 ◽  
Vol 52 (2) ◽  
pp. 494-511 ◽  
Author(s):  
Franco Montagna
Keyword(s):  
Modal Logic ◽  
Peano Arithmetic ◽  
Modal Logics ◽  
Kripke Semantics

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.

BELNAP–DUNN MODAL LOGICS: TRUTH CONSTANTS VS. TRUTH VALUES

2019 ◽  
Vol 13 (2) ◽  
pp. 416-435 ◽  
Author(s):  
SERGEI P. ODINTSOV ◽  
STANISLAV O. SPERANSKI
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
Kripke Semantics ◽  
Strong Negation ◽  
Truth Values ◽  
Normal Modal Logic ◽  
Original Language ◽  
Normal Modal Logics

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.

The lattice of modal logics: an algebraic investigation

1980 ◽  
Vol 45 (2) ◽  
pp. 221-236 ◽  
Author(s):  
W. J. Blok
Keyword(s):  
Modal Logic ◽  
Natural Number ◽  
Classical Logic ◽  
Finite Algebra ◽  
Modal Logics ◽  
Kripke Semantics ◽  
Modal Algebras ◽  
Algebraic Investigation

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.

Reduction of tense logic to modal logic. I

1974 ◽  
Vol 39 (3) ◽  
pp. 549-551 ◽  
Author(s):  
S. K. Thomason
Keyword(s):  
Modal Logic ◽  
Logical Consequence ◽  
Tense Logic ◽  
Kripke Semantics ◽  
Relational Semantics ◽  
Propositional Modal Logic ◽  
Formal Systems ◽  
Unary Operator ◽  
Countable Infinity ◽  
Image Position

It will be shown that propositional tense logic (with the Kripke relational semantics) may be regarded as a fragment of propositional modal logic (again with the Kripke semantics). This paper deals only with model theory. The interpretation of formal systems of tense logic as formal systems of modal logic will be discussed in [6].The languages M and T, of modal and tense logic respectively, each have a countable infinity of propositional variables and the Boolean connectives; in addition, M has the unary operator ⋄ and T has the unary operators F and P. A structure is a pair <W, ≺<, where W is a nonempty set and ≺ is a binary relation on W. An assignment V assigns to each propositional variable p a subset V(p) of W. Then V(α)£ W is defined for all formulas α of M or T by induction:We say that α is valid in <W, ≺>, or <W, ≺>, ⊨ α, if ⊩ (α) = W for every assignment V for <W, ≺>. If Γ is a set of formulas of M [T] and α is a formula of M [T], then α is a logical consequence of Γ, or Γ ⊩ α,if α is valid in every model of Γ i.e., in every structure in which all γ ∈ Γ are valid.

Modal operators and functional completeness, II

1977 ◽  
Vol 42 (3) ◽  
pp. 391-399 ◽  
Author(s):  
S. K. Thomason
Keyword(s):  
Modal Logic ◽  
Possible Worlds ◽  
Kripke Semantics ◽  
Functional Completeness ◽  
Possible World ◽  
States Of Affairs ◽  
Propositional Modal Logic ◽  
Modal Operators ◽  
Fixed Frame ◽  
State Of Affairs

In the Kripke semantics for propositional modal logic, a frame W = (W, ≺) represents a set of “possible worlds” and a relation of “accessibility” between possible worlds. With respect to a fixed frame W, a proposition is represented by a subset of W (regarded as the set of worlds in which the proposition is true), and an n-ary connective (i.e. a way of forming a new proposition from an ordered n-tuple of given propositions) is represented by a function fw: (P(W))n → P(W). Finally a state of affairs (i.e. a consistent specification whether or not each proposition obtains) is represented by an ultrafilter over W. {To avoid possible confusion, the reader should forget that some people prefer the term “states of affairs” for our “possible worlds”.}In a broader sense, an n-ary connective is represented by an n-ary operatorf = {fw∣ W ∈ Fr}, where Fr is the class of all frames and each fw: (P(W))n → P(W). A connective is modal if it corresponds to a formula of propositional modal logic. A connective C is coherent if whether C(P1,…, Pn) is true in a possible world depends only upon which modal combinations of P1,…,Pn are true in that world. (A modal combination of P1,…,Pn is the result of applying a modal connective to P1,…, Pn.) A connective C is strongly coherent if whether C(P1, …, Pn) obtains in a state of affairs depends only upon which modal combinations of P1,…, Pn obtain in that state of affairs.

A Modal Semantics of Negation in Logic Programming

1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani
Keyword(s):  
Modal Logic ◽  
Logic Programming ◽  
Modal Logics ◽  
Kripke Models ◽  
Logic Programs ◽  
Modal Semantics ◽  
Soundness And Completeness ◽  
Modal Completion ◽  
Well Foundedness

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.

Sign in / Sign up

Export Citation Format

Share Document