A note on modal formulae and relational properties

1975 ◽  
Vol 40 (1) ◽  
pp. 55-58 ◽  
Author(s):  
J. F. A. K. van Benthem
Keyword(s):  
Interesting Case ◽  
Order Logic ◽  
Modal Formula ◽  
First Order ◽  
Modal Operators ◽  
Relational Properties ◽  
Truth Definition ◽  
Image Position ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Consider modal propositional formulae, constructed using proposition-letters, connectives and the modal operators □ and ⋄. The semantic structures are frames, i.e., pairs <W, R> with R ⊆ W2. Let F, V be variables ranging respectively over frames and functions from the set of proposition-letters into the powerset of W. Then the relationmay be defined, for arbitrary formulae α, following the Kripke truth-definition. From this relation we may further defineNow, to every modal formula α there corresponds some property Pα of R. A particular example is obtained by considering the well-known translation of modal formulae into formulae of monadic second-order logic with a single binary first-order predicate. For these particular Pα we havefor all F and w ∈ W. These formulae Pα are, however, rather intractable and more convenient ones can often be found. An especially interesting case occurs when Pα may be taken to be some first-order formula. For example, it can be seen thatfor all F and w ∈ W. It is customary to talk about a related correspondence, namely when for all F we haveNote that this correspondence holds whenever the first one above holds.

Representability in second-order propositional poly-modal logic

2002 ◽  
Vol 67 (3) ◽  
pp. 1039-1054 ◽  
Author(s):  
G. Aldo Antonelli ◽  
Richmond H. Thomason
Keyword(s):  
Modal Logic ◽  
Possible Worlds ◽  
Second Order ◽  
Order Logic ◽  
Multiple Modalities ◽  
Modal Operators ◽  
Second Order Systems ◽  
Second Order Logic ◽  
Monadic Second Order Logic ◽  
Propositional System

AbstractA propositional system of modal logic is second-order if it contains quantifiers ∀p and ∃p which, in the standard interpretation, are construed as ranging over sets of possible worlds (propositions). Most second-order systems of modal logic are highly intractable; for instance, when augmented with propositional quantifiers, K, B, T, K4 and S4 all become effectively equivalent to full second-order logic. An exception is S5, which, being interpretable in monadic second-order logic, is decidable.In this paper we generalize this framework by allowing multiple modalities. While this does not affect the undecidability of K, B, T, K4 and S4, poly-modal second-order S5 is dramatically more expressive than its mono-modal counterpart. As an example, we establish the definability of the transitive closure of finitely many modal operators. We also take up the decidability issue, and, using a novel encoding of sets of unordered pairs by partitions of the leaves of certain graphs, we show that the second-order propositional logic of two S5 modalitities is also equivalent to full second-order logic.

scholarly journals First order quantifiers in monadic second order logic

2004 ◽  
Vol 69 (1) ◽  
pp. 118-136 ◽  
Author(s):  
H. Jerome Keisler ◽  
Wafik Boulos Lotfallah
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Existential Quantifier ◽  
Reachability Problem ◽  
Open Problems ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic ◽  
Quantifier Alternation

AbstractThis paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01].We introduce an operation existsn (S) on properties S that says “there are n components having S”. We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict.We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W.We introduce another operation alt(S) on properties which has the same relationship with the Circuit Value Problem as reach(S) (defined in [JM01]) has with the Directed Reachability Problem. We use alt(S) to show that Πn ⊈ FO(Σn), Σn ⊈ FO(∆n). and ∆n+1 ⊈ FOB(Σn), solving some open problems raised in [Mat98].

scholarly journals Where First-Order and Monadic Second-Order Logic Coincide

2016 ◽  
Vol 17 (4) ◽  
pp. 1-18 ◽  
Author(s):  
Michael Elberfeld ◽  
Martin Grohe ◽  
Till Tantau
Keyword(s):  
Second Order ◽  
Order Logic ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic

scholarly journals Symbolic WS1S

10.29007/t28j ◽  
2018 ◽  
Author(s):  
Loris D'Antoni ◽  
Margus Veanes
Keyword(s):  
Blow Up ◽  
Finite Automata ◽  
Decision Procedures ◽  
Second Order ◽  
Order Logic ◽  
Symbolic Logic ◽  
First Order ◽  
Symbolic Automata ◽  
Second Order Logic ◽  
Monadic Second Order Logic

We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets byallowing character predicates to range over decidable first order theories and not just finite alphabets.We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such alogic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata toour symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formulathat preserves satisfiability, at the price of an exponential blow-up.

scholarly journals Using hybrid logic for querying dependency treebanks

2012 ◽  
Vol 7 ◽  
Author(s):  
Anders Søgaard ◽  
Søren Lind Kristiansen
Keyword(s):  
General Purpose ◽  
Second Order ◽  
Logic Model ◽  
Order Logic ◽  
Hybrid Logic ◽  
First Order Logic ◽  
Model Checker ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Existing logic-based querying tools for dependency treebanks use first order logic or monadic second order logic. We introduce a very fast model checker based on hybrid logic with operators ↓, @ and A and show that it is much faster than an existing querying tool for dependency treebanks based on first order logic, and much faster than an existing general purpose hybrid logic model checker. The querying tool is made publicly available.

scholarly journals Local Normal Forms for First-Order Logic with Applications to Games and Automata

1999 ◽  
Vol Vol. 3 no. 3 ◽  
Author(s):  
Thomas Schwentick ◽  
Klaus Barthelmann
Keyword(s):  
Normal Forms ◽  
Winning Strategy ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Relational Structures ◽  
Second Order Logic ◽  
Monadic Second Order Logic

International audience Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata models are defined that have, on arbitrary classes of relational structures, exactly the expressive power of first-order logic and existential monadic second-order logic, respectively.

scholarly journals The complexity of first-order and monadic second-order logic revisited

2004 ◽  
Vol 130 (1-3) ◽  
pp. 3-31 ◽  
Author(s):  
Markus Frick ◽  
Martin Grohe
Keyword(s):  
Second Order ◽  
Order Logic ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic

scholarly journals Where First-Order and Monadic Second-Order Logic Coincide

2012 ◽  
Author(s):  
Michael Elberfeld ◽  
Martin Grohe ◽  
Till Tantau
Keyword(s):  
Second Order ◽  
Order Logic ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic

scholarly journals A MODEL-THEORETIC CHARACTERIZATION OF MONADIC SECOND ORDER LOGIC ON INFINITE WORDS

2017 ◽  
Vol 82 (1) ◽  
pp. 62-76 ◽  
Author(s):  
SILVIO GHILARDI ◽  
SAMUEL J. VAN GOOL
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Second Order ◽  
Order Logic ◽  
Natural Numbers ◽  
Infinite Words ◽  
First Order ◽  
First Order Theory ◽  
Second Order Logic ◽  
Monadic Second Order Logic

AbstractMonadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natural numbers with order, successor, and finitely many unary predicate symbols.Monadic second order logic over infinite words (S1S) can alternatively be described as a first-order logic interpreted in${\cal P}\left( \omega \right)$, the power set Boolean algebra of the natural numbers, equipped with modal operators for ‘initial’, ‘next’, and ‘future’ states. We prove that the first-order theory of this structure is the model companion of a class of algebras corresponding to a version of linear temporal logic (LTL) without until.The proof makes crucial use of two classical, nontrivial results from the literature, namely the completeness of LTL with respect to the natural numbers, and the correspondence between S1S-formulas and Büchi automata.

Sign in / Sign up

Export Citation Format

Share Document