Quantifier Elimination for Neocompact Sets

H. Jerome Keisler

Abstract

We shall prove quantifier elimination theorems for neocompact formulas, which define neocompact sets and are built from atomic formulas using finite disjunctions, infinite conjunctions, existential quantifiers, and bounded universal quantifiers. The neocompact sets were first introduced to provide an easy alternative to nonstandard methods of proving existence theorems in probability theory, where they behave like compact sets. The quantifier elimination theorems in this paper can be applied in a general setting to show that the family of neocompact sets is countably compact. To provide the necessary setting we introduce the notion of a law structure. This notion was motivated by the probability law of a random variable. However, in this paper we discuss a variety of model theoretic examples of the notion in the light of our quantifier elimination results.

1 Introduction

A model is said to have (first order) elimination of quantifiers if every relation on the model which can be defined by a first order formula can be defined by a quantifierfree formula. Quantifier elimination theorems have been very useful in applications of model theory to algebra, particularly Tarski’s theorem that real closed ordered fields have elimination of quantifiers (see [Ta]). There have been spectacular recent advances in the subject concerning exponential functions and restricted analytic functions ([MW], [DMM]).

We shall obtain quantifier elimination theorems for certain infinitely long formulas in a very different setting, which we shall call a law structure because it is an abstraction of the law function in probability theory. Formally, a law structure is a family of functions λ from the Cartesian powers X^{n} of a set X into Hausdorff spaces Λ(X^{n}) where λ on X^{m} is related in a nice way to λ on X^{n}. Intuitively, one should think of λ(x⃗) as the type of x⃗—the collection of all properties of x⃗ which are expressible in some language. The notion was originally motivated by the example of the law structure on a probability space Ω, where X^{n} is the set of all random variables x⃗ : Ω → R^{n}, and λ(x⃗), the law of x⃗, is the measure on R^{n} induced by x⃗. The abstract notion was introduced in order to handle more complicated examples of law structures involving discrete time and continuous time adapted probability spaces, which will be developed in the companion paper [K4]. In this paper we shall prove the quantifier elimination results and interpret them in law structures which are associated with first order models.

In the paper [HK] we introduced the notion of a saturated probability space and an analogous notion for adapted probability spaces. These notions played a key role in the model theory of adapted probability logic (see [K1]). A probability or adapted space is saturated if it is atomless and has the following back and forth property: whenever x, x̄ ∈ X^{m}, y ∈ X^{n}, and λ(x) = λ(x̄), there exists ȳ ∈ X^{n} such that λ(x̄, ȳ) = λ(x, y). This property will play a central role in the general setting of this paper.

The papers [K2], [FK1], and [FK2] introduced another model theoretic method in probability theory, based on the notion of a neocompact set of random variables. An overall survey of this method is in [K3]. The neocompact sets in a law structure are the subsets of X^{n} which are definable by formulas built from basic formulas of the form λ(x⃗, b) ∈ C, where C is compact and b is a parameter, using countable conjunctions, finite disjunctions, existential quantifiers, and bounded universal quantifiers. Neocompact sets were used in [FK1] and [CK] to prove a variety of existence theorems in probability theory. In these existence theorems the neocompact sets play a role analogous to the compact sets in classical proofs. The results hold for probability or adapted spaces with the property that the intersection of any countable chain of nonempty neocompact sets is nonempty. Such spaces are called rich.

This paper was motivated by the problem of finding the connection between saturated and rich probability spaces. Our main results will be quantifier elimination theorems showing that for many law structures with the back and forth property, including those on probability spaces and on adapted spaces, the neocompact sets can be represented in a simple form. It will follow that the back and forth property, richness, and quantifier elimination are equivalent for these law structures. This theorem is the key fact needed in the paper [K2] to prove that saturated probability and adapted spaces are rich. Our general topological setting has other applications beyond the case of probability spaces which served as the original motivation.

In Section 2 we introduce law structures. Several examples of law structures from model theory, metric spaces, and probability theory are given in Section 3. In Section 4 we introduce the basic sets, which will correspond to atomic formulas in our language, and the basic sections, which correspond to atomic formulas with parameters. In Section 5 we prove two quantifier elimination theorems for neocompact formulas. The two theorems differ in the sets that can be used as bounds for the universal quantifiers. For the universal quantifier step these results require certain “open mapping” hypotheses in addition to the back and forth property. In Section 6 we take another look at the examples from Section 3 in the light of the quantifier elimination theorems. In Section 7 we extend one of the quantifier elimination theorems to the case that the open mapping hypothesis only holds locally.

I wish to thank Sergio Fajardo and Siu-Ah Ng for helpful suggestions on this article. This research was supported in part by the National Science Foundation and the Vilas Trust Fund.

2 Law Structures

In this section we shall introduce the notion of a law structure, which will serve as a framework for the quantifier elimination theorems later on in this paper.

To prepare the reader for our abstract definition, we first briefly describe two particular law structures which are familiar objects of study in model theory and in probability theory. We shall discuss these and other examples in more detail in Section 3.

First, let A be a model with universe A for a first order logic L with equality. For each n-tuple x⃗ ∈ A^{n}, let λ^{el}(x⃗) be the elementary type of x⃗, that is, the set of all formulas of L which are satisfied by x⃗ in A. The set Λ^{el}(A^{n}) of all elementary n-types for the complete theory T h(A) of A has a natural topology, the Stone space. Given a pair (x, y) of elements of A, the elementary type λ^{el}(x, y) of the pair will contain more information than the pair of elementary types (λ^{el}(x), λ^{el}(y)). The mapping λ^{el}(x, y) ↦ (λ^{el}(x), λ^{el}(y)) will be continuous and well-behaved but in general not be one-one.

As a second example, let Ω = (Ω, P, G) be an atomless probability space, and let X be the set of all measurable functions x : Ω → R. (The elements of X are called random variables on Ω). Then the n-tuples x⃗ ∈ X^{n} correspond to measurable functions from Ω into R^{n}. Each x⃗ ∈ X^{n} determines the Borel probability measure law(x⃗) on R^{n} where the measure of a Borel set S ⊆ R^{n} is equal to the probability P [x⃗(·) ∈ S]. The set of all Borel probability measures on R^{n} has a natural topology, called the topology of weak convergence. Given a pair (x, y) of random variables, the joint probability law law(x, y) will contain more information than the pair of “marginal” laws (law(x), law(y)). The mapping law(x, y) ↦ (law(x), law(y)) is a continuous function which is “well-behaved” but not one-one.

We shall now define the general notion of a law structure with the above examples as a guide.

Let M be a family of nonempty sets closed under finite Cartesian products, and let X, Y, Z denote arbitrary elements of M. A subset of a topological space Λ is relatively compact in Λ if it is contained in a compact subset of Λ. Given a function λ : A → Λ from a set A into a topological space Λ, λ(A) will denote the range of λ with the topology inherited from Λ, and λ̄(A) will denote the closure of λ(A) in Λ(A).

Definition 2.1 A law structure (M, λ, Λ) on M is an object which assigns to each X ∈ M a Hausdorff space Λ(X) and a function λ : X → Λ(X) such that:

(Identity Rule) If x, y, z ∈ X and λ(x, y) = λ(z, z) then x = y.

(Parameter Rule) For any set A ⊆ X ∈ M and element b ∈ Y ∈ M, λ(A × {b}) is relatively compact in Λ(X × Y) if and only if λ(A) is relatively compact in Λ(X).

(Projection Rule) Suppose

π : {1, …, k} → {1, …, m}, X_{1}, …, X_{m} ∈ M,

and F_{π} is the projection

F_{π}(x_{1}, …, x_{m}) = (x_{π1}, …, x_{πk}).

Then there is a continuous function

f_{π} : λ(X_{1} × ⋯ × X_{m}) → λ(X_{π1} × ⋯ × X_{πk})

such that the following diagram is commutative:

[figure: X_{1} × ⋯ × X_{m}; λ; λ(X_{1} × ⋯ × X_{m}); f_{π}; λ(X_{π1} × ⋯ × X_{πk}); F_{π}; λ; X_{π1} × ⋯ × X_{πk}]

Moreover, if π is a bijection then f_{π} is a homeomorphism.

We shall call the mapping f_{π} in the Projection Rule the projection map. One may intuitively think of λ(x) as the set of all properties of x expressible in

some language. The Identity Rule says that the language can express equality, and the Parameter and Projection Rules say that there is a nice relationship between the law of a pair λ(x, y) and the pair of laws (λ(x), λ(y)).

We shall sometimes suppress λ and write a law structure in the short form (M, Λ) instead of (M, λ, Λ). For each X ∈ M, we shall call λ(X) the image and Λ(X) the target space.

For each x ∈ X and each C ⊆ Y, let

λ(x, C) = λ({x} × C) = {λ(x, y) : y ∈ C},
λ(C, x) = λ(C × {x}) = {λ(y, x) : y ∈ C}.

For a set C ⊆ Λ(X) we use the notation

λ^{−1}(C) = {x ∈ X : λ(x) ∈ C}.

If U is open in Λ(X), we shall say that the inverse image λ^{−1}(U) is inverse open in X, and define inverse closed sets analogously.

Recall that a net is a family b_{ν}, ν ∈ N of points in Λ indexed by an upward directed set ⟨N, ≤⟩ (cf. Kelley [Ke]). A net b_{ν} converges to a point b if for each open neighborhood U of b there is a ν ∈ N such that b_{ρ} ∈ U whenever ν ≤ ρ. A point b belongs to the closure of a set A in Λ if and only if some net of points in A converges to b. A function f : Λ → Λ′ is continuous if and only if whenever a net b_{ν} converges to b, f(b_{ν}) converges to f(b).

We now introduce some properties of law structures.

Definition 2.2 In each of the following, (M, Λ) is a law structure and X, Y are arbitrary members of M.

(M, Λ) is said to be closed iff the image λ(X) is closed in the target space Λ(X) for all X ∈ M.

(M, Λ) is said to be complete iff λ(x, Y) is closed in the image λ(X × Y) for each x ∈ X ∈ M and Y ∈ M.

(M, Λ) has the back and forth property iff whenever x, x̄ ∈ X and λ(x) = λ(x̄), we have λ(x, Y) = λ(x̄, Y). That is, if λ(x) = λ(x̄) then for every y ∈ Y there exists ȳ ∈ Y such that λ(x, y) = λ(x̄, ȳ).

(M, Λ) is said to be dense iff whenever x, x̄ ∈ X, and λ(x) = λ(x̄), the sets λ(x, Y) and λ(x̄, Y) have the same closure in λ(X × Y).

(M, Λ) has the open mapping property iff for each X ∈ M, the projection map from λ(X × Y) to λ(X) is open.

(M, Λ) has the strong (open) mapping property iff for each X ∈ M and y ∈ Y ∈ M, the projection map from λ(X, y) to λ(X) is open.

(M, Λ) is total iff it has all the above properties.

Notice that the only properties introduced in Definition 2.2 which mention the target space Λ(X) are being closed and being total; all the other properties involve the images λ(X) rather than the possibly larger target spaces Λ(X).

We remark that if (M, Λ) is closed and complete then λ(x, Y) is closed in the target space Λ(X × Y) for each x ∈ X ∈ M and Y ∈ M. Also, the strong mapping property implies the open mapping property.

Proposition 2.3 (M, Λ) has the back and forth property if and only if (M, Λ) is complete and dense.

Proof: Suppose (M, Λ) has the back and forth property. (M, Λ) is dense because given x, x̄ ∈ X with λ(x) = λ(x̄), the sets λ(x, Y) and λ(x̄, Y) are equal and thus have the same closures. To prove that (M, Λ) is complete, let λ(x, y_{ν}) converge to λ(x̄, ȳ). By the Projection Rule, λ(x) = λ(x̄). By the back and forth property there exists y ∈ Y such that λ(x, y) = λ(x̄, ȳ), as required.

Now assume that (M, Λ) is complete and dense. Let x, x̄ ∈ X with λ(x) = λ(x̄), and let y ∈ Y. By density the sets λ(x, Y) and λ(x̄, Y) have the same closure. Thus there exist y_{ν} ∈ Y such that λ(x̄, y_{ν}) converges to λ(x, y). By completeness there exists ȳ ∈ Y such that λ(x̄, y_{ν}) converges to λ(x̄, ȳ), and hence λ(x̄, ȳ) = λ(x, y). Therefore (M, Λ) has the back and forth property. □

Corollary 2.4 A law structure is total if and only if it is closed and has the back and forth and strong mapping properties. □

Here is a natural sufficient condition for the strong mapping property.

Proposition 2.5 Suppose (M, Λ) has the back and forth property and for each X and Y, the map h : λ(X × Y) → λ(X) × λ(Y) is open, where f : λ(X × Y) → λ(X) and g : λ(X × Y) → λ(Y) are the projections and h(c) = (f(c), g(c)). Then (M, Λ) has the strong mapping property.

Proof: Let (x, y) ∈ X × Y, and let U be an open neighborhood of λ(x, y) in λ(X, y). Then U = U′ ∩ λ(X, y) for some open set U′ ⊆ λ(X × Y). By hypothesis there is an open neighborhood V of h(λ(x, y)) = (b, c) such that V′ ⊆ h(U′). Then the section V = {b̄ : (b̄, c) ∈ V′} of V′ is an open neighborhood of f(λ(x)) = b in λ(X). Let b̄ ∈ V. Then (b̄, c) = h(a) for some a = (λ(x′, y′)) ∈ U′. We have λ(y′) = g(a) = c = λ(y), and by density there exists x” such that λ(x”, y) = a. Thus a ∈ U and f(a) = b̄, so V ⊆ f(U) as required. □

We conclude this section with the notion of an isomorphism between two law structures on the same M.

Definition 2.6 Let (M, λ, Λ) and (M, λ′, Λ′) be two law structures with the same M. By an isomorphism F from (M, λ, Λ) to (M, λ′, Λ′) we mean a family of homeomorphisms

F_{X} : λ̄(X) → λ̄′(X), X ∈ M

such that whenever x ∈ X ∈ M, F_{X}(λ(x)) = λ′(x). (M, λ, Λ) and (M, λ′, Λ′) are isomorphic if there is an isomorphism from one to the other.

Notice that any law structure (M, λ, Λ) is isomorphic to the law structure (M, λ, Λ′) which is formed by replacing each space Λ(X) by the closure of the image of X, so that Λ′(X) = λ̄(X). The next proposition is easily checked.

Proposition 2.7 Suppose (M, Λ) and (M, Λ′) are isomorphic law structures. Then each of the properties introduced in Definition 2.2 holds for (M, Λ) if and only if it holds for (M, Λ′). □

3 Examples of Law Structures

In this section we shall look at some examples of law structures. Several of these examples will be constructed from an arbitrary model A for a first order logic. Given A, M_{A} will be the set of all finite powers of the universe set A of A.

Example 1 (Identity law structure)

The identity law structure is the triple (M, λ, Λ) where M is the family of all Hausdorff spaces, Λ(X) = X, and λ is the identity function on each X ∈ M. The identity law structure is obviously total. All of our results in this paper will be very easy in the case of the identity law structure.

Example 2 (Elementary types)

Given a model A for a first order vocabulary L with equality, let Λ^{el}(A^{n}) be the Stone space of elementary types of n-tuples in the complete theory T h(A) of A (so that the set of all elementary types satisfying a formula is a basic clopen set). For a⃗ ∈ A^{n} let λ^{el}(a⃗) be the elementary type of a⃗. Then for each n, Λ^{el}(A^{n}) is a compact Hausdorff space, and the image λ^{el}(A^{n}) is a dense subset.

(M_{A}, Λ^{el}) is a law structure.

Here are model-theoretic necessary and sufficient conditions for (M_{A}, Λ^{el}) to have the properties introduced in Definition 2.2

Density: Always.

Hint: Use the fact that A ⊧ φ(a⃗, b⃗) implies A ⊧ ∃v⃗φ(a⃗, v⃗).

Open mapping: Always.

Closed: A realizes all n-types of T h(A).

Closed and Complete: A is ω-saturated.

Back and forth: A is ω-homogeneous in the usual model theoretic sense.

Strong mapping: A is an atomic model, that is, every elementary n-type realized in A is isolated. (Hint: For each a⃗ ∈ A^{n}, λ^{el}(a⃗, a⃗) is isolated in λ^{el}(A^{n}, a⃗) by the formula ⋀_{i<n} v_{i} = v_{i}. The strong mapping property implies that the point λ^{el}(a⃗) is isolated in λ^{el}(A^{n}).)

Total: For each n, there are only finitely many elementary n-types over A. (This implies that either A is finite or T h(A) is ω-categorical; if L is at most countable and A is infinite, this is equivalent to ω-categoricity.)

Since (M_{A}, Λ^{el}) is always dense, it is complete if and only if it has the back and forth property. Every model has an elementary extension A such that (M_{A}, Λ^{el}) is closed and complete, since every model has an ω-saturated elementary extension. If L is at most countable, then the target spaces Λ(A^{n}) will have countable bases.

Example 3 (Quantifier-free types)

Given a model A for a first order vocabulary L with equality, a quantifier-free n-type over A is a set of quantifier-free (first order) formulas in the first n variables which is maximal finitely satisfiable in A. For each n ∈ N, let Λ^{qf}(A^{n}) be the Stone space of all quantifier-free n-types over A. This is the topology in which the set of all quantifier-free types containing a quantifier-free formula is a basic clopen set. Each a⃗ ∈ A^{n} realizes a quantifier-free n-type λ^{qf}(a⃗) over A. For each n, Λ^{qf}(A^{n}) is a compact Hausdorff space, and the image λ^{qf}(A^{n}) is dense in Λ^{qf}(A^{n}).

(M_{A}, Λ^{qf}) is a law structure.

Here are model-theoretic necessary and sufficient conditions for some of the properties from Definition 2.2 in (M_{A}, Λ^{qf}).

Closed: Every quantifier-free n-type over A is realized in A.

Complete: For any a⃗ ∈ A^{m}, every quantifier-free n-type which is finitely satisfiable in (A, a⃗) and is realized in (A, b⃗) for some b⃗ ∈ A^{m} is realized in (A, a⃗).

Closed and complete: For any a⃗ ∈ A^{m}, every quantifier-free n-type which is finitely satisfiable in (A, a⃗) is realized in (A, a⃗).

Dense: For each m, any two m-tuples which satisfy the same quantifier-free formulas in A also satisfy the same existential (or universal) formulas in A.

Back and forth: If a⃗ and b⃗ satisfy the same quantifier-free formulas in A then they satisfy the same L_{∞ω} formulas in A.

Dense and open mapping: For each a⃗ ∈ A^{m} and quantifier-free formula φ(x⃗, y⃗) in m + n variables, if A ⊧ ∃y⃗ φ(a⃗, y⃗) then there is a quantifier-free formula ψ(x⃗) such that

A ⊧ ψ(a⃗) ∧ ∀x⃗(ψ(x⃗) → ∃y⃗ φ(x⃗, y⃗)).

Strong mapping: Each quantifier-free n-type is realized in A if and only if it is isolated in Λ^{qf}(A^{n}).

Total: T h(A) admits first order elimination of quantifiers and has finitely many elementary n-types for each n.

Here are some consequences:

If (M_{A}, Λ^{qf}) has the strong mapping property then it is complete.

(M_{A}, Λ^{qf}) is closed and has the strong mapping property if and only if there are only finitely many quantifier-free n-types over A for each n.

If T h(A) admits first order elimination of quantifiers, then (M_{A}, Λ^{qf}) is isomorphic to (M_{A}, Λ^{el}), and is dense and has the open mapping property by Example 2.

Note that if (M_{A}, Λ^{el}) is closed then (M_{A}, Λ^{qf}) is closed. If (M_{A}, Λ^{el}) is closed and complete, then A is ω-saturated and thus (M_{A}, Λ^{qf}) is closed and complete. But, for example, if A is a linear order of type ω^{∗}+ω+ω^{∗}+ω (two copies of Z), then (M_{A}, Λ^{qf}) is closed and complete while (M_{A}, Λ^{el}) is neither closed nor complete.

We shall return to the example of the law structures of quantifier-free types in Section 6, where we shall apply a general quantifier elimination theorem to (M_{A}, Λ^{qf}).

Example 4 (Types in infinitely many variables)

This example is like the preceding example but with types in infinitely many variables. Let κ be an infinite cardinal and work with a first order logic with κ variables.

Given a model A, let MA^{κ} be the set of all Cartesian powers A^{α} of A where α < κ. We identify A^{α} × A^{β} with A^{α+β}. For each α < κ, Λ^{qf}(A^{α}) is the Stone space of quantifier-free α-types over A, where the basic clopen sets are determined by single finite quantifier-free formulas. This is a compact Hausdorff space. For a⃗ ∈ A^{α}, λ^{qf}(a⃗) is the quantifier-free α-type of a⃗ over A.

(MA^{κ}, Λ^{qf}) is a law structure.

Example 5 (Quantifier-free types with restricted topology)

We can get a wider variety of law structures from first order models by allowing the target space to be a subspace of the Stone space with the restricted topology. In this example we consider the case where the target space is as small as possible–the target space is the image of the mapping λ.

As in Example 3, we let A be a model for a first order vocabulary L with equality and for each a⃗ ∈ A^{n}, λ^{qf}(a⃗) is the quantifier-free type of a⃗ in A. But this time we define the target space Λ^{rst}(A^{n}) to be the image λ^{qf}(A^{n}) with the restricted topology of the Stone space. Thus the basic clopen sets are the sets of all quantifier-free ntypes which are realized in A and contain a given quantifier-free formula.

In this case, the triple (M_{A}, λ^{qf}, Λ^{rst}) will not necessarily be a law structure. The target spaces will always be Hausdorff spaces, and the Projection and Identity Rules will always hold. However, the Parameter Rule will depend on the model A.

Lemma 3.1 A set B ⊆ A^{n} has a relatively compact image λ^{qf}(B) in Λ^{rst}(A^{n}) if and only if every quantifier-free n-type which is finitely satisfiable by tuples in B is realized in A.

Proof: Since Λ^{rst}(A^{n}) is a subspace of the compact space Λ^{qf}(A^{n}), the set λ^{qf}(B) is relatively compact if and only if its closure in Λ^{qf}(A^{n}) is contained in Λ^{rst}(A^{n}). A quantifier-free n-type p belongs to the closure of λ^{qf}(B) if and only if it is finitely satisfiable by tuples in B, and belongs to Λ^{rst}(A^{n}) if and only if it is realized in A. □

Proposition 3.2 (M_{A}, Λ^{rst}) satisfies the Parameter Rule, and thus is a law structure, if and only if whenever B ⊆ A^{m} and every quantifier-free m-type over A which is finitely satisfiable by tuples in B is realized in A, then for each n and c ∈ A^{n}, every quantifier-free m+n-type over A which is finitely satisfiable by tuples in B ×{c} is realized in A.

Proof: By the preceding lemma. □

If (M_{A}, Λ^{rst}) is a law structure, then it is automatically closed. (M_{A}, Λ^{rst}) is complete, dense, has the back and forth property, the open mapping property, or the strong mapping property, if and only if (M_{A}, Λ^{qf}) has that property. Thus the necessary and sufficient conditions for these properties given in Example 3 are also valid in this case. The following proposition shows when (M_{A}, Λ^{rst}) is a total law structure.

Proposition 3.3 (M_{A}, Λ^{rst}) is a total law structure if and only if it has the back and forth property, each Λ^{rst}(A^{n}) has the trivial topology where every set is open, and whenever C ⊆ A^{m} and λ^{qf}(C) is finite, λ^{qf}(C × {d}) is finite for all n and d ∈ A^{n}.

Proof: (M_{A}, Λ^{rst}) has the strong mapping property iff (M_{A}, Λ^{qf}) has the strong mapping property iff every quantifier-free n-type realized in A is isolated in Λ^{qf}(A^{n}). Λ^{rst}(A^{n}) is dense in Λ^{qf}(A^{n}), so a point is isolated in Λ^{rst}(A^{n}) if and only if it is isolated in Λ^{qf}(A^{n}). Thus (M_{A}, Λ^{rst}) has the strong mapping property if and only if Λ^{rst}(A^{n}) has the trivial topology. In the trivial topology, a set is relatively compact if and only if it is finite. Thus if the target spaces of (M_{A}, Λ^{rst}) have the trivial topology, the Parameter Rule holds if and only if whenever C ⊆ A^{m} and λ^{qf}(C) is finite, λ^{qf}(C × {d}) is finite for all n and d ∈ A^{n}. The result now follows from Corollary 2.4. □

The next proposition shows that the key properties for the law structures (M_{A}, Λ^{rst}) are preserved under unions of directed families of quantifier-free definable submodels, and thus can arise in models which omit quantifier-free types.

Proposition 3.4 Suppose that the model A is the union of an upward directed family of submodels A_{i}, i ∈ I such that for each i ∈ I, the universe of A_{i} is defined by a quantifier-free formula without parameters, and (M_{A_{i}}, Λ^{rst}) is a law structure with the back and forth property. Then:

(i) A is a law structure with the back and forth property.

(ii) If each (M_{A_{i}}, Λ^{rst}) has the open mapping property, then (M_{A}, Λ^{rst}) has the open mapping property.

(iii) If each (M_{A_{i}}, Λ^{rst}) is total, then (M_{A}, Λ^{rst}) is total.

Proof sketch: The set of formulas {¬A_{i}(v) : i ∈ I} is not realized in A. It follows that whenever C ⊆ A and λ(C) is relatively compact, C ⊆ A_{i} for some i ∈ I. Now use Proposition 3.2 to show that (M_{A}, Λ^{rst}) is a law structure. The back and forth property is easily verified. Use the criterion in Example 3 to prove (ii), and use Proposition 3.3 to prove (iii). □

The property of being total is a very severe restriction for law structures of the form (M_{A}, Λ^{rst}), since it forces the topology of the target space to be trivial. However, more interesting total law structures can arise in other settings (see the next two examples). We can get a some additional total law structures from first order models by allowing languages without equality.

If A be a model for a first order vocabulary L without equality, we define (M_{A}, λ^{qf}, Λ^{rst}) as before. In this case, the target spaces will always be Hausdorff spaces, and the Projection Rule will always hold, but both the Identity Rule and the Parameter Rule will depend on the model A.

The following exercise gives one way of constructing total law structures associated with models without equality.

Exercise: For each i ∈ I, let A_{i} be a model for a vocabulary L with equality. Form a new vocabulary L^{I} without equality by replacing each predicate symbol P of L, including the equality symbol, by a family of predicate symbols {P_{i} : i ∈ I} with the same arity as P. Let A = ∏_{i∈I} A_{i} be the model with vocabulary L^{I} without equality where the universe ∏_{i∈I} A_{i} and the function symbols are defined as is the full direct product of the models A_{i}, and each P_{i} is interpreted in A by the rule A ⊧ P_{i}(a⃗) iff A_{i} ⊧ P (a⃗(i)). Assume that for each i, (M_{A_{i}}, Λ^{rst}) is a total law structure. Prove that (M_{A}, Λ^{rst}) is a total law structure.

Hint: For a⃗ ∈ A^{n}, the quantifier-free type λ^{qf}(a⃗) can be identified with the family of types ⟨λ^{qf}(a⃗(i)) : i ∈ I⟩, and Λ^{rst}(A^{n}) may be identified with the topological product of the spaces Λ^{rst}((A_{i})^{n}).

Example 6 (Metric models)

In this example we shall associate a law structure with a metric space with additional continuous functions. This law structure will have the same relationship to the metric space model theory of Henson and Iovino [HI] as the law structure of quantifier-free types has to classical first order model theory. Baratella and Ng [BN] studied this law structure in detail in the case of Hilbert and Banach spaces, and applied the methods of this paper to obtain quantifier elimination results.

Let E = (E, ρ, c) be a metric space with a distinguished point c, and let R = (R, 0, 1, +, −, ∗, ≤) be the ordered field of real numbers. By a metric model over E we shall mean a structure

A = ⟨E, R, f_{i} : i ∈ I⟩

with a sort for the metric space E and a sort for the ordered field of reals R, and symbols for continuous functions f_{i} : E^{j} ×R^{k} → E or f_{i} : E^{j} ×R^{k} → R. In addition to the function symbols f_{i},, the vocabulary for A also has the symbols of E and R— the metric function ρ : E × E → R, the constant c, and the symbols 0, 1, +, −, ×, ≤ of R.

Banach spaces with function symbols for vector addition, scalar multiplication, and the norm, and Hilbert spaces with the Banach space function symbols and a symbol for the inner product, are examples of metric models.

We define the notion of a bounded (m, n)-type over A, define a topology on the set of bounded (m, n)-types, and use these topologies as the target spaces for a law structure.

It will be convenient to add an absolute value symbol | · | and let |u| ≤ K stand for the formula ρ(u, c) ≤ K if u has sort E and for −K ≤ u ∧ u ≤ K if u has sort R. For each natural number K, the particular set of formulas

|x⃗| ≤ K = {|x_{1}| ≤ K, …, |x_{m}| ≤ K},

which says that the x⃗ is bounded by K, plays a special role.

By an approximation of a positive quantifier-free formula φ we mean a formula obtained from φ by replacing each inequality σ ≤ τ in φ by a weaker inequality σ ≤ τ + r where r is a positive rational. A positive quantifier-free formula is approximable in A if each approximation of the formula is satisfiable in A.

Let M_{A} be the set of all finite Cartesian products E^{m} × R^{n}, m, n ∈ N, and let v⃗ have sort (m, n). We allow the possibility that m or n is zero. By a bounded (m, n)-type over A we mean a set p(v⃗) of positive quantifier-free formulas which contains |v⃗| ≤ K for some K ∈ N and which is maximal with respect to the property that every finite subset is approximable in A. We let Λ(E^{m} × R^{n}) be the set of all bounded (m, n)-types over A.

Give Λ(X) the topology whose basic closed sets are the sets of all bounded (m, n)- types which contain a given positive quantifier-free formula. For each a⃗ ∈ X ∈ M_{A}, let λ(a⃗) be the set of all positive quantifier-free formulas satisfied by a⃗ in A.

Proposition 3.5 If A is a metric model then (M_{A}, Λ) is a law structure.

Proof sketch: First show that each λ(x) is a bounded type, so the functions λ : X → Λ(X) are well-defined. Then show that Λ(X) is Hausdorff. To prove the Parameter Rule, show that for each B ⊆ X ∈ M_{A}, the image λ(B) is relatively compact if and only if B is bounded. □

In the literature (see [He], [HI]), metric structures are usually required to be uniformly continuous on bounded sets in the following sense. We say that a metric model A is uniformly continuous on bounded sets iff for each function symbol f and each K ∈ N, f is bounded and uniformly continuous on {a⃗ : |a⃗| ≤ K}.

Uniform continuity on bounded sets was not needed in order to prove that (M_{A}, Λ) is a law structure. However, it is needed in order to extend A to a metric model H whose law structure is closed and complete but has the same target spaces as (M_{A}, Λ). Such an extension can be built using the nonstandard hull construction, which is a basic tool in the model theory of Banach spaces (see Henson [He]). The following is a law structure reformulation of a well-known result.

Proposition 3.6 Let A be a metric model. The following are equivalent. (i) A is uniformly continuous on bounded sets. (ii) A has an extension H whose law structure (M_{H}, Λ) is closed and complete

and has the same target spaces as (M_{A}, Λ). □

Corollary 3.7 If A is a metric model whose law structure (M_{A}, Λ) is closed, then A is uniformly continuous on bounded sets.

Proof: If A is not uniformly continuous on bounded sets, then there is a bounded type over A which is not realized in any metric model. □

The paper [BN] showed that the law structures for Hilbert spaces are total, and investigated the properties of the law structures for nonstandard hulls of Banach spaces.

Example 7 (Random variables)

This is the example which originally motivated our work. Let Ω = (Ω, P, G) be an atomless probability space. For each complete separable metric space (M, ρ), let M = (L^{0}(Ω, M), ρ_{0}) be the metric space of all equivalence classes of P -measurable functions from Ω into M. Here two functions are equivalent if they are equal P - almost surely, and ρ_{0} is the metric of convergence in probability on M,

ρ_{0}(x, y) = inf{ε : P [ρ(x(ω), y(ω)) ≤ ε] ≥ 1 − ε}.

The product topology M × N of two complete separable metric spaces M and N again has a complete separable metric, and with this metric L^{0}(Ω, M × N) has the same topology as L^{0}(Ω, M) × L^{0}(Ω, N).

We let M_{Ω} be the family of all metric spaces M = (L^{0}(Ω, M), ρ_{0}) where M is a complete separable metric space. We form a law structure where λ(x) is the law of x, that is, the measure on M induced by x. In order to fit this into our framework we need λ(x) to be an element of an appropriate topological space Λ(M). The space of Borel probability measures on M with the Prohorov metric

d(μ, ν) = inf{ε : μ(C) ≤ ν(C^{ε}) + ε for all closed C ⊆ M}

is again a complete separable metric space, denoted by Meas(M). We take Λ(M) = Meas(M). Convergence in Meas(M) is the same as weak convergence (e.g. see [Bi]).

Each measurable function x : Ω → M induces a measure law(x) ∈ Meas(M), where

(law(x))(S) = P [x^{−1}(S)].

The function

law : L^{0}(Ω, M) → Meas(M)

is uniformly continuous, and in fact,

d(law(x), law(y)) ≤ ρ_{0}(x, y).

This example is developed in detail in [K4]. We show in that paper that for every atomless probability space Ω, (M_{Ω}, law, Meas) is a closed dense law structure with the strong mapping property, and the law function maps L^{0}(Ω, M) onto Meas(M) for every complete separable M. Thus (M_{Ω}, law, Meas) is complete if and only if it has the back and forth property, and also if and only if it is total.

Examples of atomless probability spaces (Ω, P, G) such that (M_{Ω}, law, Meas) is or is not total are given in the papers [HK] and [K4]. It is shown in [HK] that if Ω is an uncountable power of Lebesgue measure on [0, 1], or if Ω is an atomless Loeb probability space, then (M_{Ω}, law, Meas) has the back and forth property and thus is total. On the other hand, it is shown in [K4] that if Ω is a separable metric space and G is the σ-algebra of Borel subsets of Ω (or its P -completion, as in the case of Lebesgue measure), then (M_{Ω}, law, Meas) does not have the back and forth property and thus is not total.

As we indicated in the introduction, our principal motivation in this research was to develop tools for studying adapted probability spaces, which are probability spaces with the additional structure of a family of increasing σ-algebras indexed by time. There are law structures associated with adapted probability spaces where λ is the adapted law of [HK]. These law structures are considered in the sequel [K4] of this paper. As in the case of probability spaces, adapted Loeb spaces give rise to total law structures.

4 Basic Sections

In this section we shall study the family of basic sections for a law structure (M, Λ).

Definition 4.1 A set B ⊆ X is basic for a law structure (M, Λ) if B is of the form B = λ^{−1}(B̂) for some compact subset B̂ of Λ(X).

Definition 4.2 Let z ∈ Z. A set C ⊆ X is called a basic section with parameter z if C has the form

C = {x ∈ X : λ(x, z) ∈ Ĉ}

for some compact subset Ĉ of Λ(X × Z).

We remark that if B is basic, x ∈ B, and λ(x̄) = λ(x), then x̄ ∈ B. Similarly, if B is a basic section with parameter z, x ∈ B, and λ(x̄, z) = λ(x, z), then x̄ ∈ B.

Proposition 4.3 For every basic section C ⊆ X, the image λ(C) is relatively compact in Λ(X).

Proof: Let C be the basic section

C = {x ∈ X : λ(x, z) ∈ Ĉ}

where Ĉ is compact. Then λ(C × {z}) is a subset of Ĉ, and hence is relatively compact. By the Parameter Rule, λ(C) is relatively compact. □

Proposition 4.4 For every z ∈ Z, every basic set for (M, Λ) is a basic section with parameter z.

Proof: Let B = λ^{−1}(B̂) be a basic set where B̂ is compact. Let Ĉ be the closure of the set λ(B, z). By the Parameter Rule, λ(B, z) is relatively compact, so Ĉ is compact. We show that B is the basic section

B = {x ∈ X : λ(x, z) ∈ Ĉ}.

It is clear that B is contained in the right side. Suppose λ(x, z) ∈ Ĉ. Then there is a net x_{ν} in B such that λ(x_{ν}, z) converges to λ(x, z). By the Projection Rule, λ(x_{ν}) converges to λ(x). Since x_{ν} ∈ B, λ(x_{ν}) ∈ B̂, and therefore λ(x) ∈ B̂ and x ∈ B. □

Proposition 4.5 (i) Let y ∈ Y and z ∈ Z. Every basic section B ⊆ X with parameter y is a basic section with parameter (y, z).

(ii) If A ⊆ X and B ⊆ X are basic sections then A ∩ B and A ∪ B are basic sections.

Proof: The proof of (i) is the same as in the preceding lemma, but carrying the extra parameter y along. To prove (ii), we observe that by (i) we may assume that A and B both have the same parameter, say z ∈ Z. Then

A = {x ∈ X : λ(x, z) ∈ Â}, B = {x ∈ X : λ(x, z) ∈ B̂},

where Â and B̂ are compact. Then

A ∩ B = {x ∈ X : λ(x, z) ∈ Â ∩ B̂},

which is again a basic section, and similarly for A ∪ B. □

Proposition 4.6 For each X ∈ M, every finite subset A = {x_{1}, …, x_{m}} of X is a basic section with parameter z = (x_{1}, …, x_{m}) in the Cartesian power Z = X^{m}.

Proof: Let Â be the finite (and hence compact) set

Â = {λ(x_{i}, z) : i = 1, …, m}.

If x ∈ A then obviously λ(x, z) ∈ Â. Conversely, if λ(x, z) = λ(x_{i}, z) ∈ Â, then by the Projection Rule we have λ(x, x_{i}) = λ(x_{i}, x_{i}), and hence x = x_{i} ∈ A by the Identity Rule. □

Since finite unions and arbitrary intersections of compact sets are compact, we see that for each X ∈ M the family of basic subsets of X is closed under finite unions and arbitrary intersections. Moreover, for each z ∈ Z, the family of basic sections B ⊆ X with parameter z is closed under finite unions and arbitrary intersections. We now consider finite Cartesian products of basic sets.

Proposition 4.7 (i) If B ⊆ X and C ⊆ Y are basic sets and λ(B ×C) is relatively compact, then B × C is a basic set in X × Y.

(ii) If B ⊆ X and C ⊆ Y are basic sections with parameter z ∈ Z and λ(B × C) is relatively compact, then B × C is a basic section in X × Y with parameter z.

(iii) Let B ⊆ X × Z and C ⊆ Y × Z be basic sets, and let

D = {(x, y, z) ∈ X × Y × Z : (x, z) ∈ B and (y, z) ∈ C}.

If λ(D) is relatively compact then D is a basic set.

Proof: (i) and (ii) follow easily from (iii). We prove (iii). We have

B = λ^{−1}(B̂), C = λ^{−1}(Ĉ),

where B̂ and Ĉ are compact. Let D̂ be the closure of λ(D). λ(D) is relatively compact by hypothesis, so D̂ is compact. We show that

D = λ^{−1}(D̂).  (1)

It is clear that D ⊆ λ^{−1}(D̂). Suppose (x, y, z) ∈ λ^{−1}(D̂), that is, d = λ(x, y, z) ∈ D̂. Then some net d_{ν} converges to d in λ(D). For each ν, choose (x_{ν}, y_{ν}, z_{ν}) ∈ D such that λ(x_{ν}, y_{ν}, z_{ν}) = d_{ν}. Then (x_{ν}, z_{ν}) ∈ B and (y_{ν}, z_{ν}) ∈ C, so λ(x_{ν}, z_{ν}) ∈ B̂, λ(y_{ν}, z_{ν}) ∈ Ĉ. By the Projection Rule, λ(x_{ν}, z_{ν}) converges to λ(x, z), and λ(y_{ν}, z_{ν}) converges to λ(y, z). Therefore λ(x, z) ∈ B̂ and λ(y, z) ∈ Ĉ. Hence (x, z) ∈ B and (y, z) ∈ C, so (x, y, z) ∈ D. □

Corollary 4.8 If B is a basic section with parameter y, then B × {z} is a basic section with parameter (y, z). □

Proposition 4.9 (i) If (M, Λ) is closed then λ(A) is compact for every basic set A.

(ii) If (M, Λ) is closed and complete then for every basic section B ⊆ X, λ(B) is compact in Λ(X).

Proof: (i) Let A ⊆ X be the basic set A = λ^{−1}(Â) where Â in compact in Λ(X). Then λ(A) = Â ∩ λ(X). Since (M, Λ) is closed, the image λ(X) is closed, so Â ∩ λ(X) is compact.

(ii) Let B be the basic section

B = {x ∈ X : λ(x, z) ∈ Â}

where Â is compact. By Proposition 4.3 and Corollary 4.8, the closures λ̄(B) and λ̄(B, z, z) are compact. We must show that λ̄(B) = λ(B).

By hypothesis the sets λ(X × Z, z), and λ(X, z, z) are closed in their target spaces. We have B × {z} ⊆ A where A is the basic set A = λ^{−1}(Â). Thus

λ̄(A, z) ⊆ λ(X × Z, z),
λ̄(B, z, z) ⊆ λ(X, z, z) ∩ λ̄(A, z).

By the projection rule, the projection function continuously maps λ(X, z, z) onto λ(X). Therefore the projection maps the compact set λ̄(B, z, z) onto λ̄(B). Similarly, the projection maps the compact set λ̄(A, z) onto λ̄(A). By part (i), λ̄(A) = λ(A).

Let b ∈ λ̄(B, z, z). Then there exist x, x′ ∈ X and z′ ∈ Z such that

b = λ(x, z, z) = λ(x′, z′, z) ∈ λ̄(A, z).

It follows that (x′, z′) ∈ A. By the Projection Rule, λ(z, z) = λ(z′, z), and thus by the Identity Rule, z′ = z. Therefore (x′, z) ∈ A and hence x′ ∈ B. Thus the projection λ(x′) of b belongs to λ(B). This shows that λ(B) = λ̄(B) as required. □

Definition 4.10 We say that a family A of sets is compact iff every subsets of A which has the finite intersection property has a nonempty intersection.

Proposition 4.11 (i) If (M, Λ) is closed then for each X ∈ M, the family of basic sets B ⊆ X is compact.

(ii) If (M, Λ) is closed and complete then for each X, Z ∈ M and z ∈ Z, the family of basic sections B ⊆ X with parameter z is compact.

Proof: We prove (ii); the proof of (i) is similar. Let {C_{i} : i ∈ I} be a set of basic sections in X with parameter z with the finite intersection property. The sets C_{i} have the form

C_{i} = {x ∈ X : λ(x, z) ∈ Ĉ_{i}}

where Ĉ_{i} is compact. By Corollary 4.8, each product C_{i} × {z} is a basic section, and by Proposition 4.9 each image B̂_{i} = λ(C_{i}, z) is compact. This set has the finite intersection property. Therefore there is a point b ∈ ⋂_{i∈I} B̂_{i}. Then b = λ(x, z) for some x ∈ X. For each i ∈ I we have B̂_{i} ⊆ Ĉ_{i}, so b ∈ Ĉ_{i} and x ∈ C_{i}. □

A Hausdorff space is said to be a k-space, or to be compactly generated, if whenever A ∩ C is closed for every compact set C, then A is closed (e.g. see Kelley [Ke]). For example, each first countable space, and each locally compact space, is compactly generated. Let us call a law structure (M, Λ) compactly generated if each of its target spaces is compactly generated.

Remark 4.12 If (M, Λ) is compactly generated, then the converse holds for each part of Propositions 4.9 and 4.11. □

5 Elimination of Quantifiers

The following result will give the existential step for each of our quantifier elimination theorems. It shows that the back and forth property for a closed law structure is equivalent to the closure of the family of basic sets under existential projection.

Theorem 5.1 For any law structure (M, Λ), (i) implies (ii) and (ii) implies (iii). (i) (M, Λ) is closed and has the back and forth property. (ii) For every basic set A ⊆ X × Y, the set

B = {x ∈ X : (∃y ∈ Y)(x, y) ∈ A}  (2)

is basic.

(iii) (M, Λ) has the back and forth property.

Proof: Assume (i). Let A ⊆ X × Y be basic and B be the set defined in equation (2). By Proposition 4.9, λ(A) is compact. Let f : λ(X × Y) → λ(X) be the projection map which is continuous by the Projection Rule. The image B̂ = f(λ(A)) is compact. We show that B is the basic set

B = λ^{−1}(B̂).  (3)

If x ∈ B, then (x, y) ∈ A for some y ∈ Y, whence λ(x, y) ∈ λ(A) and λ(x) = f(λ(x, y)) ∈ B̂. On the other hand, if λ(x) ∈ B̂, then there exists (x̄, ȳ) ∈ A such that λ(x̄) = λ(x). Since (M, Λ) has the back and forth property, there exists y ∈ Y such that λ(x, y) = λ(x̄, ȳ). Thus (x, y) ∈ A and x ∈ B. This proves (3). Thus B is basic and (ii) holds.

Now assume (ii). Let x, x̄ ∈ X, y ∈ Y, and λ(x) = λ(x̄). Then the set

C = λ^{−1}({λ(x, y)})

is basic, and by (ii) the set

D = {x′ ∈ X : (∃y′ ∈ Y)(x′, y′) ∈ C}

is basic. Since x ∈ D and λ(x) = λ(x̄), we have x̄ ∈ D, and thus there exists ȳ ∈ Y such that λ(x̄, ȳ) = λ(x, y). This proves (iii). □

We now turn to the universal quantifier. The following easy lemma shows that the universal quantifier over Y is trivial unless λ(Y) is relatively compact. Since we do not wish to restrict our attention to the case that the target spaces λ(Y) are relatively compact, we shall allow bounded universal quantifiers (∀y ∈ C) as well as ordinary universal quantifiers over Y.

Lemma 5.2 Let A be a basic subset of X × Y. If the universal projection

B = {x ∈ X : (∀y ∈ Y)(x, y) ∈ A}

is nonempty then λ(Y) is relatively compact.

More generally, if C ⊆ Y and the universal projection

D = {x ∈ X : (∀y ∈ C)(x, y) ∈ A}

is nonempty then λ(C) is relatively compact.

Proof: Suppose D is nonempty and take x ∈ D. Then C is a subset of the basic section {y ∈ Y : (x, y) ∈ A}. By Proposition 4.3, λ(C) is relatively compact. □

The following theorem shows that density with the open mapping property implies the closure of the family of basic sets under universal projections bounded by inverse open sets.

Theorem 5.3 Let (M, Λ) be a law structure. If (M, Λ) is dense and has the open mapping property, then for each basic set A ⊆ X × Y and nonempty inverse open set C ⊆ Y, the set

D = {x ∈ X : (∀y ∈ C)(x, y) ∈ A}

is basic.

Proof: We have A = λ^{−1}(Â) where Â is compact, and C = λ^{−1}(Ĉ) where Ĉ is open. Since C is nonempty we may choose y_{0} ∈ C. Then D is contained in the basic section

E = {x ∈ X : (x, y_{0}) ∈ A}.

The image λ(E) is relatively compact by Proposition 4.3. Therefore λ(D) is relatively compact, and thus has a compact closure D̂.

To show that D is basic, we shall prove that

D = λ^{−1}(D̂).  (4)

We prove the nontrivial inclusion. Suppose that x ∉ D. Choose y ∈ C such that (x, y) ∉ A. Let f, g be the projection maps from λ(X × Y) to λ(X) and to λ(Y). By the Projection Rule, g is continuous, so the set g^{−1}(Ĉ) is open, and therefore

U = g^{−1}(Ĉ) − Â

is open in λ(X × Y). By the open mapping property, the set V = f(U) is open in λ(X). We have g(λ(x, y)) = λ(y) ∈ Ĉ and λ(x, y) ∉ Â, so λ(x, y) ∈ U. Therefore λ(x) ∈ V.

Whenever λ(x̄) ∈ V there exists ȳ ∈ Y such that λ(x̄, ȳ) ∈ U. Then ȳ ∈ C and (x̄, ȳ) ∉ A, so x̄ ∉ D. Thus V ∩ λ(D) = ∅. Therefore λ(x) does not belong to the closure D̂ of λ(D), and x ∉ λ^{−1}(D̂). This proves (4), so D is a basic set. □

Remark 5.4 If (M, Λ) is compactly generated, then the converse of Theorem 5.3 also holds. □

The following theorem will give the universal step in a second quantifier elimination theorem which requires the strong mapping property.

Theorem 5.5 Let (M, Λ) be a law structure with the back and forth and strong mapping properties. Then for each basic set A ⊆ X × Y and nonempty basic set C ⊆ Y, the set

D = {x ∈ X : (∀y ∈ C)(x, y) ∈ A}

is basic.

Proof: We have A = λ^{−1}(Â) and C = λ^{−1}(Ĉ) for some compact sets Â and Ĉ. As in the proof of Theorem 5.3, λ(D) has a compact closure D̂. To show that D

is basic, we prove that

D = λ^{−1}(D̂).  (5)

Suppose x ∉ D. Let U be the complement of Â, which is open. Then there exists y ∈ C such that (x, y) ∉ A, so λ(x, y) ∈ U. Let f be the projection from λ(X ×{y}) to λ(X). By the strong mapping property, the set V = f(U ∩ λ(X × {y}) is open, and λ(x) ∈ V.

Suppose λ(x̄) ∈ V. There exists x′ ∈ X such that λ(x′, y) ∈ U and f(λ(x′, y)) = λ(x′) = λ(x̄). By the back and forth property, there exists ȳ such that λ(x̄, ȳ) = λ(x′, y). Then λ(x̄, ȳ) ∈ U, so (x̄, ȳ) ∉ A. Moreover, λ(ȳ) = λ(y), so ȳ ∈ C. Therefore x̄ ∉ D. This shows that V ∩ λ(D) = ∅, so λ(x) does not belong to the closure D̂ of λ(D), and x ∉ λ^{−1}(D̂). This proves (5). □

Remark 5.6 If (M, Λ) is compactly generated and has the back and forth property, then the converse of Theorem 5.5 holds. □

We shall now apply the last few theorems to obtain two quantifier elimination theorems which involve infinitely long formulas. To give us the flexibility that we need, we shall define a language that depends on two families of sets A, B, where the universal quantifiers will be bounded by sets in A and the basic formulas will be taken from B. This is the language of neocompact formulas, which corresponds to the neocompact sets studied in [K2] and [FK1]. This language depends only on the family M and the families A and B, and does not require a law structure.

Let M be a family of nonempty sets closed under finite Cartesian products. For each X ∈ M let A(X) and B(X) be families of subsets of X. We shall usually refer to these families as A and B, dropping the X. In our first quantifier elimination theorem B will be the family of basic sets for (M, Λ) and A will be the family of inverse open sets. Later we will use other families A, B.

Let us fix an index set I, and for each i ∈ I let X_{i} ∈ M and let v_{i} be a variable of sort X_{i}. We allow the possibility that X_{i} = X_{j} even though i ≠ j in I. Given a finite set J ⊆ I of indices, we shall let X_{J} be the product space X_{J} = ∏_{j∈J} X_{j}. We shall use the notation a_{J} = ⟨a_{j} : j ∈ J⟩ for a finite sequence indexed by J.

Definition 5.7 By an atomic formula with support J over B we mean an expression v_{J} ∈ B where B ∈ B(X_{J}). A neocompact formula over (A, B) with support J is an expression which belongs to every set E(X_{J}) of expressions such that:

(a) Every atomic formula over B with support J belongs to E(X_{J}).

(b) If φ and ψ belong to E(X_{J}), then φ ∨ ψ belongs to E(X_{J}).

(c) If φ ∈ E(X_{H}), ψ ∈ E(X_{J}), and H ⊆ J, then φ ∧ ψ belongs to E(X_{J}).

(d) If {φ_{k} : k ∈ K} is a nonempty subset of E(X_{J}), then the conjunction ⋀_{k∈K} φ_{k} belongs to E(X_{J}).

(e) If φ belongs to E(X_{J}) and H ⊆ J, then (∃v_{H}) φ belongs to E(X_{J−H}).

(f) If φ belongs to E(X_{J}), H ⊆ J, and D is a nonempty set in A(X_{H}), then (∀v_{H} ∈ D) φ belongs to E(X_{J−H}).

Notice that the list of formation rules (a)–(f) contains no negation rule and no infinite disjunction rule.

The notion of an element x_{J} ∈ X_{J} satisfying a neocompact formula over (A, B) in a law structure (M, Λ) is defined in the natural way. As usual, the set of all elements which satisfy a neocompact formula is called the set defined by the formula. Each atomic formula with support J defines a set in B(X_{J}). Two neocompact formulas are said to be equivalent if they define the same set.

Here is our first quantifier elimination theorem. By a QE law structure we shall mean a closed law structure with the back and forth and open mapping properties.

Theorem 5.8 (First QE Theorem) Suppose (M, Λ) is a QE law structure. Let A be the family of inverse open sets and B be the family of basic sets for (M, Λ). Then each neocompact formula over (A, B) is equivalent in (M, Λ) to an atomic formula with the same support, and thus defines a basic set for (M, Λ).

Proof: The proof is by induction on the complexity of neocompact formulas. Theorems 5.1 and 5.3 are used in the quantifier steps (e) and (f). □

In applications, the family M is often closed under countable as well as finite Cartesian products. For example, the family M_{Ω} in the law structure (M_{Ω}, Meas) for a probability space Ω is closed under countable Cartesian products. In this case, a countable sequence of parameters z_{n} ∈ Z_{n} ∈ M can be combined to form a single parameter z = ⟨z_{n}⟩ ∈ ∏_{n} Z_{n} ∈ M. Thus neocompact formulas can be built starting from basic sections rather than basic sets, as long as only countably many parameters are used in one formula.

A neocompact formula over (A, B) is countable if all the conjunctions occurring in the formula (using (d)) are countable. The First QE Theorem has the following form for countable neocompact formulas with parameters.

Theorem 5.9 Let (M, Λ) be a QE law structure such that M is closed under countable Cartesian products. Let A be the family of inverse open sets and B be the family of basic sections for (M, Λ). Then every countable neocompact formula over (A, B) defines a basic section over (A, B).

Proof: For each z ∈ Z ∈ M, let B_{z} be the family of all basic sections with parameter z. The First QE Theorem shows that for each z ∈ Z ∈ M, every neocompact formula over (A, B_{z}) defines a basic section with parameter z. Consider a sequence z = ⟨z_{n} : n ∈ N⟩ where z_{n} ∈ Z_{n} ∈ M and Z = ∏_{n} Z_{n}. We show that for each n, each basic section B = {x : (x, z_{n}) ∈ A} with parameter z_{n} is a basic section with parameter z. The set A is basic, so by the Parameter Rule, λ(A × {z}) is relatively compact. Thus A×{z} is contained in a basic set D. By the Projection Rule, the projection f : λ(Z) → λ(Z_{n}) is continuous. We have f(λ(z)) = λ(z_{n}) and

B = {x : ∃y[(x, y, z) ∈ D ∧ ((x, y) ∈ A) ∧ f(λ(z)) = λ(y)]}.

This is a neocompact formula over (A, B_{z}), so B is a basic section with parameter z.

Any countable neocompact formula φ over (A, B) is built from countably many basic sections with parameters z_{n}, n ∈ N. By the preceding paragraph, there is a single parameter z such that φ is a neocompact formula over (A, B_{z}). Therefore φ defines a basic section with parameter z. □

We now proceed to our second quantifier elimination theorem, which has universal quantifiers bounded by basic sets rather than by inverse open sets, and thus concerns neocompact formulas over (B, B). Neocompact formulas over (B, B) are sometimes called neocompact formulas over B (this convention is used in [K4]).

Theorem 5.10 (Second QE Theorem) Let (M, Λ) be a total law structure. Let B be the family of basic sets for (M, Λ). Then each neocompact formula over (B, B) is equivalent in (M, Λ) to an atomic formula over B with the same support, and thus defines a basic set for (M, Λ).

Proof: By induction on complexity of neocompact formulas, using Theorem 5.1 at the existential quantifier step and Theorem 5.5 at the universal quantifier step. □

The following remark shows that every neocompact formula in the First QE Theorem is equivalent to a neocompact formula in the Second QE Theorem.

Remark 5.11 Let A be the set of inverse open sets, and let B be the set of basic sets for a law structure (M, Λ). Then every neocompact formula over (A, B) is equivalent to a neocompact formula over (B, B) with the same support.

Proof: By induction on the complexity of neocompact formulas over (A, B). For the universal quantifier step, we replace the universal quantifier

(∀y ∈ C) φ,

where C ⊆ Y is a nonempty inverse open set, by the infinite conjunction

⋀_{c∈C}(∀y ∈ B(c)) φ,

where B(c) is the basic set λ^{−1}(λ(c)). □

The Second QE Theorem, like the First QE Theorem, has the following consequence for countable neocompact formulas with parameters.

Theorem 5.12 Let (M, Λ) be a total law structure such that M is closed under countable Cartesian products. Let A be the family of basic sets and B be the family of basic sections for (M, Λ). Then every countable neocompact formula over (A, B) defines a basic section. □

The neocompact sets in [FK1] and other papers were built from the basic sets using the formation rules (a)–(f) for countable neocompact formulas (so the conjunctions in (d) are countable). However, [FK1] used the following more generous rule (c̃) in place of (c).

(c̃) The Cartesian product of two neocompact sets is neocompact.

In terms of formulas, this rule says:

(c̃) If φ belongs to E(X_{H}), ψ belongs to E(X_{J}), and H, J are disjoint, then φ ∧ ψ belongs to E(X_{H∪J}).

The next proposition shows that in many cases, including those in [FK1], the formation rules (c) and (c̃) lead to equivalent classes of neocompact formulas, even if H, J are not required to be disjoint.

Proposition 5.13 Let A and B be families of sets in a law structure (M, Λ), such that B is closed under finite Cartesian products, and whenever C ∈ B(X × Y) there exist A ∈ B(X) and B ∈ B(Y) such that C ⊆ A × B. Then for any neocompact formulas ψ, φ over (A, B) with finite supports H, J, ψ ∧φ is equivalent to a neocompact formula over (A, B) with support H ∪ J.

Proof: First show by induction on the complexity of formulas that the set defined by any neocompact formula φ(v_{J}) over (A, B) is contained in a finite union of sets in B(X_{J}).

We may therefore let C be a finite union of sets in B(X_{H}) which contains the set defined by ψ, and let D be a finite union of sets in B(X_{J}) which contains the set defined by φ. Then the projection of D to X_{J−H} is contained in a finite union E of sets in B(X_{J−H}). We see that the set defined by ψ ∧ φ is contained in C × E, which is a finite union of sets in B(X_{H∪J}). Thus C × E is defined by a finite disjunction θ of atomic formulas with support H ∪J. Using formation rule (c), ψ ∧φ is equivalent to the neocompact formula ψ ∧ (φ ∧ θ). □

A family of sets is said to be countably compact if every countable subfamily with the finite intersection property has nonempty intersection. A set which is defined by a countable neocompact formula over (A, B) is called a neocompact set over (A, B).

Many applications, such as those in [K2], [FK1], and [CK], make use of families (A, B) over which the family of neocompact sets is countably compact. For this reason, they can be used to prove existence theorems in a manner analogous to the use of compact sets in classical proofs. To get the applications, one does not need to introduce the law function at all. Instead, one can directly introduce smaller but simpler families of sets (A, B), which may have no obvious connection to a law structure, and then work with the neocompact formulas built from them. Sometimes, as in the case of adapted spaces, the law function is very complicated and one can greatly simplify applications by building neocompact formulas from more elementary sets.

We can get countable compactness for the neocompact sets from the following lemma and corollary.

Lemma 5.14 Let (M, Λ) be a closed and complete law structure such that M is closed under countable products. Then for each X ∈ M the family of basic sections B ⊆ X for (M, Λ) is countably compact.

Proof: For each n ∈ N let B_{n} ⊆ X be a basic section with parameter z_{n} ∈ Z_{n} ∈ M. Suppose the countable set {B_{n} : n ∈ N} has the finite intersection property. As in the proof of Proposition 5.9, there is a single parameter z ∈ Z ∈ M such that each B_{n} is a basic section with parameter z. By Proposition 4.11, the family of basic sections in X with parameter z is compact. Therefore the intersection ⋂_{n} B_{n} is nonempty. □

Corollary 5.15 Let M be a family of sets closed under countable Cartesian products, and let A(X), B(X) be families of subsets of X for each X ∈ M. Suppose that either

(i) There is a QE law structure (M, Λ) such that every A ∈ A(X) is inverse open and every B ∈ B(X) is a basic section, or

(ii) There is a total law structure (M, Λ) such that every A ∈ A is a basic set and every B ∈ B(X) is a basic section.

Then for each X the family of neocompact subsets of X over (A, B) is countably compact.

Proof: We give the proof in case (ii); case (i) is similar. Let A′ be the family of all basic sets and B′ the family of all basic sections for (M, Λ). Then A ⊆ A′ and B ⊆ B′. By Theorem 5.12, each neocompact set over (A′, B′) in X belongs to B′(X). By Lemma 5.14, the family B′(X) is countably compact. The desired conclusion follows. □

The quantifier elimination theorems for neocompact formulas lead to quantifier elimination theorems for a larger class of formulas, called the neoclosed formulas over (A, B). The neoclosed formulas are built using the same formation rules as the neocompact formulas, except that there is a larger collection of atomic formulas and that the existential quantifiers are bounded by basic sets. A set which is defined by a countable neoclosed formula over (A, B) is called a neoclosed set. As the name implies, the neoclosed sets play a role analogous to the closed sets in applications such as those in [FK1].

In the following definition, M is a family of nonempty sets closed under finite Cartesian products, and for each X ∈ M, A(X) and B(X) are families of subsets of X.

Definition 5.16 By an atomic neoclosed formula with support J over B we mean an expression (v_{J} ∈ A) where A is a subset of X_{J} such that A ∩ B ∈ B(X_{J}) for each B ∈ B(X_{J}). A neoclosed formula over (A, B) with support J is an expression which belongs to every set E(X_{J}) of expressions such that (b), (c), (d),

(f) from Definition 5.7 hold, and:

(ã) Every atomic neoclosed formula over B belongs to E(X_{J}).

(ẽ) If φ belongs to E(X_{J}), C ∈ B(X_{H}), and H ⊆ J, then (∃v_{H} ∈ C) φ belongs to E(X_{J−H}).

Note that if each X ∈ M is a Hausdorff space and B is the family of all compact sets, then every neoclosed formula over (A, B) defines a closed set. However, this would not be true if the existential quantifier rule (ẽ) allowed unbounded existential quantifiers, because unbounded existential projections of closed relations need not be closed.

The following result is a general principle for obtaining quantifier elimination for neoclosed formulas from quantifier elimination for neocompact formulas.

Proposition 5.17 Suppose that B is closed under finite Cartesian products, and that each A ∈ A(X) is a union of sets C ∈ A(X) such that C ⊆ B for some B ∈ B(X). Then for each neoclosed formula φ over (A, B) with support J and each B ∈ B(X_{J}), φ(x_{J}) ∧ (x_{J} ∈ B) is equivalent to a neocompact formula over (A, B) with support J. Thus if each neocompact formula over (A, B) is equivalent to an atomic formula with the same support, then every neoclosed formula over (A, B) is equivalent to an atomic neoclosed formula with the same support.

Proof: We argue by induction on φ. All but the quantifier steps are trivial. For the existential quantifier step (ẽ), let C ∈ B(X_{H}) and let ψ(x_{J−H}) = (∃x_{H} ∈ C) φ(x_{J}). Let B ∈ B(X_{J−H}). Then ψ(x_{J−H}) ∧ (x_{J−H} ∈ B) is equivalent to the neocompact formula

(∃x_{J−H})[φ(x_{J}) ∧ (x_{J} ∈ B × C)].

For the universal step (f) let D ∈ A(X_{H}) and let ψ(x_{J−H}) = (∀x_{H} ∈ D) φ(x_{J}). Then there are sets D_{i} ∈ A(X_{H}), C_{i} ∈ B(X_{H}), i ∈ I such that D = ⋃_{i∈I} D_{i} and D_{i} ⊆ C_{i} for each i ∈ I. Let B ∈ B(X_{J−H}). Then ψ(x_{J−H})∧(x_{J−H} ∈ B) is equivalent to the neocompact formula

⋀_{i∈I}(∀x_{H} ∈ D_{i})[φ(x_{J}) ∧ (x_{J} ∈ B × C_{i})].

This completes the induction. □

6 Examples Revisited

In this section we shall revisit some of the examples from Section 3 and see what our quantifier elimination theorems say about them.

Example 1: The identity law structure is total. For the identity law structure the Second QE Theorem says that every neocompact formula over (B, B) defines a compact set, where B is the family of compact sets. This can be easily seen directly by observing that the family of compact sets is closed under all the operations (a)–(f) which are used to build neocompact formulas.

Example 3: We revisit the law structure (M_{A}, Λ^{qf}) of quantifier-free types where A is a model for a first order logic with equality. In order to distinguish between formulas of first order logic and the atomic and neocompact formulas which appear in our quantifier elimination theorems, we shall call formulas of first order logic finite formulas here.

The atomic formulas with support J are the finite or infinite conjunctions of finite quantifier-free formulas with free variables from v_{j}, j ∈ J. The basic sets C ∈ B are the sets defined by these formulas. The inverse open sets C ∈ A are defined by finite or infinite disjunctions of finite quantifier-free formulas. The neocompact formulas over (A, B) are built from the atomic formulas using the rules (a)-(f). Although the list of rules (a)-(f) contains no formation rule for negations, negations may appear “inside” atomic formulas within neocompact formulas.

For example, in an ordered field the atomic formula x ≠ y ∧ ⋀_{n} n × |x − y| ≤ 1 says that x is infinitely close but not equal to y. Given a neocompact formula θ(y, z⃗), the neocompact formula

∀x∃y(θ(y, z⃗) ∧ ⋀_{n} n × |x − y| ≤ 1)

says that every element is infinitely close to an element of the set {y : θ(y, z⃗)}, and the formula

∀y[⋁_{n} |y| < n → φ(y, z⃗)]

says that φ(y, z⃗) holds for all finite y.

In a group, the atomic formula ⋀_{n} x^{n} ≠ 1 says that x has infinite order, the neocompact formula

⋀_{n} ∃x( ⋀_{m<n} x^{m} ≠ 1 ∧ x^{n} = 1)

says that there exist elements of all finite orders, and the neocompact formula

∀x[⋁_{m} x^{m} = 1 → ∃y(xy = yx ∧ ⋀_{n} y_{n} ≠ 1)]

says that every element of finite order commutes with some element of infinite order.

Each of Theorems 5.3 and 5.1 by itself gives a sufficient condition for T h(A) to admit first order quantifier elimination. The First QE Theorem combines these two theorems to give a quantifier elimination theorem for the (infinite) neocompact formulas over A.

Corollary 6.1 (i) If (M_{A}, Λ^{qf}) is dense and has the open mapping property, then every universal formula (∀y⃗ ∈ C)φ(x⃗, y⃗) is equivalent in A to a conjunction of quantifier-free formulas ⋀ Γ(x⃗).

(ii) If (M_{A}, Λ^{qf}) is closed, dense, and has the open mapping property, then T h(A) admits first order elimination of quantifiers.

Proof: Part (i) follows from Theorem 5.3. Assume the hypotheses of (ii) and let ∀y⃗φ(x⃗, y⃗) be a finite universal formula. By (i), the set of quantifier-free formulas Γ(x⃗) ∪ {¬φ(x⃗, y⃗)} is not satisfiable in A. Since (M_{A}, Λ^{qf}) is closed, this set is not finitely satisfiable in A. It follows that ∀y⃗φ(x⃗, y⃗) is equivalent in A to the conjunction of a finite subset Γ_{0}(x⃗) ⊆ Γ(x⃗). First order quantifier elimination now follows by induction on the complexity of formulas. □

The next corollary is proved by a similar argument but uses Theorem 5.1 instead of 5.3.

Corollary 6.2 (i) If (M_{A}, Λ^{qf}) has the back and forth property and is closed, then every existential formula ∃y⃗φ(x⃗, y⃗) is equivalent in A to a conjunction of quantifierfree formulas ⋀ Γ(x⃗).

(ii) Suppose (M_{A}, Λ^{qf}) has the back and forth property, and for every set of quantifier-free formulas Σ(x⃗) and universal formula ψ(x⃗), if Σ(x⃗)∪{ψ(x⃗)} is finitely satisfiable in A then it is satisfiable in A. Then T h(A) admits first order elimination of quantifiers. □

One of the easiest ways to prove that a theory admits first order elimination of quantifiers is to take an ω-saturated model B and show that any pair a⃗, b⃗ in B which satisfy the same quantifier-free formulas satisfy the same finite existential formulas, i.e. that (M_{B}, Λ^{qf}) is dense. Using ω-saturation, this shows that the hypotheses of Corollary 6.2(ii) hold for (M_{B}, Λ^{qf}). For example, one can show in this way that the theories of dense linear order, algebraically closed fields, and real closed ordered fields admit first order elimination of quantifiers.

Things are especially simple if the vocabulary of A has no function symbols.

Corollary 6.3 If A is a model whose vocabulary is finite and has no function symbols, and (M_{A}, Λ^{qf}) is dense, then T h(A) admits first order elimination of quantifiers.

Proof: For each n, A has only finitely many quantifier-free n-types, so the hypotheses of Corollary 6.2(ii) hold for (M_{B}, Λ^{qf}). □

Example 4: We revisit the law structure of quantifier-free types in countably many variables. Let A be a model, and consider the law structure (MA^{ω_{1}}, Λ^{qf}). In this case the corresponding language has formulas with countably many variables, so the support J of a formula will be a finite or countable set. A basic set B ∈ B with support J will be defined by an infinite conjunction of finite quantifier-free formulas whose variables are included in the set v_{J}, and an inverse open set C ∈ A will be defined by an infinite disjunction of finite quantifier-free formulas. The neocompact formulas over (A, B) will contain quantifiers over countable sets of variables. In this case the First QE Theorem says the following.

Corollary 6.4 Suppose that the law structure (M_{A}, Λ^{qf}) of finite quantifier-free types is dense and has the open mapping property, and for all α < ω_{1} and a⃗ ∈ A^{α}, every set of finite quantifier-free formulas with constants for a⃗ and countably many variables which is finitely satisfiable in (A, a⃗) is realized in (A, a⃗). Then every neocompact formula over (A, B) is equivalent in A to a conjunction of finite quantifier-free formulas. □

Since the set M is closed under countable products, we may also apply Theorem 5.9 to obtain:

Corollary 6.5 Assume the hypotheses of Corollary 6.4. Let B′ be the family of basic sections for (MA^{ω_{1}}, Λ^{qf}). Then every countable neocompact formula over (A, B′) defines a basic section, and for each α < ω_{1} the family of neocompact sets over A^{α} is countably compact. □

Example 5: We now revisit the law structures (M_{A}, Λ^{rst}) of quantifier-free n-types which are realized in a model A with the restricted topology.

Proposition 3.2 gave a criterion for (M_{A}, Λ^{rst}) to be a law structure. If (M_{A}, Λ^{rst}) is a law structure then it is automatically closed, and has the completeness, density, open mapping, or strong mapping property if and only if (M_{A}, Λ^{qf}) has that property. However, (M_{A}, Λ^{rst}) may have fewer basic sets, and hence fewer neocompact formulas, than the corresponding law structures (M_{A}, Λ^{qf}).

In the corollaries below, let A be the family of inverse open sets, which are defined by disjunctions of quantifier-free formulas. Also, let B be the family of basic sets for (M_{A}, Λ^{rst}). A basic set is defined by the conjunction of a finite or infinite set Γ(v⃗) of quantifier-free formulas such that every quantifier-free type p over A which contains Γ(v⃗) is realized in A. In general, the model A will not realize all quantifier-free types over A.

Corollary 6.6 Suppose (M_{A}, Λ^{qf}) has the back and forth and open mapping properties, and (M_{A}, Λ^{rst}) is a law structure. Then every neocompact formula over (A, B) defines a basic set for (M_{A}, Λ^{rst}) with the same support.

Proof: (M_{A}, Λ^{rst}) is closed and has the back and forth and open mapping properties, so the First QE Theorem applies. □

Proposition 3.4 gave us a supply of models A which satisfy the hypotheses of the above corollary.

Corollary 6.7 Suppose T h(A) admits first order elimination of quantifiers and (M_{A}, Λ^{rst}) is a complete law structure. Then every neocompact formula over (A, B) defines a basic set for (M_{A}, Λ^{rst}) with the same support.

Proof: First order quantifier elimination for T h(A) implies that (M_{A}, Λ^{qf}) is dense with the open property, and since it is complete it has the back and forth property. □

Example 7: We now revisit the law structure of random variables. Let Ω be a probability space whose law structure (M_{Ω}, law, Meas) is complete. Then (M_{Ω}, law, Meas) is total, so the Second QE Theorem applies. Let B be the family of basic sets for (M_{Ω}, law, Meas). Thus the atomic formulas over B are the formulas stating that law(x⃗) ∈ B where B is a compact set in Meas(M) for some separable metric space M. It is shown in [FK1] that many of the central notions in probability theory can be expressed by neocompact formulas in the law structures of probability spaces or adapted probability spaces. Some examples are the notions of a Brownian motion, martingale, stopping time, adapted process, and stochastic integral.

See [K4] for more examples of total law structures from probability theory, and [BN] for Banach space examples.

7 Products of Law Structures

In this section we extend the Second QE Theorem to law structures in which the strong mapping property only holds “locally”. This will be needed for the applications of our results to continuous time stochastic processes in the forthcoming paper [K4]. We shall introduce the notion of a product of a sequence of law structures, and show that under appropriate hypotheses a countable product admits elimination of quantifiers for neocompact formulas where A is the family of sets which are basic for some finite product. At the end of this section we shall again revisit the examples of law structures of quantifier-free types with the full and restricted topologies.

Let (M, λ_{1}, Λ_{1}) and (M, λ_{2}, Λ_{2}) be two law structures over the same family M. Then (M, λ, Λ) is a law structure where λ(x) = (λ_{1}(x), λ_{2}(x)), and Λ(X) is the topological product of Λ_{1}(X) and Λ_{2}(X).

Now let (M, λ_{k}, Λ_{k}) be a law structure on M for each k ∈ N. For each X ∈ M let λ(x) be the sequence λ(x) = ⟨λ_{k}(x) : k ∈ N⟩ and let Λ(X) be the topological product of Λ_{k}(X), k ∈ N.

We emphasize that in this section we are dealing with a sequence of law structures all of which are over the same family M, and we form a product of the target spaces Λ_{k}(X). This is different from the law structures (M_{A}, Λ^{rst}) considered in Example 5 where A is a countable Cartesian product of models A_{k}, and from the parameter forms of the QE theorems, where M is assumed to be closed under countable Cartesian products.

Proposition 7.1 The product (M, λ, Λ) is a law structure.

Proof: The Parameter Rule follows from Tychonoff’s theorem on products of compact sets. □

Let (M, λ⃗_{k}, Λ⃗_{k}) be the product of the first k + 1 law structures in the sequence, that is, λ⃗_{k} = ⟨λ_{0}, …, λ_{k}⟩, and Λ⃗_{k}(X) is the topological product Λ_{0}(X)×⋯×Λ_{k}(X).

In the examples at the end of this section we shall see that law structures of quantifier-free types over an infinite vocabulary are isomorphic to products of law structures of quantifier-free types over finite reducts of the vocabulary. For a similar reason, the law structures of continuous time stochastic processes in [K4] will be products of law structures of finite discrete time stochastic processes.

The next few results give relationships between a countable infinite product of law structures and the finite subproducts.

Proposition 7.2 Suppose that (M, Λ⃗_{k}) is a dense law structure for each k ∈ N. Then (M, Λ) is a dense law structure.

Proof: Let x, x̄ ∈ X, λ(x) = λ(x̄), and y ∈ Y. Then for each k ∈ N we have λ⃗_{k}(x) = λ⃗_{k}(x̄). Since (M, λ⃗_{k}) is dense, for each k ∈ N and neighborhood U of λ⃗_{k}(x, y) there exists ȳ ∈ Y such that λ_{k}(x̄, ȳ) ∈ U. Let

f : Λ(X × Y) → Λ⃗_{k}(X × Y)

be the natural projection map. Let V be a neighborhood of λ(x, y). Then for some k ∈ N and neighborhood U of λ⃗_{k}(x, y), f^{−1}(U) ⊆ V. Therefore there exists ȳ ∈ Y such that λ(x̄, ȳ) ∈ V. This shows that (M, Λ) is dense. □

Proposition 7.3 Suppose that for each k ∈ N, (M, Λ⃗_{k}) is dense and has the open mapping property . Then (M, Λ) is dense and has the open mapping property.

Proof: (M, Λ) is dense by Proposition 7.2. Let x ∈ X ∈ M, y ∈ Y and let U be an open neighborhood of λ(x, y). Then for some k and open set U_{k} in λ⃗_{k}(X × Y), U = f^{−1}(U_{k}) where f is the projection from λ(X × Y) to λ⃗_{k}(X × Y). By the open mapping property for (M, Λ⃗_{k}), the projection g_{k} from λ⃗_{k}(X × Y) to λ⃗_{k}(X) is open, so the set V_{k} = g_{k}(U_{k}) is open in λ⃗_{k}(X). Then V = f^{−1}(V_{k}) is open in Λ(X) and V = g(U) where g is the projection from λ(X × Y) to λ(X). □

Proposition 7.4 Let (M, Λ_{m}) be a sequence of first countable law structures. Suppose k ∈ N and whenever λ⃗_{k}(B) is relatively compact, λ(B) is relatively compact.

(i) If (M, Λ) is closed, then (M, Λ⃗_{m}) is closed for each m ≥ k.

(ii) If (M, Λ) is closed and complete, then (M, Λ⃗_{m}) is closed and complete for each m ≥ k.

Proof: (i) Let x_{n} be a sequence in X ∈ M such that λ⃗_{m}(x_{n}) converges to b in Λ⃗_{m}(X). Let B = {x_{n} : n ∈ N}. Then λ⃗_{m}(B) is relatively compact. Since m ≥ k, λ⃗_{k}(B) is relatively compact. By hypothesis, λ(B) is relatively compact. Therefore the sequence λ(x_{n}) has a subsequence λ(x_{f(n)}) which converges to a point c. Since (M, Λ) is closed, c = λ(x) for some x ∈ X. Then λ⃗_{m}(x_{f(n)}) converges to λ⃗_{m}(x), so b = λ⃗_{m}(x) and thus (M, Λ⃗_{m}) is closed.

(ii) Let x_{n} be a sequence in X ∈ M and y ∈ Y ∈ M be such that λ⃗_{m}(x_{n}, y) converges to b in Λ⃗_{m}(X ×Y). As in part (i), the sequence λ(x_{n}, y) has a subsequence λ(x_{f(n)}, y) which converges to a point c in Λ(X × Y). Since (M, Λ) is closed and complete, there exists x ∈ X such that λ(x, y) = c. Then λ⃗_{m}(x_{n}, y) converges to λ⃗_{m}(x, y) = b, so (M, Λ⃗_{m}) is closed and complete. □

As a preparation for our next quantifier elimination theorem we prove some lemmas relating basic sets for (M, Λ⃗_{k}) and for (M, Λ).

Lemma 7.5 Let A, B ⊆ X. If k ≤ m, A is basic for (M, Λ⃗_{k}), and B is basic for (M, Λ⃗_{m}), then A ∩ B is basic for (M, Λ⃗_{m}).

Proof: Let

A = λ⃗_{k}^{−1}(Â), B = λ⃗_{m}^{−1}(B̂),

where Â is compact in Λ⃗_{k}(X) and B̂ is compact in Λ⃗_{m}(X). Let p : Λ⃗_{m}(X) → Λ⃗_{k}(X) be the natural projection map. Then

A ∩ B = {x ∈ X : λ⃗_{m}(x) ∈ p^{−1}(Â) ∩ B̂}.

Since p is continuous, p^{−1}(Â) is closed, so p^{−1}(Â) ∩ B̂ is compact. This shows that A ∩ B is basic for (M, Λ⃗_{m}). □

Lemma 7.6 A set B ⊆ X is basic for (M, Λ) if and only if B = ⋂_{k} B_{k} for some sequence of basic sets B_{k} for (M, λ⃗_{k}), k ∈ N. Moreover, the sets B_{k} may be taken to be a decreasing chain B_{0} ⊇ B_{1} ⊇ · · ·.

Proof: Suppose first that B_{k} ⊆ X is basic for (M, λ⃗_{k}) for each k ∈ N. Let B = ⋂_{k} B_{k}, and let B_{k} = λ⃗_{k}^{−1}(B̂_{k}) where B̂_{k} is compact in Λ⃗_{k}(X). For each k, λ⃗_{k}(B) ⊆ B̂_{k} is relatively compact, so λ(B) is relatively compact by the Tychonoff product theorem. Therefore the closure B̂ of λ(B) is compact. Let λ(x) ∈ B̂. Since the projection is continuous and λ⃗_{k}(B) ⊆ B̂_{k}, λ⃗_{k}(x) ∈ B̂_{k}. Therefore x ∈ B_{k}. Since this holds for all k, x ∈ B. This proves that B = λ^{−1}(B̂), so B is basic for (M, Λ).

For any compact subset C of Λ(X), we have

{x ∈ X : λ(x) ∈ C} = ⋂_{k}{x ∈ X : λ⃗_{k}(x) ∈ p_{k}(C)}

where p_{k} is the projection onto the first k coordinates. Each set p_{k}(C) is compact in Λ⃗_{k}(X). This shows that any basic set for (M, Λ) can be put into the required form ⋂_{k} B_{k}.

Moreover, by Lemma 7.5, for each k the finite intersection C_{k} = ⋂_{m=0}^{k} B_{m} is basic for (M, Λ⃗_{k}), so B is an intersection of a decreasing chain of sets C_{k} basic for (M, Λ⃗_{k}). □

Corollary 7.7 If B_{n} is basic for (M, Λ⃗_{n}) for each n ≥ k, then B = ⋂_{n=k}^{∞} B_{n} is basic for (M, Λ).

Proof: Since B_{k} is basic for (M, Λ⃗_{k}), λ⃗_{k}(B_{k}) is relatively compact in Λ⃗_{k}(X). By continuity of the projection maps, λ⃗_{n}(B_{k}) is relatively compact in Λ⃗_{n}(X) for each n < k. Therefore for each n < k there is a basic set B_{n} for (M, Λ⃗_{n}) such that B_{n} ⊇ B_{k}. Then B = ⋂_{n} B_{n} and so B is basic for (M, Λ) by Lemma 7.6. □

Corollary 7.8 Suppose B ⊆ X is basic for (M, Λ⃗_{k}). The following are equivalent. (i) For each m ≥ k, B is basic for (M, Λ⃗_{m}). (ii) B is basic for (M, Λ). (iii) λ(B) is relatively compact.

Proof: (i) implies (ii) by Corollary 7.7. (ii) implies (iii) by the definition of a basic set. Assume (iii), and let B̂ be a compact set in Λ(X) which contains λ(B). Then Ĉ = p(B̂) is a compact set in Λ⃗_{m}(X) which contains λ⃗_{m}(B), where p is the projection map. So C = λ⃗_{m}^{−1}(Ĉ) is basic for (M, Λ⃗_{m}) and C ⊇ B. By Lemma 7.5, B = B ∩ C is basic for (M, Λ⃗_{m}). This proves (i). □

Corollary 7.9 Suppose that X ∈ M and Λ(X) is compact. Then every set B ⊆ X which is basic for (M, Λ⃗_{k}) is also basic for (M, Λ) and for (M, Λ⃗_{m}) whenever m > k. □

Lemma 7.10 Let (M, Λ_{k}) be a sequence of law structures, each with the back and forth and strong mapping properties. For each k ∈ N, basic set A ⊆ X × Y for (M, Λ), and nonempty basic set C ⊆ Y for (M, λ⃗_{k}), the set

B = {x ∈ X : (∀y ∈ C)(x, y) ∈ A}

is basic for (M, Λ).

Proof: By Lemma 7.6, A has the form A = ⋂_{n} A_{n} where A_{n} is basic for (M, Λ⃗_{n}). By Lemma 7.5, we may assume that A_{k} = ⋂_{n=0}^{k} A_{n}, so that A = ⋂_{n=k}^{∞} A_{n}. Then

B = ⋂_{n=k}^{∞}{x ∈ X : (∀y ∈ C)(x, y) ∈ A_{n}} = ⋂_{n=k}^{∞} B_{n}.

If B is empty then it is basic for (M, Λ). Suppose B is nonempty. Let n ≥ k. By Lemma 5.2, λ(C) is relatively compact. Hence by Corollary 7.8, C is basic for (M, Λ⃗_{n}). Then by Proposition 5.5, B_{n} is basic for (M, Λ⃗_{n}), and by Corollary 7.7, B is basic for (M, Λ). □

The following result is a generalization of the Second QE theorem. The strong mapping property is only assumed locally, and the universal quantifiers are eliminated only locally, where “local” means over the finite subproducts.

Theorem 7.11 (Local QE Theorem) Let (M, Λ_{k}) be a sequence of law structures such that (M, Λ) is closed and complete, and for each k, (M, Λ⃗_{k}) has the back and forth and strong mapping properties.

Let A_{k} be the set of all basic sets B for (M, Λ⃗_{k}), and let A = ⋃_{k} A_{k}. Let B be the family of basic sets for (M, Λ). Then every neocompact formula over (A, B) is equivalent in (M, Λ) to an atomic formula over B with the same support, and thus defines a basic set for (M, Λ).

Proof: By Proposition 7.2, (M, Λ) is dense, and by Proposition 2.3 it has the back and forth property. Argue by induction on the complexity of neocompact formulas over (A, B), using Theorem 5.1 and Lemma 7.10 at the quantifier steps. □

Here is the corresponding theorem with parameters.

Theorem 7.12 Suppose M is closed under countable Cartesian products. Let (M, Λ_{k}) and A be as in the preceding theorem. Let B be the family of all basic sections for (M, Λ).

(i) Every countable neocompact formula over (A, B) defines a basic section for (M, Λ).

(ii) The family of neocompact subsets of X over (A, B) is countably compact. □

Example 3 (Quantifier-free types) revisited again:

Let L be a first order vocabulary which is the union of a countable chain L = ⋃_{k} L_{k} of first order vocabularies L_{k}, A be a model for L, A_{k} be the reduct of A to L_{k}, and Λ_{k}^{qf}(A^{n}) be the space of all quantifier-free n-types for A_{k}. Then the law structure (M_{A}, Λ^{qf}) of quantifier-free types is isomorphic to the product of the law structures (M_{A_{k}}, Λ_{k}^{qf}). Similarly, the law structure (M_{A}, Λ^{el}) of elementary types over A is isomorphic to the product of the law structures (M_{A_{k}}, Λ^{el}).

Hint: Let F^{n} be the mapping from Λ^{qf}(A^{n}) into ∏_{k} Λ_{k}^{qf}(A^{n}) such that (F^{n}(p))(k) is the reduct of p to L_{k}. Then F^{n} is a homeomorphism from Λ^{qf}(A^{n}) to a closed subspace of ∏_{k} Λ_{k}^{qf}(A^{n}) and induces a law structure isomorphism.

For the law structure (M_{A}, Λ^{qf}), the Local QE Theorem gives nothing beyond the First QE Theorem 5.8, because in this case it turns out that the universal quantifiers bounded by sets in A are easily replaced by universal quantifiers bounded by inverse open sets.

If each (M_{A_{k}}, Λ_{k}^{qf}) has a property but (M_{A}, Λ^{qf}) does not, we can conclude that the property is not preserved under countable products of law structures. As an illustration, let L_{k} have k + 1 unary predicates U_{0}, …, U_{k} and one binary relation E. Let A be a model of the complete theory where the U_{k} are disjoint, E has two equivalence classes, and each equivalence class of E contains infinitely many elements of each U_{k}. This theory admits elimination of quantifiers, so the law structures of quantifier-free and elementary types are the same. For each k, T h(A_{k}) is ω-categorical, so (M_{A_{k}}, Λ_{k}^{qf}) is a total law structure.

Now let each equivalence class of E in A have a different finite number of elements realizing the type {¬U_{n}(x) : n ∈ N}. Then (M_{A}, Λ^{qf})) is not closed and has neither the back and forth property nor the strong mapping property. Thus the back and forth property, the strong mapping property, and closedness are not preserved under countable products.

Example 5 (Restricted topology) revisited again:

Again let L be a first order vocabulary which is the union of a countable chain L = ⋃_{k} L_{k} of first order vocabularies L_{k}. Let A be a model for L and let A_{k} be the reduct of A to L_{k}. Assume that each (M_{A_{k}}, Λ_{k}^{rst}) is a law structure. Assume further that whenever each L_{k}-reduct of a quantifier-free n-type p ∈ Λ^{qf}(A^{n}) over A is realized in A_{k}, p is realized in A.

Proposition 7.13 (M_{A}, Λ^{rst}) is a law structure and is isomorphic to the product of the law structures (M_{A_{k}}, Λ_{k}^{rst}), k ∈ N.

Hint: As in the preceding example, let F^{n} be the mapping from Λ^{rst}(A^{n}) to a closed subset of ∏_{k} Λ_{k}^{rst}(A^{n}) such that (F^{n}(p))(k) is the reduct of p to L_{k}. Show that the closure of F^{n}(Λ^{rst}(A^{n})) in the topological product ∏_{k} Λ_{k}^{rst}(A^{n}) is the set of all F^{n}(p) such that for each k the reduct of p to L_{k} is realized in A_{k}. □

A set C ⊆ X_{J} belongs to the family A_{k} of sets which are basic for (M_{A_{k}}, Λ_{k}^{rst}) iff C is defined by a conjunction of quantifier-free formulas ⋀_{t∈T} ψ_{t}(v⃗) such that each ψ_{t} belongs to L_{k}, and every quantifier-free type p ⊇ {ψ_{t} : t ∈ T } over A_{k} is realized in A_{k}. We let A = ⋃_{k} A_{k} and let B be the set of basic sets for (M_{A}, Λ^{rst}).

In this case the Local Quantifier Elimination Theorem says the following:

Corollary 7.14 If (M_{A_{k}}, Λ_{k}^{rst}) is a total law structure for each k and (M_{A}, Λ^{rst}) is complete, then every neocompact formula over (A, B) is equivalent in A to a conjunction of quantifier-free formulas with the same support. □

References

[BN] S. Baratella and S-A Ng. Quantifier Elimination in Banach Spaces. To appear.

[Bi] P. Billingsley. Convergence of Probability Measures. Wiley (1968).

[CK] N. Cutland and H. J. Keisler. Neocompact Sets and Stochastic Navier-Stokes Equations. Pp. 31-54 in Stochastic Partial Differential Equations. London Math. Soc. Lecture Notes Series 216, ed. by A. Etheridge, Cambridge 1995.

[DMM] L. van den Dries, A. Macintyre, and D. Marker. The Elementary Theory of Restricted Analytic Fields with Exponentiation. Ann. Math. 140 (1994), 183-205.

[FK1] S. Fajardo and H. J. Keisler. Existence Theorems in Probability Theory. Advances in Mathematics 120 (1996), pp. 191-257.

[FK2] S. Fajardo and H. J. Keisler. Neometric Spaces. Advances in Mathematics 118 (1996), pp. 134-175.

[He] C. W. Henson. Nonstandard Hulls of Banach Spaces. Israel J. Math. 25 (1976), pp. 108-144.

[HI] C. W. Henson and J. Iovino. Banach Space Model Theory. To appear.

[HK] D. N. Hoover and H. J. Keisler. Adapted Probability Distributions. Trans. Amer. Math. Soc. 286 (1984), 159-201.

[K1] H. J. Keisler. Probability Quantifiers; pp. 506-556 in Model-Theoretic Logics, ed. by K. J. Barwise and S. Feferman, Springer-Verlag (1985).

[K2] H. J. Keisler. From Discrete to Continuous Time. Ann. Pure and Applied Logic 52 (1991), 99-141.

[K3] H. J. Keisler. A Neometric Survey. Pp. 233-250 in Developments in Nonstandard Analysis, ed. by N. Cutland et al, Longman 1995.

[K4] H. J. Keisler. Rich and Saturated Adapted Spaces. To appear.

[Ke] J. Kelley. General Topology. D Van Nostrand 1955.

[MW] A. Macintyre and A. Wilkie. On the Decidability of the Real Exponential Field. To appear.

[Ta] A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of Calif. Press 1951, Second ed.

University of Wisconsin, Madison WI. keisler@math.wisc.edu

Mathematical Subject Classification, 1991:

Primary: 03C10, 03C90

Secondary: 54E35

Keywords: elimination, quantifier, neocompact