First-order definability in modal logic

1975 ◽  
Vol 40 (1) ◽  
pp. 35-40 ◽  
Author(s):  
R. I. Goldblatt
Keyword(s):  
Modal Logic ◽  
Binary Relation ◽  
Second Order ◽  
Order Conditions ◽  
Kripke Models ◽  
Order Condition ◽  
First Order ◽  
Axiom Systems ◽  
Set Of Points ◽  
First Order Definability

In the early days of the development of Kripke-style semantics for modal logic a great deal of effort was devoted to showing that particular axiom systems were characterised by a class of models describable by a first-order condition on a binary relation. For a time the approach seemed all encompassing, but recent work by Thomason [6] and Fine [2] has shown it to be somewhat limited—there are logics not determined by any class of Kripke models at all. In fact it now seems that modal logic is basically second-order in nature, in that any system may be analysed in terms of structures having a nominated class of second-order individuals (subsets) that serve as interpretations of propositional variables (cf. [7]). The question has thus arisen as to how much of modal logic can be handled in a first-order way, and precisely which modal sentences are determined by first-order conditions on their models. In this paper we present a model-theoretic characterisation of this class of sentences, and show that it does not include the much discussed LMp → MLp.Definition 1. A modal frame ℱ = 〈W, R〉 consists of a set W on which a binary relation R is defined. A valuation V on ℱ is a function that associates with each propositional variable p a subset V(p) of W (the set of points at which p is “true”).

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander
Keyword(s):  
Modal Logic ◽  
Optimal Strategy ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
First Order ◽  
Modal Operators ◽  
Crucial Difference ◽  
Definition Of ◽  
Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

scholarly journals COMPLETENESS OF SECOND-ORDER PROPOSITIONAL S4 AND H IN TOPOLOGICAL SEMANTICS

2018 ◽  
Vol 11 (3) ◽  
pp. 507-518
Author(s):  
PHILIP KREMER
Keyword(s):  
Modal Logic ◽  
Intuitionistic Logic ◽  
Second Order ◽  
Topological Semantics ◽  
First Order ◽  
Propositional Modal Logic ◽  
Propositional Quantifiers ◽  
Modal Logic S4 ◽  
Natural Way

AbstractWe add propositional quantifiers to the propositional modal logic S4 and to the propositional intuitionistic logic H, introducing axiom schemes that are the natural analogs to axiom schemes typically used for first-order quantifiers in classical and intuitionistic logic. We show that the resulting logics are sound and complete for a topological semantics extending, in a natural way, the topological semantics for S4 and for H.

Reflections on the concept of symmetry

2005 ◽  
Vol 13 (S2) ◽  
pp. 3-11 ◽  
Author(s):  
KUNO LORENZ
Keyword(s):  
Binary Relation ◽  
Second Order ◽  
The Other ◽  
First Order ◽  
Broken Symmetries ◽  
Other Hand ◽  
Logical Notion ◽  
The One ◽  
Ancient Usage

The concept of symmetry is omnipresent, although originally, in Greek antiquity, distinctly different from the modern logical notion. In logic a binary relation R is called symmetric if xRy implies yRx. In Greek, ‘being symmetric’ in general usage is synonymous with ‘being harmonious’, and in technical usage, as in Euclid's Elements, it is synonymous with ‘commensurable’. Due to the second meaning, which is close to the etymology of συ´μμετρoς, ‘with measure’ has likewise to be read as ‘being [in] rational [ratios]’ and displays the origin of the concept of rationality of establishing a proportion. Heraclitus can be read as a master of such connections. Exercising rationality is a case of simultaneously finding and inventing symmetries. On that basis a proposal is made of how to relate the modern logical notion of symmetry, a second-order concept, on the one hand with modern first-order usages of the term symmetric in geometry and other fields, and on the other hand with the notion of balance that derives from the ancient usage of symmetric. It is argued that symmetries as states of balance exist only in theory, in practice they function as norms vis-à-vis broken symmetries.

scholarly journals An Arithmetically Complete Predicate Modal Logic

2021 ◽  
Author(s):  
George Tourlakis ◽  
Yunge Hao
Keyword(s):  
Modal Logic ◽  
Current Paper ◽  
Kripke Models ◽  
First Order ◽  
Semantic Completeness ◽  
First Order Modal Logic ◽  
Conservation Theorem ◽  
Order Extension

This paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness (with respect to finite reverse well-founded Kripke models) is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that \(\textup{ML}^3\) is arithmetically complete. As expanded below, \(\textup{ML}^3\) is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"\(\Box\)" simulating the the informal classical "\(\vdash\)"―is also arithmetically complete in the Solovay sense.

Elucidation of the Nucleophilic Potential of Diazocyclopentadiene

Synthesis ◽  
2022 ◽  
Author(s):  
Herbert Mayr ◽  
Manfred Hartnagel ◽  
Armin R. Ofial
Keyword(s):  
Rate Constants ◽  
Second Order ◽  
Order Conditions ◽  
First Order ◽  
Electrophilic Substitutions ◽  
Order Rate ◽  
Nucleophilic Reactivity ◽  
Pseudo First Order

AbstractDiazocyclopentadiene reacts with benzhydrylium ions (Ar2CH+) to give 2,5-dibenzhydryl-substituted diazocyclopentadienes. The kinetics have been determined photometrically in dichloromethane under pseudo-first-order conditions using diazocyclopentadiene in excess. Plots of the second-order rate constants (log k 2) versus the electrophilicity parameters E of the benzhydrylium ions gave the nucleo­philicity parameter N = 4.84 and susceptibility s N = 1.06 for diazo­cyclopentadiene according to the correlation log k(20 °C) = s N(E + N). Diazocyclopentadiene thus has a similar nucleophilic reactivity as pyrrole. Previously reported electrophilic substitutions of diazocyclopentadiene are rationalized by these parameters and new reaction possibilities are predicted.

Universal First-Order Definability in Modal Logic

1980 ◽  
Vol 26 (19-21) ◽  
pp. 327-330 ◽  
Author(s):  
R. E. Jennings ◽  
D. K. Johnston ◽  
P. K. Schotch
Keyword(s):  
Modal Logic ◽  
First Order ◽  
First Order Definability

How to glue analysis models

1984 ◽  
Vol 49 (4) ◽  
pp. 1339-1349 ◽  
Author(s):  
D. Van Dalen
Keyword(s):  
Intuitionistic Logic ◽  
Second Order ◽  
Kripke Semantics ◽  
Kripke Models ◽  
Closure Properties ◽  
Second Order Arithmetic ◽  
First Order ◽  
Order Arithmetic ◽  
Analysis Models

Among the more traditional semantics for intuitionistic logic the Beth and the Kripke semantics seem well-suited for direct manipulations required for the derivation of metamathematical results. In particular Smoryński demonstrated the usefulness of Kripke models for the purpose of obtaining closure properties for first-order arithmetic, [S], and second-order arithmetic, [J-S]. Weinstein used similar techniques to handle intuitionistic analysis, [W]. Since, however, Beth-models seem to lend themselves better for dealing with analysis, cf. [D], we have developed a somewhat more liberal semantics, that shares the features of both Kripke and Beth semantics, in order to obtain analogues of Smoryński's collecting operations, which we will call Smoryński-glueing, in line with the categorical tradition.

Sign in / Sign up

Export Citation Format

Share Document