scholarly journals Successor-Invariant First-Order Logic on Classes of Bounded Degree (Extended Abstract)

Author(s):  
Julien Grange

We study the expressive power of successor-invariant first-order logic, which is an extension of first-order logic where the usage of a successor relation on the vertices of the graph is allowed, as long as the validity of formulas is independent on the choice of a particular successor. We show that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Julien Grange

We study the expressive power of successor-invariant first-order logic, which is an extension of first-order logic where the usage of an additional successor relation on the structure is allowed, as long as the validity of formulas is independent of the choice of a particular successor on finite structures. We show that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.


1999 ◽  
Vol 64 (4) ◽  
pp. 1751-1773 ◽  
Author(s):  
Lauri Hella ◽  
Leonid Libkin ◽  
Juha Nurmonen

AbstractMany known tools for proving expressibility bounds for first-ordér logic are based on one of several locality properties. In this paper we characterize the relationship between those notions of locality. We note that Gaifman's locality theorem gives rise to two notions: one deals with sentences and one with open formulae. We prove that the former implies Hanf's notion of locality, which in turn implies Gaifman's locality for open formulae. Each of these implies the bounded degree property, which is one of the easiest tools for proving expressibility bounds. These results apply beyond the first-order case. We use them to derive expressibility bounds for first-order logic with unary quantifiers and counting. We also characterize the notions of locality on structures of small degree.


2021 ◽  
pp. 8-30
Author(s):  
Salvatore Florio ◽  
Øystein Linnebo

Plural logic is a logical system in which plural terms and predicates figure as primitive expressions alongside the singular resources of ordinary first-order logic. The philosophical significance of this system depends on two of its alleged features: being pure logic and providing more expressive power than first-order logic. This chapter first introduces the language and axioms of plural logic and then analyzes this logic’s main philosophical applications in metaphysics, philosophy of mathematics, and semantics.


1999 ◽  
Vol Vol. 3 no. 3 ◽  
Author(s):  
Thomas Schwentick ◽  
Klaus Barthelmann

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.


2007 ◽  
Vol 72 (2) ◽  
pp. 601-618 ◽  
Author(s):  
Benjamin Rossman

AbstractWe consider successor-invariant first-order logic (FO + succ)inv, consisting of sentences Φ involving an “auxiliary” binary relation S such that (, S1) ⊨ Φ ⇔ (, S2) ⊨ Φ for all finite structures and successor relations S1, S2 on . A successor-invariant sentence Φ has a well-defined semantics on finite structures with no given successor relation: one simply evaluates Φ on (, S) for an arbitrary choice of successor relation S. In this article, we prove that (FO + succ)inv is more expressive on finite structures than first-order logic without a successor relation. This extends similar results for order-invariant logic [8] and epsilon-invariant logic [10].


2005 ◽  
Vol 70 (3) ◽  
pp. 696-712 ◽  
Author(s):  
Johan Van Benthem

AbstractMinimal predicates P satisfying a given first-order description ϕ(P) occur widely in mathematical logic and computer science. We give an explicit first-order syntax for special first-order ‘PIA conditions’ ϕ(P) which guarantees unique existence of such minimal predicates. Our main technical result is a preservation theorem showing PIA-conditions to be expressively complete for all those first-order formulas that are preserved under a natural model-theoretic operation of ‘predicate intersection’. Next, we show how iterated predicate minimization on PIA-conditions yields a language MIN(FO) equal in expressive power to LFP(FO), first-order logic closed under smallest fixed-points for monotone operations. As a concrete illustration of these notions, we show how our sort of predicate minimization extends the usual frame correspondence theory of modal logic, leading to a proper hierarchy of modal axioms: first-order-definable, first-order fixed-point definable, and beyond.


2008 ◽  
Vol 19 (01) ◽  
pp. 205-217 ◽  
Author(s):  
STEVEN LINDELL

We use singulary vocabularies to analyze first-order definability over doubly-linked data structures. Singulary vocabularies contain only monadic predicate and monadic function symbols. A class of mathematical structures in any vocabulary can be elementarily interpreted in a singulary vocabulary, while preserving notions of total size and degree. Doubly-linked data structures are a special case of bounded-degree finite structures in which there are reciprocal connections between elements, corresponding closely with physically feasible models of information storage. They can be associated with logical models involving unary relations and bijective functions in what we call an invertible singulary vocabulary. Over classes of these models, there is a normal form for first-order logic which eliminates all quantification of dependent variables. The paper provides a syntactically based proof using counting quantifiers. It also makes precise the notion of implicit calculability for arbitrary arity first-order formulas. Linear-time evaluation of first-order logic over doubly-linked data structures becomes a direct corollary. Included is a discussion of why these special data structures are appropriate for physically realizable models of information.


2009 ◽  
Vol 74 (1) ◽  
pp. 168-186 ◽  
Author(s):  
Michael Benedikt ◽  
Luc Segoufin

AbstractThis work deals with the expressive power of logics on finite graphs with access to an additional “arbitrary” linear order. The queries that can be expressed this way are the order-invariant queries for the logic. For the standard logics used in computer science, such as first-order logic, it is known that access to an arbitrary linear order increases the expressiveness of the logic. However, when we look at the separating examples, we find that they have satisfying models whose Gaifman Graph is complex – unbounded in valence and in treewidth. We thus explore the expressiveness of order-invariant queries over well-behaved graphs. We prove that first-order order-invariant queries over strings and trees have no additional expressiveness over first-order logic in the original signature. We also prove new upper bounds on order-invariant queries over bounded treewidth and bounded valence graphs. Our results make use of a new technique of independent interest: the application of algebraic characterizations of definability to show collapse results.


2000 ◽  
Vol 65 (4) ◽  
pp. 1749-1757 ◽  
Author(s):  
Martin Otto

AbstractThere are properties of finite structures that are expressible with the use of Hilbert's ∈-operator in a manner that does not depend on the actual interpretation for ∈-terms. but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly enhance the expressive power of first-order logic even as far as deterministic queries are concerned, thereby answering a question raised by Abiteboul and Vianu.


1979 ◽  
Vol 44 (2) ◽  
pp. 129-146 ◽  
Author(s):  
John Cowles

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


Sign in / Sign up

Export Citation Format

Share Document