Characterizing quantifier extensions of dependence logic

Typically, a formal language has variables that range over a collection of objects, or domain of discourse. A language is ‘second-order’ if it has, in addition, variables that range over sets, functions, properties or relations on the domain of discourse. A language is third-order if it has variables ranging over sets of sets, or functions on relations, and so on. A language is higher-order if it is at least second-order. Second-order languages enjoy a greater expressive power than first-order languages. For example, a set S of sentences is said to be categorical if any two models satisfying S are isomorphic, that is, have the same structure. There are second-order, categorical characterizations of important mathematical structures, including the natural numbers, the real numbers and Euclidean space. It is a consequence of the Löwenheim–Skolem theorems that there is no first-order categorical characterization of any infinite structure. There are also a number of central mathematical notions, such as finitude, countability, minimal closure and well-foundedness, which can be characterized with formulas of second-order languages, but cannot be characterized in first-order languages. Some philosophers argue that second-order logic is not logic. Properties and relations are too obscure for rigorous foundational study, while sets and functions are in the purview of mathematics, not logic; logic should not have an ontology of its own. Other writers disqualify second-order logic because its consequence relation is not effective – there is no recursively enumerable, sound and complete deductive system for second-order logic. The deeper issues underlying the dispute concern the goals and purposes of logical theory. If a logic is to be a calculus, an effective canon of inference, then second-order logic is beyond the pale. If, on the other hand, one aims to codify a standard to which correct reasoning must adhere, and to characterize the descriptive and communicative abilities of informal mathematical practice, then perhaps there is room for second-order logic.

Infinitary logic and admissible sets

Journal of Symbolic Logic ◽

10.2307/2271099 ◽

1969 ◽

Vol 34 (2) ◽

pp. 226-252 ◽

Cited By ~ 63

Author(s):

Jon Barwise

Keyword(s):

Second Order ◽

Order Logic ◽

Predicate Calculus ◽

Generalized Quantifiers ◽

Infinitary Logic ◽

First Order ◽

Admissible Sets ◽

Classical Language ◽

Second Order Logic ◽

Order Predicate Calculus

In recent years much effort has gone into the study of languages which strengthen the classical first-order predicate calculus in various ways. This effort has been motivated by the desire to find a language which is(I) strong enough to express interesting properties not expressible by the classical language, but(II) still simple enough to yield interesting general results. Languages investigated include second-order logic, weak second-order logic, ω-logic, languages with generalized quantifiers, and infinitary logic.

First order quantifiers in monadic second order logic

Journal of Symbolic Logic ◽

10.2178/jsl/1080938831 ◽

2004 ◽

Vol 69 (1) ◽

pp. 118-136 ◽

Cited By ~ 2

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

Logics with Multiteam Semantics

ACM Transactions on Computational Logic ◽

10.1145/3487579 ◽

2022 ◽

Vol 23 (2) ◽

pp. 1-30

Author(s):

Erich Grädel ◽

Richard Wilke

Keyword(s):

Wide Spectrum ◽

Expressive Power ◽

Second Order ◽

Order Logic ◽

Specific Class ◽

Mathematical Basis ◽

Logical Operators ◽

Team Semantics ◽

Independence Properties ◽

Second Order Logic

Team semantics is the mathematical basis of modern logics of dependence and independence. In contrast to classical Tarski semantics, a formula is evaluated not for a single assignment of values to the free variables, but on a set of such assignments, called a team. Team semantics is appropriate for a purely logical understanding of dependency notions, where only the presence or absence of data matters, but being based on sets, it does not take into account multiple occurrences of data values. It is therefore insufficient in scenarios where such multiplicities matter, in particular for reasoning about probabilities and statistical independencies. Therefore, an extension from teams to multiteams (i.e. multisets of assignments) has been proposed by several authors. In this paper we aim at a systematic development of logics of dependence and independence based on multiteam semantics. We study atomic dependency properties of finite multiteams and discuss the appropriate meaning of logical operators to extend the atomic dependencies to full-fledged logics for reasoning about dependence properties in a multiteam setting. We explore properties and expressive power of a wide spectrum of different multiteam logics and compare them to second-order logic and to logics with team semantics. In many cases the results resemble what is known in team semantics, but there are also interesting differences. While in team semantics, the combination of inclusion and exclusion dependencies leads to a logic with the full power of both independence logic and existential second-order logic, independence properties of multiteams are not definable by any combination of properties that are downwards closed or union closed and thus are strictly more powerful than inclusion-exclusion logic. We also study the relationship of logics with multiteam semantics with existential second-order logic for a specific class of metafinite structures. It turns out that inclusion-exclusion logic can be characterised in a precise sense by the Presburger fragment of this logic, but for capturing independence, we need to go beyond it and add some form of multiplication. Finally, we also consider multiteams with weights in the reals and study the expressive power of formulae by means of topological properties.

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

Discrete Mathematics & Theoretical Computer Science ◽

10.46298/dmtcs.254 ◽

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.

On Representations of Intended Structures in Foundational Theories

Journal of Philosophical Logic ◽

10.1007/s10992-021-09628-2 ◽

2021 ◽

Author(s):

Neil Barton ◽

Moritz Müller ◽

Mihai Prunescu

Keyword(s):

Expressive Power ◽

Second Order ◽

Order Logic ◽

Trade Off ◽

First Order ◽

Informal Mathematics ◽

Second Order Logic

AbstractOften philosophers, logicians, and mathematicians employ a notion of intended structure when talking about a branch of mathematics. In addition, we know that there are foundational mathematical theories that can find representatives for the objects of informal mathematics. In this paper, we examine how faithfully foundational theories can represent intended structures, and show that this question is closely linked to the decidability of the theory of the intended structure. We argue that this sheds light on the trade-off between expressive power and meta-theoretic properties when comparing first-order and second-order logic.

Polyteam semantics

Journal of Logic and Computation ◽

10.1093/logcom/exaa048 ◽

2020 ◽

Vol 30 (8) ◽

pp. 1541-1566

Author(s):

Miika Hannula ◽

Juha Kontinen ◽

Jonni Virtema

Keyword(s):

Analogous Result ◽

Expressive Power ◽

Order Logic ◽

Mathematical Framework ◽

Dependency Theory ◽

Dependence Logic ◽

First Order ◽

Team Semantics ◽

Implication Problem ◽

Second Order Logic

Abstract Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define Polyteam Semantics in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatization for the associated implication problem. We relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterize the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic ($\textsf{ESO}$). The analogous result is shown to hold for poly-independence logic and all $\textsf{ESO}$-definable properties. We also relate poly-inclusion logic to greatest fixed point logic.

The relative expressive power of some logics extending first-order logic

Journal of Symbolic Logic ◽

10.2307/2273723 ◽

1979 ◽

Vol 44 (2) ◽

pp. 129-146 ◽

Cited By ~ 7

Author(s):

John Cowles

Keyword(s):

Model Theory ◽

Expressive Power ◽

Second Order ◽

Order Logic ◽

The Other ◽

First Order Logic ◽

Finite Sets ◽

Limited Ability ◽

First Order ◽

Second Order Logic

In recent years there has been a proliferation of logics which extend first-order logic, e.g., logics with infinite sentences, logics with cardinal quantifiers such as “there exist infinitely many…” and “there exist uncountably many…”, and a weak second-order logic with variables and quantifiers for finite sets of individuals. It is well known that first-order logic has a limited ability to express many of the concepts studied by mathematicians, e.g., the concept of a wellordering. However, first-order logic, being among the simplest logics with applications to mathematics, does have an extensively developed and well understood model theory. On the other hand, full second-order logic has all the expressive power needed to do mathematics, but has an unworkable model theory. Indeed, the search for a logic with a semantics complex enough to say something, yet at the same time simple enough to say something about, accounts for the proliferation of logics mentioned above. In this paper, a number of proposed strengthenings of first-order logic are examined with respect to their relative expressive power, i.e., given two logics, what concepts can be expressed in one but not the other?For the most part, the notation is standard. Most of the notation is either explained in the text or can be found in the book [2] of Chang and Keisler. Some notational conventions used throughout the text are listed below: the empty set is denoted by ∅.

Expanding the Expressive Power of Monadic Second-Order Logic on Restricted Graph Classes

Lecture Notes in Computer Science - Combinatorial Algorithms ◽

10.1007/978-3-642-45278-9_15 ◽

2013 ◽

pp. 164-177 ◽

Cited By ~ 3

Author(s):

Robert Ganian ◽

Jan Obdržálek

Keyword(s):

Expressive Power ◽

Second Order ◽

Order Logic ◽

Graph Classes ◽

Second Order Logic ◽

Monadic Second Order Logic