Finite model theory

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Model Theory ◽  
Classical Model ◽  
Expressive Power ◽  
Order Logic ◽  
Finite Model ◽  
Descriptive Complexity ◽  
Finite Model Theory ◽  
First Order ◽  
Finite Models ◽  
Finite Structures

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.

Some Aspects of Model Theory and Finite Structures

2002 ◽  
Vol 8 (3) ◽  
pp. 380-403 ◽  
Author(s):  
Eric Rosen
Keyword(s):  
Computer Science ◽  
Complexity Theory ◽  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Finite Model ◽  
Finite Model Theory ◽  
First Order ◽  
Single Sentence ◽  
Finite Structures

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.

Finite Variable Logics in Descriptive Complexity Theory

1998 ◽  
Vol 4 (4) ◽  
pp. 345-398 ◽  
Author(s):  
Martin Grohe
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Complexity Classes ◽  
Finite Model ◽  
Polynomial Space ◽  
Finite Model Theory ◽  
First Order ◽  
First Order Theory ◽  
Finite Structures

Throughout the development of finite model theory, the fragments of first-order logic with only finitely many variables have played a central role. This survey gives an introduction to the theory of finite variable logics and reports on recent progress in the area.For each k ≥ 1 we let Lk be the fragment of first-order logic consisting of all formulas with at most k (free or bound) variables. The logics Lk are the simplest finite-variable logics. Later, we are going to consider infinitary variants and extensions by so-called counting quantifiers.Finite variable logics have mostly been studied on finite structures. Like the whole area of finite model theory, they have interesting model theoretic, complexity theoretic, and combinatorial aspects. For finite structures, first-order logic is often too expressive, since each finite structure can be characterized up to isomorphism by a single first-order sentence, and each class of finite structures that is closed under isomorphism can be characterized by a first-order theory. The finite variable fragments seem to be promising candidates with the right balance between expressive power and weakness for a model theory of finite structures. This may have motivated Poizat [67] to collect some basic model theoretic properties of the Lk. Around the same time Immerman [45] showed that important complexity classes such as polynomial time (PTIME) or polynomial space (PSPACE) can be characterized as collections of all classes of (ordered) finite structures definable by uniform sequences of first-order formulas with a fixed number of variables and varying quantifier-depth.

Almost Everywhere Equivalence of Logics in Finite Model Theory

1996 ◽  
Vol 2 (4) ◽  
pp. 422-443 ◽  
Author(s):  
Lauri Hella ◽  
Phokion G. Kolaitis ◽  
Kerkko Luosto
Keyword(s):  
Model Theory ◽  
Expressive Power ◽  
Systematic Investigation ◽  
Finite Model ◽  
Descriptive Complexity ◽  
Finite Model Theory ◽  
Almost Everywhere ◽  
Finite Structures ◽  
The Status ◽  
New Framework

AbstractWe introduce a new framework for classifying logics on finite structures and studying their expressive power. This framework is based on the concept of almost everywhere equivalence of logics, that is to say, two logics having the same expressive power on a class of asymptotic measure 1. More precisely, if L, L′ are two logics and μ is an asymptotic measure on finite structures, then L ≡a.e.L′ (μ) means that there is a class C of finite structures with μ(C) = 1 and such that L and L′ define the same queries on C. We carry out a systematic investigation of ≡a.e. with respect to the uniform measure and analyze the ≡a.e.-equivalence classes of several logics that have been studied extensively in finite model theory. Moreover, we explore connections with descriptive complexity theory and examine the status of certain classical results of model theory in the context of this new framework.

scholarly journals The Finite Model Theory of Bayesian Networks: Descriptive Complexity

2018 ◽  
Author(s):  
Fabio Gagliardi Cozman ◽  
Denis Deratani Mauá
Keyword(s):  
Bayesian Networks ◽  
Bayesian Network ◽  
Model Theory ◽  
Complexity Class ◽  
Finite Model ◽  
Descriptive Complexity ◽  
Finite Model Theory ◽  
First Order

We adapt the theory of descriptive complexity to Bayesian networks, to quantify the expressivity of specifications based on predicates and quantifiers. We show that Bayesian network specifications that employ first-order quantification capture the complexity class PP; by allowing quantification over predicates, the resulting Bayesian network specifications capture each class in the hierarchy PP^(NP^...^NP), a result that does not seem to have equivalent in the literature.

scholarly journals A finite model-theoretical proof of a property of bounded query classes within PH

2004 ◽  
Vol 69 (4) ◽  
pp. 1105-1116 ◽  
Author(s):  
Leszek Aleksander Kołodziejczyk
Keyword(s):  
Normal Form ◽  
Model Theory ◽  
Finite Model ◽  
Sufficient Condition ◽  
Finite Model Theory ◽  
Finite Models ◽  
Constructible Function ◽  
Simple Sufficient Condition

Abstract.We use finite model theory (in particular, the method of FM-truth definitions, introduced in [MM01] and developed in [K04], and a normal form result akin to those of [Ste93] and [G97]) to prove:Let m ≥ 2. Then:(A) If there exists k such that NP⊆ Σm TIME(nk)∩ Πm TIME(nk), then for every r there exists kr such that :(B) If there exists a superpolynomial time-constructible function f such that NTIME(f), then additionally .This strengthens a result by Mocas [M96] that for any r, .In addition, we use FM-truth definitions to give a simple sufficient condition for the arity hierarchy to be strict over finite models.

On fixed-point logic with counting

2000 ◽  
Vol 65 (2) ◽  
pp. 777-787 ◽  
Author(s):  
Jörg Flum ◽  
Martin Grohe
Keyword(s):  
Fixed Point ◽  
Complexity Theory ◽  
Polynomial Time ◽  
Planar Graphs ◽  
Expressive Power ◽  
Descriptive Complexity ◽  
Main Motivation ◽  
First Order ◽  
Finite Structures ◽  
Tree Width

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.

Epsilon-logic is more expressive than first-order logic over finite structures

2000 ◽  
Vol 65 (4) ◽  
pp. 1749-1757 ◽  
Author(s):  
Martin Otto
Keyword(s):  
Expressive Power ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Database Theory ◽  
Finite Structures

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.

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

1979 ◽  
Vol 44 (2) ◽  
pp. 129-146 ◽  
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 ∅.

Strong 0-1 laws in finite model theory

2000 ◽  
Vol 65 (4) ◽  
pp. 1686-1704
Author(s):  
Wafik Boulos Lotfallah
Keyword(s):  
Model Theory ◽  
Sample Space ◽  
Finite Model ◽  
Additive Measure ◽  
Finite Model Theory ◽  
Finite Models ◽  
The Universe ◽  
New Framework

AbstractWe introduce a new framework for asymptotic probabilities of sentences, in which we have a σ-additive measure on the sample space of all sequences A = {} of finite models, where the universe of is {1,2, …, n}. and use this framework to strengthen 0-1 laws for logics.

Sign in / Sign up

Export Citation Format

Share Document