scholarly journals Descriptive complexity of finite structures: Saving the quantifier rank

2005 ◽  
Vol 70 (2) ◽  
pp. 419-450 ◽  
Author(s):  
Oleg Pikhurko ◽  
Oleg Verbitsky

AbstractWe say that a first order formula Φ distinguishes a structure M over a vocabulary L from another structure M′ over the same vocabulary if Φ is true on M but false on M′. A formula Φ defines an L-structure M if Φ distinguishes M from any other non-isomorphic L-structure M′. A formula Φ identifies an n-element L-structure M if Φ distinguishes M from any other non-isomorphic n-element L-structure M′.We prove that every n-element structure M is identifiable by a formula with quantifier rank less than and at most one quantifier alternation, where k is the maximum relation arity of M. Moreover, if the automorphism group of M contains no transposition of two elements, the same result holds for definability rather than identification.The Bernays-Schönfinkel class consists of prenex formulas in which the existential quantifiers all precede the universal quantifiers. We prove that every n-element structure M is identifiable by a formula in the Bernays-Schönfinkel class with less than quantifiers. If in this class of identifying formulas we restrict the number of universal quantifiers to k, then less than quantifiers suffice to identify M and. as long as we keep the number of universal quantifiers bounded by a constant, at total quantifiers are necessary.

2000 ◽  
Vol 65 (2) ◽  
pp. 777-787 ◽  
Author(s):  
Jörg Flum ◽  
Martin Grohe

One of the fundamental results of descriptive complexity theory, due to Immerman [13] and Vardi [18], says that a class of ordered finite structures is definable in fixed-point logic if, and only if, it is computable in polynomial time. Much effort has been spent on the problem of capturing polynomial time, that is, describing all polynomial time computable classes of not necessarily ordered finite structures by a logic in a similar way.The most obvious shortcoming of fixed-point logic itself on unordered structures is that it cannot count. Immerman [14] responded to this by adding counting constructs to fixed-point logic. Although it has been proved by Cai, Fürer, and Immerman [1] that the resulting fixed-point logic with counting, denoted by IFP+C, still does not capture all of polynomial time, it does capture polynomial time on several important classes of structures (on trees, planar graphs, structures of bounded tree-width [15, 9, 10]).The main motivation for such capturing results is that they may give a better understanding of polynomial time. But of course this requires that the logical side is well understood. We hope that our analysis of IFP+C-formulas will help to clarify the expressive power of IFP+C; in particular, we derive a normal form. Moreover, we obtain a problem complete for IFP+C under first-order reductions.


Author(s):  
Shawn Hedman

This final chapter unites ideas from both model theory and complexity theory. Finite model theory is the part of model theory that disregards infinite structures. Examples of finite structures naturally arise in computer science in the form of databases, models of computations, and graphs. Instead of satisfiability and validity, finite model theory considers the following finite versions of these properties. • A first-order sentence is finitely satisfiable if it has a finite model. • A first-order sentence is finitely valid if every finite structure is a model. Finite model theory developed separately from the “classical” model theory of previous chapters. Distinct methods and logics are used to analyze finite structures. In Section 10.1, we consider various finite-variable logics that serve as useful languages for finite model theory. We define variations of the pebble games introduced in Section 9.2 to analyze the expressive power of these logics. Pebble games are one of the few tools from classical model theory that is useful for investigating finite structures. In Section 10.2, it is shown that many of the theorems from Chapter 4 are no longer true when restricted to finite models. There is no analog for the Completeness and Compactness theorems in finite model theory. Moreover, we prove Trakhtenbrot’s theorem which states that the set of finitely valid first-order sentences is not recursively enumerable. Descriptive complexity is the subject of 10.3. This subject describes the complexity classes discussed in Chapter 7 in terms of the logics introduced in Chapter 9. We prove Fagin’s theorem relating the class NP to existentional second-order logic. We prove the Cook–Levin theorem as a consequence of Fagin’s Theorem. This theorem states that the Satisfiability Problem for Propositional Logic is NP-complete. We conclude this chapter (and this book) with a section describing the close connection between logic and the P = NP problem. In this section, we discuss appropriate logics for the study of finite models. First-order logic, since it describes each finite model up to isomorphism, is too strong. For this reason, we must weaken the logic. It may seem counter-intuitive that we should gain knowledge by weakening our language.


10.37236/4910 ◽  
2015 ◽  
Vol 22 (2) ◽  
Author(s):  
Julie Linman ◽  
Michael Pinsker

The random permutation is the Fraïssé limit of the class of finite structures with two linear orders. Answering a problem stated by Peter Cameron in 2002, we use a recent Ramsey-theoretic technique to show that there exist precisely 39 closed supergroups of the automorphism group of the random permutation, and thereby expose all symmetries of this structure. Equivalently, we classify all structures which have a first-order definition in the random permutation.


2021 ◽  
Vol 82 (2) ◽  
Author(s):  
Robin Hirsch ◽  
Jaš Šemrl

AbstractThe motivation for using demonic calculus for binary relations stems from the behaviour of demonic turing machines, when modelled relationally. Relational composition (; ) models sequential runs of two programs and demonic refinement ($$\sqsubseteq $$ ⊑ ) arises from the partial order given by modeling demonic choice ($$\sqcup $$ ⊔ ) of programs (see below for the formal relational definitions). We prove that the class $$R(\sqsubseteq , ;)$$ R ( ⊑ , ; ) of abstract $$(\le , \circ )$$ ( ≤ , ∘ ) structures isomorphic to a set of binary relations ordered by demonic refinement with composition cannot be axiomatised by any finite set of first-order $$(\le , \circ )$$ ( ≤ , ∘ ) formulas. We provide a fairly simple, infinite, recursive axiomatisation that defines $$R(\sqsubseteq , ;)$$ R ( ⊑ , ; ) . We prove that a finite representable $$(\le , \circ )$$ ( ≤ , ∘ ) structure has a representation over a finite base. This appears to be the first example of a signature for binary relations with composition where the representation class is non-finitely axiomatisable, but where the finite representation property holds for finite structures.


2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Manuel Bodirsky ◽  
Bertalan Bodor

Abstract Let K exp + \mathcal{K}_{{\operatorname{exp}}{+}} be the class of all structures 𝔄 such that the automorphism group of 𝔄 has at most c ⁢ n d ⁢ n cn^{dn} orbits in its componentwise action on the set of 𝑛-tuples with pairwise distinct entries, for some constants c , d c,d with d < 1 d<1 . We show that K exp + \mathcal{K}_{{\operatorname{exp}}{+}} is precisely the class of finite covers of first-order reducts of unary structures, and also that K exp + \mathcal{K}_{{\operatorname{exp}}{+}} is precisely the class of first-order reducts of finite covers of unary structures. It follows that the class of first-order reducts of finite covers of unary structures is closed under taking model companions and model-complete cores, which is an important property when studying the constraint satisfaction problem for structures from K exp + \mathcal{K}_{{\operatorname{exp}}{+}} . We also show that Thomas’ conjecture holds for K exp + \mathcal{K}_{{\operatorname{exp}}{+}} : all structures in K exp + \mathcal{K}_{{\operatorname{exp}}{+}} have finitely many first-order reducts up to first-order interdefinability.


2002 ◽  
Vol 8 (3) ◽  
pp. 380-403 ◽  
Author(s):  
Eric Rosen

Model theory is concerned mainly, although not exclusively, with infinite structures. In recent years, finite structures have risen to greater prominence, both within the context of mainstream model theory, e.g., in work of Lachlan, Cherlin, Hrushovski, and others, and with the advent of finite model theory, which incorporates elements of classical model theory, combinatorics, and complexity theory. The purpose of this survey is to provide an overview of what might be called the model theory of finite structures. Some topics in finite model theory have strong connections to theoretical computer science, especially descriptive complexity theory (see [26, 46]). In fact, it has been suggested that finite model theory really is, or should be, logic for computer science. These connections with computer science will, however, not be treated here.It is well-known that many classical results of ‘infinite model theory’ fail over the class of finite structures, including the compactness and completeness theorems, as well as many preservation and interpolation theorems (see [35, 26]). The failure of compactness in the finite, in particular, means that the standard proofs of many theorems are no longer valid in this context. At present, there is no known example of a classical theorem that remains true over finite structures, yet must be proved by substantially different methods. It is generally concluded that first-order logic is ‘badly behaved’ over finite structures.From the perspective of expressive power, first-order logic also behaves badly: it is both too weak and too strong. Too weak because many natural properties, such as the size of a structure being even or a graph being connected, cannot be defined by a single sentence. Too strong, because every class of finite structures with a finite signature can be defined by an infinite set of sentences. Even worse, every finite structure is defined up to isomorphism by a single sentence. In fact, it is perhaps because of this last point more than anything else that model theorists have not been very interested in finite structures. Modern model theory is concerned largely with complete first-order theories, which are completely trivial here.


1995 ◽  
Vol 06 (04) ◽  
pp. 339-351
Author(s):  
WIESŁAW SZWAST

The minimal Gödel class is the class of first-order prenex sentences whose quantifier prefix consists of two universal quantifiers followed by just one existential quantifier. We prove that asymptotic probabilities of existential second-order sentences, whose first-order part is in the minimal Gödel class, form a dense subset of the unit interval.


Author(s):  
A. M. W. Glass ◽  
Yuri Gurevich ◽  
W. Charles Holland ◽  
Saharon Shelah

Classifying (unordered) sets by the elementary (first order) properties of their automorphism groups was undertaken in (7), (9) and (11). For example, if Ω is a set whose automorphism group, S(Ω), satisfiesthen Ω has cardinality at most ℵ0 and conversely (see (7)). We are interested in classifying homogeneous totally ordered sets (homogeneous chains, for short) by the elementary properties of their automorphism groups. (Note that we use ‘homogeneous’ here to mean that the automorphism group is transitive.) This study was begun in (4) and (5). For any set Ω, S(Ω) is primitive (i.e. has no congruences). However, the automorphism group of a homogeneous chain need not be o-primitive (i.e. it may have convex congruences). Fortunately, ‘o-primitive’ is a property that can be captured by a first order sentence for automorphisms of homogeneous chains. Hence our general problem falls naturally into two parts. The first is to classify (first order) the homogeneous chains whose automorphism groups are o-primitive; the second is to determine how the o-primitive components are related for arbitrary homogeneous chains whose automorphism groups are elementarily equivalent.


Sign in / Sign up

Export Citation Format

Share Document