Finite model theory is currently not one of the hot topics in the philosophy and history of mathematics, not even in the philosophy and history of mathematical logic. The philosophy of mathematics and mathematical logic has concentrated on infinite structures, closely related to foundational issues. In that context, finite models deserved only marginal attention because it was taken for granted that the study of finite structures is trivial compared to the study of infinite structures. In (...) retrospect, research on finite structures turned out to be neither trivial nor irrelevant but had an important impact on theoretical computer science. A closer look at the early history of the spectrum problem shows that the birth of finite model theory has roots in formal logic, at a time when computer science did not yet exist. (shrink)

This book gives a comprehensive overview of central themes of finite model theory – expressive power, descriptive complexity, and zero-one laws – together with selected applications relating to database theory and artificial intelligence, especially constraint databases and constraint satisfaction problems. The final chapter provides a concise modern introduction to modal logic, emphasizing the continuity in spirit and technique with finite model theory. This underlying spirit involves the use of various fragments of and hierarchies (...) within first-order, second-order, fixed-point, and infinitary logics to gain insight into phenomena in complexity theory and combinatorics. The book emphasizes the use of combinatorial games, such as extensions and refinements of the Ehrenfeucht-Fraissé pebble game, as a powerful way to analyze the expressive power of such logics, and illustrates how deep notions from model theory and combinatorics, such as o-minimality and treewidth, arise naturally in the application of finite model theory to database theory and AI. Students of logic and computer science will find here the tools necessary to embark on research into finite model theory, and all readers will experience the excitement of a vibrant area of the application of logic to computer science. (shrink)

In [9] we introduced a new framework for asymptotic probabilities, in which a $\sigma-additive$ measure is defined on the sample space of all sequences $A = $ of finite models, where the universe of An is {1, 2, .., n}. In this framework we investigated the strong 0-1 law for sentences, which states that each sentence either holds in An eventually almost surely or fails in An eventually almost surely. In this paper we define the strong convergence law for (...) formulas, which carries over the ideas of the strong 0-1 law to formulas with free variables, and roughly states that for each formula φ(x), the fraction of tuples a in An, which satisfy the formula φ(x), almost surely has a limit as n tends to infinity. We show that the infinitary logic with finitely many variables has the strong convergence law for formulas for the uniform measure, and further characterize the measures on random graphs for which the strong convergence law holds. (shrink)

We 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 $\scr{L}\equiv _{\text{a.e.}}\scr{L}^{\prime}(\mu)$ 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 $\equiv _{\text{a.e.}}$ with respect to the uniform measure and analyze the $\equiv _{\text{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. (shrink)

We study model theory of fields with actions of a fixed finite group scheme. We prove the existence and simplicity of a model companion of the theory of such actions, which generalizes our previous results about truncated iterative Hasse–Schmidt derivations [13] and about Galois actions [14]. As an application of our methods, we obtain a new model complete theory of actions of a finite group on fields of finite imperfection degree.

In this paper we set out the basic model theory of differential fields of characteristic 0, which have finitely many commuting derivations. We give axioms for the theory of differentially closed differential fields with m derivations and show that this theory is ω-stable, model complete, and quantifier-eliminable, and that it admits elimination of imaginaries. We give a characterization of forking and compute the rank of this theory to be ω m + 1.

We give a survey of results obtained in the model theory of finite and pseudo-finite fields.

Let G be a finite group. We explore the model-theoretic properties of the class of differential fields of characteristic zero in m commuting derivations equipped with a G-action by differential fie...

This is a survey, intended both for group theorists and model theorists, concerning the structure of pseudofinite groups, that is, infinite models of the first-order theory of finite groups. The focus is on concepts from stability theory and generalisations in the context of pseudofinite groups, and on the information this might provide for finite group theory.

Djordjević [Dj 1] proved that under natural technical assumptions, if a complete L n -theory is stable and has amalgamation over sets, then it has arbitrarily large finite models. We extend his study and prove the existence of arbitrarily large finite models for classes of models of L n -theories (maybe omitting types) under weaker amalgamation properties. In particular our analysis covers the case of vector spaces.

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

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

In [01], we gave algebraic characterizations of elementary equivalence for finitely generated finite-by-abelian groups, i.e. finitely generated FC-groups. We also provided several examples of finitely generated finite-by-abelian groups which are elementarily equivalent without being isomorphic. In this paper, we shall use our previous results to describe precisely the models of the theories of finitely generated finite-by-abelian groups and the elementary embeddings between these models.

We describe the progress of model theory in the last half century from the standpoint of how finite model theory might develop.

We investigate theories of initial segments of the standard models for arithmetics. It is easy to see that if the ordering relation is definable in the standard model then the decidability results can be transferred from the infinite model into the finite models. On the contrary we show that the Σ₂—theory of multiplication is undecidable in finite models. We show that this result is optimal by proving that the Σ₁—theory of multiplication and order is (...) decidable in finite models as well as in the standard model. We show also that the exponentiation function is definable in finite models by a formula of arithmetic with multiplication and that one can define in finite models the arithmetic of addition and multiplication with the concatenation operation. We consider also the spectrum problem. We show that the spectrum of arithmetic with multiplication and arithmetic with exponentiation is strictly contained in the spectrum of arithmetic with addition and multiplication. (shrink)

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. 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. 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. (shrink)

A survey of the isomorphic submodels of Vω, the set of hereditarily finite sets. In the usual language of set theory, Vω has 2ℵ0 isomorphic submodels. But other set-theoretic languages give different systems of submodels. For example, the language of adjunction allows only countably many isomorphic submodels of Vω.

In this paper, we show that the finite model property fails for certain non‐integral semilinear substructural logics including Metcalfe and Montagna's uninorm logic and involutive uninorm logic, and a suitable extension of Metcalfe, Olivetti and Gabbay's pseudo‐uninorm logic. Algebraically, the results show that certain classes of bounded residuated lattices that are generated as varieties by their linearly ordered members are not generated as varieties by their finite members.

We prove a finite model theorem and infinitary completeness result for the propositional -calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.

This paper shows how the classical finite probability theory (with equiprobable outcomes) can be reinterpreted and recast as the quantum probability calculus of a pedagogical or toy model of quantum mechanics over sets (QM/sets). There have been several previous attempts to develop a quantum-like model with the base field of ℂ replaced by ℤ₂. Since there are no inner products on vector spaces over finite fields, the problem is to define the Dirac brackets and the (...) probability calculus. The previous attempts all required the brackets to take values in ℤ₂. But the usual QM brackets <ψ|ϕ> give the "overlap" between states ψ and ϕ, so for subsets S,T⊆U, the natural definition is <S|T>=|S∩T| (taking values in the natural numbers). This allows QM/sets to be developed with a full probability calculus that turns out to be a non-commutative extension of classical Laplace-Boole finite probability theory. The pedagogical model is illustrated by giving simple treatments of the indeterminacy principle, the double-slit experiment, Bell's Theorem, and identical particles in QM/Sets. A more technical appendix explains the mathematics behind carrying some vector space structures between QM over ℂ and QM/Sets over ℤ₂. (shrink)

We use finite model theory to prove:Let m ≥ 2. Then: If there exists k such that NP ⊆ σmTIME ∩ ΠmTIME, then for every r there exists kr such that PNP[nr] ⊆ σmTIME ∩ ΠmTIME; If there exists a superpolynomial time-constructible function f such that NTIME ⊆ Σpm ∪ Πpm, then additionally PNP[nr] ⊈ Σpm ∪ Πpm.This strengthens a result by Mocas [M96] that for any r, PNP[nr] ⊈ NEXP.In addition, we use FM-truth definitions to give (...) a simple sufficient condition for the σ11 arity hierarchy to be strict over finite models. (shrink)

This paper shows how the classical finite probability theory (with equiprobable outcomes) can be reinterpreted and recast as the quantum probability calculus of a pedagogical or toy model of quantum mechanics over sets (QM/sets). There have been several previous attempts to develop a quantum-like model with the base field of ℂ replaced by ℤ₂. Since there are no inner products on vector spaces over finite fields, the problem is to define the Dirac brackets and the (...) probability calculus. The previous attempts all required the brackets to take values in ℤ₂. But the usual QM brackets <ψ|ϕ> give the "overlap" between states ψ and ϕ, so for subsets S,T⊆U, the natural definition is <S|T>=|S∩T| (taking values in the natural numbers). This allows QM/sets to be developed with a full probability calculus that turns out to be a non-commutative extension of classical Laplace-Boole finite probability theory. The pedagogical model is illustrated by giving simple treatments of the indeterminacy principle, the double-slit experiment, Bell's Theorem, and identical particles in QM/Sets. A more technical appendix explains the mathematics behind carrying some vector space structures between QM over ℂ and QM/Sets over ℤ₂. (shrink)

A Steiner triple system (STS) is a set S together with a collection B of subsets of S of size 3 such that any two elements of S belong to exactly one element of B. It is well known that the class of finite STS has a Fraïssé limit M_F. Here, we show that the theory T of M_F is the model completion of the theory of STSs. We also prove that T is not small and (...) it has quantifier elimination, TP2, NSOP1, elimination of hyperimaginaries and weak elimination of imaginaries. (shrink)

Review by: Michael Benedikt The Bulletin of Symbolic Logic, Volume 19, Issue 1, Page 112-115, March 2013.

A stable theory is finitely based if every set of indiscernibles is based on a finite subset. This is a common generalization of superstability and 1-basedness. We show that if such theories have more than one model they must have infinitely many, and prove some other conjectures.

We study properties of forking in the classes of all finite models of a complete theory in a finite variable logic. We also study model constructions under the assumption that forking is trivial.

In this paper, we investigate the Lindenbaum algebra ℒ of the theory T fin = Th of the class M fin of all finite models of a finite rich signature. We prove that this algebra is an atomic Boolean algebra while its Gödel numeration γ is a [Formula: see text]-numeration. Moreover, the quotient algebra /ℱ, γ/ℱ) modulo the Fréchet ideal ℱ is a [Formula: see text]-algebra, which is universal over the class of all [Formula: see text] Boolean (...) algebras. These conditions characterize uniquely the algebra ℒ; moreover, these conditions characterize up to recursive isomorphism the numerated Boolean quotient algebra /ℱ, γ/ℱ). These results extend the work of Trakhtenbrot [17] and Vaught [18] on the first order theory of the class of all finite models of a finite rich signature. (shrink)

We search for a set-up in which results from the theory of infinite models hold for finite models. As an example we prove results from stability theory.

We consider all combinatorially possible systems corresponding to subsets of finite set theory (i.e., Zermelo-Fraenkel set theory without the axiom of infinity) and for each of them either provide a well-founded locally finite graph that is a model of that theory or show that this is impossible. To that end, we develop the technique of axiom closure of graphs.

We propose a set theory, called NRFST, in which the Cantorian axiom of infinity is negated, and a new notion of infinity is introduced via non standard methods, i. e. via adequate notions of standard and internal, two unary predicates added to the language of ZF. After some initial results on NRFST, we investigate its relative consistency with respect to ZF and Kawai's WNST.

In his Ph.D. thesis [7], L. van den Dries studied the model theory of fields with finitely many orderings and valuations where all open sets according to the topology defined by an order or a valuation is globally dense according with all other orderings and valuations. Van den Dries proved that the theory of these fields is companionable and that the theory of the companion is decidable .In this paper we study the case where the fields (...) are expanded with finitely many orderings and an independent derivation. We show that the theory of these fields still admits a model companion in the language Lequation image = {+, –, ·, D, <1, …, model companion by CODFm and give a geometric axiomatization of this theory which uses basic notions of algebraic geometry and some generalized open subsets which appear naturally in this context. This axiomatization allows to recover the one given in [4] for the theory CODF of closed ordered differential fields. Most of the technics we use here are already present in [2] and [4].Finally, we prove that it is possible to describe the completions of CODFm and to obtain quantifier elimination in a slightly enriched language. This generalizes van den Dries' results in the “derivation free” case. (shrink)

The current paper studies the formal properties of the Global Reflection Principle, to wit the assertion “All theorems of$\mathrm {Th}$are true,” where$\mathrm {Th}$is a theory in the language of arithmetic and the truth predicate satisfies the usual Tarskian inductive conditions for formulae in the language of arithmetic. We fix the gap in Kotlarski’s proof from [15], showing that the Global Reflection Principle for Peano Arithmetic is provable in the theory of compositional truth with bounded induction only ($\mathrm {CT}_0$). (...) Furthermore, we extend the above result showing that$\Sigma _1$-uniform reflection over a theory of uniform Tarski biconditionals ($\mathrm {UTB}^-$) is provable in$\mathrm {CT}_0$, thus answering the question of Beklemishev and Pakhomov [2]. Finally, we introduce the notion of a prolongable satisfaction class and use it to study the structure of models of$\mathrm {CT}_0$. In particular, we provide a new model-theoretical characterization of theories of finite iterations of uniform reflection and present a new proof characterizing the arithmetical consequences of$\mathrm {CT}_0$. (shrink)

Stemming from the works of Petr Hájek on mathematical fuzzy logic, graded model theory has been developed by several authors in the last two decades as an extension of classical model theory that studies the semantics of many-valued predicate logics. In this paper we take the first steps towards an abstract formulation of this model theory. We give a general notion of abstract logic based on many-valued models and prove six Lindström-style characterizations of maximality (...) of first-order logics in terms of metalogical properties such as compactness, abstract completeness, the Löwenheim–Skolem property, the Tarski union property, and the Robinson property, among others. As necessary technical restrictions, we assume that the models are valued on finite MTL-chains and the language has a constant for each truth-value. (shrink)

This paper shows how the classical finite probability theory (with equiprobable outcomes) can be reinterpreted and recast as the quantum probability calculus of a pedagogical or "toy" model of quantum mechanics over sets (QM/sets). There are two parts. The notion of an "event" is reinterpreted from being an epistemological state of indefiniteness to being an objective state of indefiniteness. And the mathematical framework of finite probability theory is recast as the quantum probability calculus for QM/sets. (...) The point is not to clarify finite probability theory but to elucidate quantum mechanics itself by seeing some of its quantum features in a classical setting. (shrink)

The paper discusses the notion of finite model truth definitions (or FM-truth definitions), introduced by M. Mostowski as a finite model analogue of Tarski's classical notion of truth definition. We compare FM-truth definitions with Vardi's concept of the combined complexity of logics, noting an important difference: the difficulty of defining FM-truth for a logic ᵍ does not depend on the syntax of L, as long as it is decidable. It follows that for a natural ᵍ there (...) exist FM-truth definitions whose evaluation is much easier than the combined complexiy of ᵍ would suggest. We apply the general theory to give a complexity-theoretical characterization of the logics for which the $\Sigma_{m}^{d}$ classes (prenex classes of higher order logics) define FM-truth. For any $d \geq 2.m \geq 1$ we construct a family $\{[\Sigma_{m}^{d}]^{\leg\kappa}\}\kappa\in\omega$ of syntactically defined fragments of $\Sigma_{m}^{d}$ which satisfy this characterization. We also use the $[\Sigma_{m}^{d}]\leg\kappa$ classes to give a refinement of known results on the complexity classes captured by $\Sigma_{m}^{d}$ . We close with a few simple corollaries, one of which gives a sufficient condition for the existence, given a vocabulary $\sigma$ , of a fixed number $\kappa$ such that model checking for all first order sentences over $\sigma$ can be done in deterministic time $n^{\kappa}$. (shrink)

We use the Drozd-Warfield structure theorem for finitely presented modules over a serial ring to investigate the model theory of modules over a serial ring, in particular, to give a simple description of pp-formulas and to classify the pure-injective indecomposable modules. We also study the question of whether every pure-injective indecomposable module over a valuation ring is the hull of a uniserial module.