Archive for Mathematical Logic manuscript No. (will be inserted by the editor)

David Pierce

Model-theory of vector-spaces over unspecified fields

Received: date / Revised: date

Abstract Vector-spaces over unspecified fields can be axiomatized as one-sorted structures, namely, abelian groups with the relation of parallelism. Parallelism is binary linear dependence. When equipped with the n-ary relation of linear dependence for some positive integer n, a vector-space is existentially closed if and only if it is n-dimensional over an algebraically closed field. In the signature with an n-ary predicate for linear dependence for each positive integer n, the theory of infinite-dimensional vector-spaces over algebraically closed fields is the modelcompletion of the theory of vector-spaces.

Keywords vector-space · model-completeness · sort

Mathematics Subject Classification (2000) 03C10 · 03C60

0 Introduction

In Abraham Robinson’s original definition [14, §2.2], a (first-order) theory T is model-complete if the theory T ∪ diag𝔐 is complete whenever 𝔐 ⊧ T. Two equivalent formulations are as follows, in current notation, where 𝔐 and 𝔑 are models of T:

1. 𝔐 ⊆ 𝔑 ⟹ 𝔐 ≼_{1} 𝔑 (Robinson’s Test) [14, 2.3.1];

2. 𝔐 ⊆ 𝔑 ⟹ 𝔐 ≼ 𝔑 [14, 2.4.1].

Model-completeness is of use in the discovery of complete theories, since a modelcomplete theory with a model that embeds in every other model is complete [14, 4.1.6]. Discovery of model-complete theories—complete or not—is also of interest in itself.

David Pierce Mathematics Department, Middle East Technical University, Ankara, Turkey, 06531 E-mail: dpierce@metu.edu.tr

Robinson gives some examples of model-complete theories, including the theories of non-trivial torsion-free divisible abelian groups [14, §3.1], algebraically closed fields [14, §3.2], and real-closed fields [14, §3.3]; these examples are now standard [12, ch. 3]. Robinson notes also, in effect, that the theory of non-trivial vector-spaces over a given field is model-complete [14, §3.6]. However, although his notation would seem to allow it, he does not appear to consider the theory of vector-spaces tout court (over an unspecified field).

In the most usual formulation, a vector-space is a two-sorted structure. About early versions of model-theory, Angus Macintyre notes [11, §2.4, p. 198]:

For no good reason, natural structures were forced into a one-sorted formulation (and by now it is a considerable nuisance that there is no basic model-theory text in a many-sorted setting).

Nonetheless, the possibility of treating vector-spaces as two-sorted structures has been acknowledged in one textbook [15, §5.4]; also, modules in general have been treated as two-sorted structures [8, ch. 9]. A natural signature for this treatment of vector-spaces includes:

1. the signature of abelian groups, for the vectors;

2. the signature of rings, for the scalars;

3. a symbol for multiplication of vectors by scalars (in the present paper, this symbol is ∗).

In this signature, let T be the theory of vector-spaces, and if n ∈ {1,2,3,...}∪{∞}, let T_{n} be the theory of vector-spaces of dimension n. Andrey Kuzichev [10] gives an explicit elimination of quantified vector-variables in T_{n}. Indeed, suppose C is a formula whose vector-variables are from the tuple (x_{1},...,x_{m},y). (Kuzichev says m ⩾ 1, but this is not necessary if summations ∑ _{i=1}^{0} f_{i} are understood to be 0.) Let C′ be the result of replacing each y in C with ∑ _{i=1}^{m} α_{i} ∗ x_{i}, and let C^{∗} be the result of replacing each atomic sub-formula λ ∗ y = ∑ _{i=1}^{m} μ_{i} ∗ x_{i} of C with λ = 0 ∧ ∑ _{i=1}^{m} μ_{i}∗ x_{i} = 0. Then

T ⊢ ∃y C ↔ (∃ααα C′∨ (C^{∗}∧ ∃y ∀ααα y ≠ ∑_{i=1}^{m} α_{i}∗ x_{i})).

In each of the theories T_{n}, we can express the formula ∃y ∀ααα y ≠ ∑ _{i=1}^{m} α_{i} ∗ x_{i} without quantified vector-variables. Kuzichev gives the corollary that, if U is a complete theory of the scalar-field, then T_{n}∪ U is complete.

However, these complete theories T_{n}∪ U are never model-complete, unless n = 1. They are not even inductive: the union of a chain of models need not be a model (no matter what U is, unless n = 1; see §2 below). The problem is the lack of a way to express linear independence with an existential formula. The picture changes if predicates for linear independence or dependence are added.

I arrive, myself, at the example of vector-spaces by noting first that, in the Elements [5], Euclid gives a geometric formulation of certain field-theoretic identities. For example, the identity (x+y)(x−y)+y^{2} = x^{2} is Euclid’s Proposition II.5, but Euclid expresses it in terms of the squares and rectangles bounded by certain straight lines (������� �������� what we might call line-segments; see Figure 0.1).

At the beginning of the Geometry [2], René Descartes shows how straight lines (lignes droites) can be multiplied to produce lines rather than rectangles, if one line is chosen as unit:

x  y  x − y

Fig. 0.1 Euclid’s II.5

D A  B E C

Fig. 0.2 Descartes’s geometric multiplication

Soit par exemple AB l’vnité, & qu’il faille multiplier BD par BC, ie n’ay qu’a ioindre les poins A & C, puis tirer DE parallele a CA, & BE est le produit de cete Multiplication^{1} [Fig. 0.2].

By means of Descartes’s observation, we can interpret the scalar-field in a vector-space of dimension at least two by means of the binary relation of parallelism, that is, binary linear dependence (§1). So vector-spaces of dimension at least two are axiomatizable, as one-sorted structures, in the signature of abelian groups with a binary predicate. Also, the axioms can be chosen to be ∀∃.

When the predicate for parallelism is used, then the existentially closed vectorspaces are two-dimensional. (It does not matter whether a separate sort for the scalars is retained or not.) If, more generally, an n-ary predicate for linear dependence is used, then the existentially closed vector-spaces are n-dimensional over algebraically closed fields (§2). The class of such models being elementary, its theory is model-complete, although it does not admit full quantifier-elimination.

On the value of looking at basic structures, I quote again Descartes, this time from near the end of the fourth of his Rules for the Direction of the Mind [4]:

Quant à moi, conscient de ma faiblesse, j’ai décidé d’observer opiniâtrement, dans ma quête de connaissances, un ordre tel qu’en partant toujours des choses les plus simples et les plus faciles, je m’interdise de passer à d’autres, avant que dans les premières il ne m’apparaisse qu’il ne reste plus rien à désirer; c’est pourquoi j’ai poussé jusqu’à ce jour, aussi loin que j’ai pu, l’étude de cette mathématique universelle…^{2}

The result about existentially closed vector-spaces means, in part, that a vectorspace of n+1 dimensions can be embedded in an n-dimensional space so that linear independence of n-element sets (more precisely, n-tuples) is preserved. A sim-

1 ‘For example, let AB be taken as unity, and let it be required to multiply BD by BC. I have only to join the points A and C, and draw DE parallel to CA; then BE is the product of BD and BC’ [2, p. 5]. 2 ‘Aware how slender my powers are, I have resolved in my search for knowledge of things to adhere unswervingly to a definite order, always starting with the simplest and easiest things and never going beyond them till there seems to be nothing further which is worth achieving where they are concerned. Up to now, therefore, I have devoted all my energies to this universal mathematics… ’ [3, p. 20].

ilar result arises in the model-theory of fields: Let (a_{0},...,a_{n}) be algebraically independent over a field K, and let (b,c) be a generic solution to ∑ _{i=0}^{n} a_{i}x^{i} = y. (This generalizes [12, Example 8.1.2, p. 291]; see also [13, Example 2.1.8, p. 77].) Then tr-deg(K(a_{0},...,a_{n})/K) = n + 1, while tr-deg(K(a_{0},...,a_{n},b,c)/K(b,c)) = n, although every n-tuple of elements of K(a_{0},...,a_{n}) that is algebraically independent over K is still independent over K(b,c).

Recently and independently, Moshe Kamensky [9] has worked with (twosorted) vector-spaces and has given theories of them that have elimination of quantifiers; this elimination is achieved by means of additional sorts, as for the Grassmannians of the finite powers of the scalar-field.

1 Interpretation of the field in the vector-space

In a chapter of his own textbook on the subject, Robin Hartshorne [6, ch. 3] presents Descartes’s approach to geometry. It is perhaps a Cartesian spirit that allows Alfred Tarski [17,18] to axiomatize Euclidean geometry by means of the ternary relation of between-ness and the quaternary relation of equidistance; these relations allow the underlying (real-closed) field to be recovered from the space.

In the present section, I specify an origin in space and work with the groupstructure determined by it; then only a binary relation is needed to recover the underlying (arbitrary) field. This observation was useful to me in showing that a field equipped with a space and Lie-ring of derivations can be described as a onesorted structure in two ways: as a field with certain operators, or as a Lie-ring with certain operators.

A vector-space can be defined as a triple (V,K,∗), where V is an abelian group (of vectors), K is a field (of scalars), and ∗ is a function (x,v v v) ↦ x∗v v vfrom K ×V to V so that:

1. the functions v v v ↦ a ∗ v v v(where a ∈ K) are endomorphisms of V, and

2. the function x ↦ (v v v↦ x∗v v v) is a ring-homomorphism from K into (End(V),∘).

Since K is a field, the homomorphism into (End(V),∘) is an embedding, unless V is trivial; excluding this case, we may treat the homomorphism as an inclusion, so that multiplication in K is literally composition. Even in the trivial case, let us retain the symbol for composition to denote multiplication of scalars.

Model-theoretically then, a vector-space is a two-sorted structure, in the signature {+,−,000,∘,0,1,∗}; here the elements of {+,−} do double duty, taking arguments from the sort of vectors or the sort of scalars. I shall use normal-face variables for scalars (as 0), and boldface for vectors (as 000) or, in more general contexts, for tuples of variables.

In every vector-space, the binary relation ∥ on the sort of vectors is defined by the sentence

x x x∥ y y y↔ ∃u ∃v (u ∗ x x x+ v ∗ y y y= 000∧ (u ≠ 0 ∨ v ≠ 0)).  (1.1)

(Here and throughout the paper, outer universal quantifiers are suppressed.) The sentence (1.1) has the form

α ↔ ∃z_{0}··· ∃z_{n−1} β,  (1.2)

where α and β are quantifier-free, and none of the z_{i} appears in α; such a sentence is equivalent to the conjunction of the ∀∃-sentence ∃z_{0}··· ∃z_{n−1} (α → β) and the universal sentence β → α.

Let VS_{2} be the theory of vector-spaces that have been expanded to the signature {+,−,000,∘,0,1,∗,∥} so as to satisfy (1.1). (The subscript 2 alludes to the number of arguments that ∥ takes.) Models of the theory VS_{2} can be extended so as to satisfy also

∃x x x∃y y yx x x∦ y y y.  (1.3)

Let VS_{2}^{m} be the theory of the resulting structures: the vector-spaces, with parallelism, of dimension at least two. (The superscript ‘m’ refers to a minimum dimension.) This theory is inductive.

Reduction of a one-sorted structure is the discarding of some named operations or relations; we may understand reduction of a many-sorted structure to involve also the discarding of some sorts. In this sense, every model (V,K,∗,∥) of VS_{2}^{m} has a one-sorted reduct (V,∥) in the signature {+,−,000,∥}. This reduct is an abelian group with a certain binary relation; we might just call the reduct an abelian group with parallelism. Let VS_{2}^{r} be the theory of these structures. The theories VS_{2}^{m} and VS_{2}^{r} will be related in Theorem 1.1.

In general, the models of a theory T in a signature L are the objects of a category whose morphisms are either embeddings or elementary embeddings. Let the two possibilities for the category be Mod^{⊆} (T) and Mod^{≼}(T) respectively. If L ⊆ L′, and T′is a theory of L′, and reducts to L of models of T′are models of T, then we may speak of reduction from T′to T: it is a functor R from Mod^{≼}(T′) to Mod^{≼}(T), and from Mod^{⊆} (T′) to Mod^{⊆} (T) (this is a trivial case of Lemma 1.1 below).

Possibly, along with the reduction-functor R from Mod^{≼}(T′) to Mod^{≼}(T), there is an expansion-functor E from Mod^{≼}(T) to Mod^{≼}(T′) such that R ∘ E is the identity, and for each model 𝔄 of T′, there is a ‘reasonable’ isomorphism σ_{ER}^{𝔄} from 𝔄 to E(R(𝔄))—reasonable in the sense that, for all models 𝔄 and 𝔄^{∗} of T′, for every elementary embedding h of 𝔄 in 𝔄^{∗}, the following diagram commutes:

𝔄 −−⟶^{h}  𝔄^{∗}
σ_{EF}^{𝔄} ↓  ↓_{σ_{ER}^{𝔄^{∗}}}
E(R(𝔄)) −−−−→_{E(R(h))} E(R(𝔄^{∗}))

In a word then, R is an equivalence of categories; we might say also that R is a weakly conservative reduction. For example, R is weakly conservative in case T′ is VS_{2}, and L is {+,−,000,∘,0,1,∗} (so that T is just the theory of vectorspaces). However, in this case, E is not functorial on Mod^{⊆} (T). For example, (ℂ,ℝ,∗) ⊆ (ℂ,ℂ,∗), but (ℂ,ℝ,∗,∥) ⊈ (ℂ,ℂ,∗,∥). This is a point to be developed in §2. Briefly, E is not functorial here, because non-parallelism does not have an existential definition. In cases where E is functorial on Mod^{⊆} (T), and the diagram above commutes whenever h embeds 𝔄 in 𝔄^{∗}, so that R is an equivalence of Mod^{⊆} (T′) and Mod^{⊆} (T),—in such cases, we may say that R is simply a conservative reduction.

Now the statement of Theorem 1.1 makes sense. For the proof, I first note that reduction and expansion are instances of interpretation. In the account of Wilfrid Hodges [7, §5.3, p. 212], an interpretation of a (one-sorted) structure 𝔄 whose signature is L in a structure 𝔅 whose signature is L′consists, for some positive integer n, of:

1. a function φ ↦ φ_{I} converting each k-ary unnested atomic formula of L, for each k in ω, into an nk-ary formula of L′,

2. an n-ary formula δ_{I} of L′, and

3. a surjective function f_{I}^{𝔅} from δ_{I}^{𝔅} to A, such that

𝔅 ⊧ φ_{I}(b b b) ⟺ 𝔄 ⊧ φ(f_{I}^{𝔅}(b b b))  (1.4)

for all b b bfrom δ_{I}^{𝔅}.

We may assume that the universe A of 𝔄 is literally the set δ_{I}^{𝔅}, modulo the equivalence-relation defined in 𝔅 by (x = y)_{I}. Then f_{I}^{𝔅} is the quotient-map, and 𝔄 is uniquely determined by 𝔅 and φ ↦ φ_{I} and δ_{I} [7, 5.3.3, p. 216]: we may write 𝔄 = I(𝔅). Thus we have a function I converting structures of L′into structures of L.

In case 𝔄 has several sorts, composing a tuple (A_{α} : α ∈ S) perhaps, then the definition must be modified: For each α in S, for some positive integer n_{α}, there will be an formula δ_{I,α} in some n_{α} -tuple of variables (each variable being assigned to a sort), along with a function f_{I,α}^{𝔅} from δ_{I,α}^{𝔅} onto A_{α}, so that a variant of (1.4) holds, namely,

𝔅 ⊧ φ_{I}(b b b_{α(0)},...,b b b_{α(k−1)} ) ⟺ 𝔄 ⊧ φ(f_{I,α(0)}^{𝔅}(b b b_{α(0)}),...,f_{I,α(k−1)}^{𝔅} (b b b_{α(k−1)} ))

(1.5)

where b b b_{α(j)} ∈ δ_{I,α(j)} ^{𝔅}.

The function φ ↦ φ_{I} extends so that its domain comprises all unnested formulas of L, and (1.4) or (1.5) still holds [7, 5.3.2, p. 214]: the extension takes φ ∧ ψ to φ_{I} ∧ ψ_{I}, and ¬φ to ¬(φ_{I}), and ∃x φ to ∃(x^{0},...,x^{n−1} )(φ_{I} ∧ δ_{I}(x^{0},...,x^{n−1} )) (with appropriate modifications in the many-sorted case).

If there are theories T of L and T′ of L′ such that I(𝔅) ⊧ T whenever 𝔅 ⊧ T′, then let us say that I is an interpretation from T′to T. In this case, we can understand I as a functor from Mod^{≼}(T′) to Mod^{≼}(T), where, if 𝔅 and 𝔅^{∗} are models of T′, and h is an elementary embedding of 𝔅 in 𝔅^{∗}, then I(h) is the well-defined elementary embedding of I(𝔅) in I(𝔅^{∗}) given by

I(h)(f_{I}^{𝔅}(b b b)) = f_{I}^{𝔅^{∗}}(h(b b b))  (1.6)

[7, 5.3.4(a), p. 217]. If the formulas involved in I are simple enough, then more follows:

Lemma 1.1 If I is an interpretation from T′ to T (and therefore a functor from Mod^{≼}(T′) to Mod^{≼}(T)), then I is also a functor from Mod^{⊆} (T′) to Mod^{⊆} (T), provided both that the formula δ_{I} is existential, and also that the formula φ_{I} is existential whenever φ is an unnested atomic formula of L, or is ¬(x = y), or is ¬Rx^{0}··· x^{k−1} for some predicate R in L.

Proof The claim is a variant of [7, 5.3.4(b), p. 217] and a refinement of [7, §5.4, exercise 3, p. 225].

An interpretation I from T′to T, paired with an interpretation J from T to T′, is a bi-interpretation of T′and T if there are formulas χ_{IJ} of L, and χ_{JI} of L′, such that, whenever 𝔄 ⊧ T, then the set

{(a,f_{I}^{J(𝔄)}(f_{J}^{𝔄}(b b b_{0}),...,f_{J}^{𝔄}(b b b_{n−1} ))): 𝔄 ⊧ χ_{IJ}(a,b b b_{0},...,b b b_{n−1} )}  (1.7)

is (the graph of) an isomorphism σ_{IJ}^{𝔄} from 𝔄 to I(J(𝔄)), and similarly for all models of T′, with the places of I and J reversed (Hodges [7, §5.4(c), p. 222], generalizing Ahlbrandt and Ziegler [1, p. 67]; in the case of several sorts, there will be several formulas χ_{IJ,α}, indexed with the sorts, and the graph of σ_{IJ}^{𝔄} will have components of the form {(a,f_{I,α}^{J(𝔄)}(f_{J,β(0)}^{𝔄}(b b b_{0}),...,f_{J,β(n_{α} −1)}^{𝔄}(b b b_{n_{α} −1} ))): 𝔄 ⊧ χ_{IJ,α}(a,b b b_{0},...,b b b_{n_{α} −1} )}). A special case was alluded to above, where reduction can be ‘undone’ by an expansion.

Lemma 1.2 If (I,J) is a bi-interpretation of T′ and T, then I is an equivalence of the categories Mod^{≼}(T′) and Mod^{≼}(T); if I and J are also functorial between Mod^{⊆} (T′) and Mod^{⊆} (T), then these categories too are equivalent, provided that the formulas χ_{IJ} and χ_{JI} are existential.

Proof To prove the first claim, if 𝔄 and 𝔄^{∗} are models of T, and h is an elementary embedding of 𝔄 in 𝔄^{∗}, then we show that the following diagram commutes (and likewise for models of T′):

𝔄 −−⟶^{h}  𝔄^{∗}
σ_{IJ}^{𝔄} ↓  ↓_{σ_{IJ}^{𝔄^{∗}}}
I(J(𝔄)) −−⟶_{I(J(h))} I(J(𝔄^{∗}))

Suppose a ∈ A (and all models are one-sorted; extra sorts would be a challenge only to the notation.) Then (abbreviating the notation in (1.7)) we have σ_{IJ}^{𝔄}(a) = f_{I}^{J(𝔄)}(f_{J}^{𝔄}(b b b)) for some b b bsuch that 𝔄 ⊧ χ_{IJ}(a,b b b). Then 𝔄^{∗} ⊧ χ_{IJ}(h(a),h(b b b)) since h is elementary, so by (1.6)

σ_{IJ}^{𝔄^{∗}}(h(a)) = f_{I}^{J(𝔄^{∗})}(f_{J}^{𝔄^{∗}}(h(b b b))) = f_{I}^{J(𝔄^{∗})}(J(h)(f_{J}^{𝔄}(b b b)))

= I(J(h))(f_{I}^{J(𝔄)}(f_{J}^{𝔄}(b b b)) = I(J(h))(σ_{IJ}^{𝔄}(a)).

So the diagram does commute, and the first claim is proved. If h is merely an embedding, but I(h) is still well-defined as an embedding by (1.6), then the same argument works, provided also χ_{IJ} is existential. ⊓⊔

Now let us return to the special case of reductions and expansions. The following lemma singles out some of the basic properties of vector-spaces to be used in proving Theorem 1.1.

Lemma 1.3 Suppose (V,K,∗,∥) ⊧ VS_{2}^{m}.

1. Say x x x,y y y∈ V, and x x x ≠ 0. Then

x x x∥ y y y ⟺ ∃u u ∗ x x x= y y y ⟺ ∃!u u ∗ x x x= y y y.

2. The relation ∥, restricted to V ∖ {000}, is an equivalence-relation.

3. The set {y y y∈ V : x x x∥ y y y} is a subgroup of V, for all x x xin V.

4. Let x x x, zzz, and w w w be vectors in V such that x x x∦ zzz; let u ∈ K; and let y y y= u ∗ x x x.

Then

u ∗ zzz= w w w ⟺ zzz∥ w w w & x x x− zzz∥ y y y− w w w.

Proof I write a proof for item 4 only, assuming items 1, 2, and 3. Assume x x x∦ zzz and y y y= u∗x x x. Part of item 3 is that 000 is parallel to every vector; so zzz ≠ 000. Similarly, but with the help of item 2, we have zzz∦ x x x− zzz, so x x x− zzz ≠ 000. Hence, if u ∗ zzz= w w w, then zzz ∥ w w w by item 1, and also y y y− w w w = u ∗ (x x x− zzz), which is parallel to x x x− zzz for the same reason. Conversely, say zzz ∥ w w w. Then w w w = t ∗ zzz for some t in K, so that y y y− w w w = u ∗ x x x− t ∗ zzz = u ∗ (x x x− zzz) + (u − t) ∗ zzz. If also x x x− zzz ∥ y y y− w w w, then (u − t) ∗ zzz∥ x x x− zzzby item 3, so u = t. ⊓⊔

Theorem 1.1 Reduction from VS_{2}^{m} to VS_{2}^{r} is conservative.

Proof We have R from Mod^{⊆} (VS_{2}^{m}) to Mod^{⊆} (VS_{2}^{r}). To go the other way, we want to interpret an arbitrary model (V,K,∗,∥) of VS_{2}^{m} in its reduct, (V,∥), obtaining an expansion-functor E. (It will follow that the reducts (V,∥) compose an elementary class.) In the notation for interpretations given earlier, we shall need formulas δ_{E,vec} and δ_{E,sca}; these will be x x x= x x xand

x x x_{0} ≠ 000∧ x x x_{0} ∥ x x x_{1},

respectively. Then f_{E,vec}^{(V,∥)}will be the identity on V, while f_{E,sca}^{(V,∥)}will be given by

f_{E,sca}^{(V,∥)}(aaa_{0},aaa_{1}) = b ⟺ (V,K,∗,∥) ⊧ b ∗ aaa_{0} = aaa_{1}.  (1.8)

Indeed, the function f_{E,sca}^{(V,∥)}is well defined on δ_{E,sca}^{(V,∥)}, and is surjective onto K, by Lemma 1.3 (item 1):

1. If (V,∥) ⊧ δ_{E,sca}(aaa_{0},aaa_{1}), then there is a unique b in K such that (V,K,∗,∥) ⊧ b ∗ aaa_{0} = aaa_{1}.

2. If b ∈ K, and aaa ≠ 000, then (V,∥) ⊧ δ_{E,sca}(aaa,b ∗ aaa).

Let f_{E,sca}^{(V,∥)}be denoted by

(x x x,y y y) ↦ [x x x: y y y].

We have to define the function φ ↦ φ_{E}. This will be the identity at all formulas with no scalar-variables. It is now enough to suppose that φ is one of

x = y, x + y = z, x ∘ y = z, x ∗ y y y= zzz.

The formula (x = y)_{E} will be the equation

[x x x_{0} : x x x_{1}] = [y y y_{0} : y y y_{1}],  (1.9)

expressed in {+,−,0,∥}. To obtain this expression, first note that

y y y_{0} ≠ 000 & [x x x_{0} : x x x_{1}] ∗ y y y_{0} = y y y_{1} ⟺ [x x x_{0} : x x x_{1}] = [y y y_{0} : y y y_{1}].  (1.10)

Now let ψ(x x x_{0},x x x_{1},y y y_{0},y y y_{1}) denote the formula

x x x_{0} ∦ y y y_{0}∧ x x x_{0} ∥ x x x_{1}∧ y y y_{0} ∥ y y y_{1}∧ x x x_{0}− y y y_{0} ∥ x x x_{1}− y y y_{1}.

(The situation can be illustrated by Fig. 0.2 of §0, with (A,B,C,D,E) replaced with (x x x_{0},000,y y y_{0},x x x_{1},y y y_{1}).) This formula ψ defines a subset of δ_{E,sca}^{(V,∥)}× δ_{E,sca}^{(V,∥)}; that is, it defines a binary relation on δ_{E,sca}^{(V,∥)}. This relation is symmetric, though not reflexive, and not quite transitive. However, by Lemma 1.3 (item 4) and (1.10), and by the assumption that dim_{K}V ⩾ 2, we have

[x x x_{0} : x x x_{1}] = [y y y_{0} : y y y_{1}] & x x x_{0} ∦ y y y_{0} ⟺ ψ(x x x_{0},x x x_{1},y y y_{0},y y y_{1}); [x x x_{0} : x x x_{1}] = [y y y_{0} : y y y_{1}] & x x x_{0} ∥ y y y_{0} ⟺ x x x_{0} ∥ y y y_{0} & ∃zzz_{0} ∃zzz_{1}

(ψ(x x x_{0},x x x_{1},zzz_{0},zzz_{1}) & ψ(zzz_{0},zzz_{1},y y y_{0},y y y_{1})).

From these observations, we obtain (1.9) as a formula of {+,−,0,∥}. A slight simplification is possible: (x = y)_{E} can be the existential formula

∃zzz_{0} ∃zzz_{1} (ψ(x x x_{0},x x x_{1},y y y_{0},y y y_{1}) ∨ (ψ(x x x_{0},x x x_{1},zzz_{0},zzz_{1}) ∧ ψ(zzz_{0},zzz_{1},y y y_{0},y y y_{1}))).  (1.11)

We obtain the remaining formulas φ_{E} by means of (1.10) and the following identities:

[x x x: y y y] + [x x x: zzz] = [x x x: y y y+ zzz];
[y y y: zzz] ∘ [x x x: y y y] = [x x x: zzz].

In particular, writing (1.9)as an abbreviation for (1.11), we can tabulate the results:

\begin{matrix}φ & φ_{E} \\ x + y = z & ∃w w w([x x x_{0} : w w w] = [y y y_{0} : y y y_{1}] ∧ [x x x_{0} : x x x_{1}+ w w w] = [zzz_{0} : zzz_{1}]) \\ x ∘ y = z & ∃w w w([y y y_{1} : w w w] = [x x x_{0} : x x x_{1}] ∧ [y y y_{0} : w w w] = [zzz_{0} : zzz_{1}]) \\ x ∗ y y y= zzz & [x x x_{0} : x x x_{1}] = [y y y: zzz] ∨ (y y y= 000∧ zzz= 000). \end{matrix}

These formulas φ_{E} are existential. Also, ¬((x = y)_{E}) is equivalent to the existential formula

∃w w w([x x x_{0} : x x x_{1}] = [y y y_{0} : w w w] ∧ w w w ≠ y y y_{1}).

Now we have E as a functor from Mod^{⊆} (VS_{2}^{r}) to Mod^{⊆} (VS_{2}^{m}), by Lemma 1.1. The composition R ∘ E is the identity, and σ_{RE}^{(V,∥)}is the identity, and χ_{RE} is x x x= y y y. For the other side, σ_{ER}^{(V,K,∗,∥)}is the identity on V, while on K it takes y to the equivalence-class {(x x x_{0},x x x_{1}): x x x_{0} ≠ 000 & y ∗ x x x_{0} = x x x_{1}}; correspondingly, χ_{ER,vec} is x x x= y y y, while χ_{ER,sca}is x x x_{0} ≠ 000 & y∗x x x_{0} = x x x_{1}. By Lemma 1.2, the proof is complete.

⊓⊔ 2 Existentially closed vector-spaces

It was said in §0 that, if U is a complete theory of fields, then the theory, in {+,−,000,∘,0,1,∗}, of n-dimensional vector-spaces whose scalar-fields are models of U is complete, but not model-complete or even inductive, if n > 1. Indeed, suppose V is a vector-space with basis (b b b_{0},...,b b b_{n−1} ) over a model K of U, and n > 1. If K ⊂ K′, then the b b b_{i} span a vector-space W over K′, but we can have b b b_{0} = a ∗ b b b_{1} for some a in K′∖ K, so that dim_{K′}W ⩽ n − 1. Still, (V,K,∗) is a substructure of (W,K′,∗). We can have K′⊧ U, and we can extend W to an n-dimensional space V′ over K′. So (V,K,∗) is a substructure of (V′,K′,∗), and both are models of T_{n}∪ U. Continuing, we form a chain

(V,K,∗) ⊂ (V′,K′,∗) ⊂ ···⊂ (V^{(k)},K^{(k)},∗) ⊂ ···  (2.1)

of models of T_{n}∪ U; the union of this chain has dimension at most n − 1. The chain can have dimension one, even if n = ∞: for each k, let V^{(k)} have basis (b b b_{k},b b b_{k+1},...), and assume b b b_{k} = a_{k}∗ b b b_{k+1} for some a_{k} in K^{(k+1)} ∖ K^{(k)}.

However, when the structures in (2.1)expand to models of VS_{2}^{m}, they no longer form a chain: non-parallelism is not preserved in super-structures. Nonetheless, we shall see that there are chains where non-parallelism is preserved in going up, but the union has dimension two. The conclusion will be that the existentially closed models of VS_{2}^{m} are two-dimensional. There is a generalization involving chains that preserve n-ary linear independence.

If n > 0, let P^{n} be an n-ary predicate for linear dependence. (So P^{2}x x xy y y means x x x∥ y y y; but P^{1} is superfluous, since P^{1}x x x is equivalent to x x x= 000.) For each positive n, there is a theory VS_{n} of vector-spaces in the signature {+,−,000,∘,0,1,∗,P^{n}}, axiomatized by the usual vector-space axioms, along with

P^{n}x x x_{0}··· x x x_{n−1} ↔ ∃y^{0}··· ∃y^{n−1} ( ∑_{i<n} y^{i}∗ x x x_{i} = 000∧ ⋁_{i<n} y^{i} ≠ 0) .  (2.2)

Having the form of (1.2), the axiom (2.2) is equivalent to an ∀∃-sentence. So VS_{n} is inductive. Models of VS_{n} have two sorts. But let VS_{n}^{m} be the theory of models of VS_{n} of dimension at least n; so VS_{n}^{m} has the additional axiom

∃x x x_{0}··· ∃x x x_{n−1} ¬P^{n}x x x_{0}··· x x x_{n−1} .

In this theory, when n ⩾ 2, we can define non-parallelism and parallelism in VS_{n}^{m} by means of the existential formulas

∃(x x x_{2},...,x x x_{n−1} ) ¬P^{n}x x x_{0}··· x x x_{n−1} ,

∃(x x x_{2},...,x x x_{n}) ( x x x_{1} = 0 ∨ (¬P^{n}x x x_{1}··· x x x_{n}∧ ⋀_{j=2}^{n} P^{n}x x x_{0}··· x x x_{j−1} x x x_{j+1} ··· x x x_{n})) .

Indeed, if (aaa_{1},...,aaa_{n}) is linearly independent, but (aaa_{0},...,aaa_{i−1} ,aaa_{i+1} ,...,aaa_{n}) is not, then aaa_{0} is a unique linear combination of (aaa_{1},...,aaa_{n}), and this combination does not use aaa_{j}. If that is so, whenever 2 ⩽ j ⩽ n, then aaa_{0} must be a multiple of aaa_{1}. If we reduce a model of VS_{n}^{m} to the sort of vectors, in the signature {+,−,000,P^{n}}, the reduct might be termed an abelian group with n-ary linear dependence. As a porism from Theorem 1.1, we have that the reduction from VS_{n}^{m} to the theory of abelian groups with n-ary linear dependence is conservative. By Theorem 2.3 below, the model-companion of VS_{n}—hence, of VS_{n}^{m}—is the theory VS_{n}^{∗} of ndimensional vector-spaces over algebraically closed fields. Hence the theory of abelian groups with n-ary linear dependence is likewise companionable.

To warm up for the proof of Theorem 2.3, I consider first VS_{1}, the theory of non-trivial vector-spaces. I shall generally write models as (V,K), rather than the full (V,K,∗):

Theorem 2.1 The theory VS_{1} is companionable; its model-companion is the theory VS_{1}^{∗}. The model-companion is not a model-completion; much less does it admit quantifier-elimination; but it is the model-completion of the theory of vectorspaces of dimension at most 1.

Proof Suppose (V,K) ⊧ VS_{1} and has basis B. We may assume that B is a subset of a field extending K (while still being linearly independent over K). Then we can form (K(B)^{alg},K(B)^{alg}), a model of VS_{1}^{∗} in which (V,K) embeds.

Suppose (V,K) ⊧ VS_{1}^{∗} and is a substructure of the models (W,L) and (W′,L′), which have equal cardinality greater than |K|. Then |L| = |L′|, so L ≅ L′over K; hence

(W,L) ≅ (L ⊗_{K}V,L) ≅ (L′⊗_{K}V,L′) ≅ (W′,L′)

over (V,K). So VS_{1}^{∗}∪diag(V,K)is categorical in powers greater than |K|; having also no finite models, the theory is complete. Therefore VS_{1}^{∗} is model-complete, so it is the model-companion of VS_{1}.

In the foregoing argument, it is enough to suppose merely that (V,K) is onedimensional; K need not be algebraically closed. Even if V = {000}, the theory VS_{1}^{∗} ∪ diag(V,K)is complete. This shows that VS_{1}^{∗} is the model-completion of the theory of vector-spaces of dimension at most 1.

The model (ℚ^{alg},ℚ^{alg}) of VS_{1}^{∗} has the two substructures (⟨1,√ 2⟩,ℚ) and (⟨1,√ 3⟩,ℚ), which are two-dimensional isomorphic models of VS_{1}, although the formula

∃z (z ∘ z = 1 + 1 ∧ z ∗ x x x_{0} = x x x_{1})

is satisfied in (ℚ^{alg},ℚ^{alg}) by (1,√ 2), but not by (1,√ 3). Therefore the theory VS_{1}^{∗} ∪ diag(⟨1,√ 2⟩,ℚ)is the same as VS_{1}^{∗} ∪ diag(⟨1,√ 3⟩,ℚ)(as long as the same symbol denotes √ 2 and √ 3 respectively), but this theory is not complete. Thus VS_{1}^{∗} is not a model-completion of VS_{1}. ⊓⊔

Proving the more general Theorem 2.3 below requires some preliminary work on matrices. I shall understand an m × n matrix (m rows, n columns) as a function on m×n, that is, on {(i,j) ∈ ω^{2}: i < m & j < n}. Such a function can be denoted by

(u_{j}^{i})_{j<n}^{i<m} ;

its transpose is (u_{j}^{i})_{i<m}^{j<n}. I shall consider elements of a Cartesian power like K^{n} as row-vectors, that is, 1 × n matrices.

Lemma 2.1 For all positive integers n, if U is an n × n matrix (over some field), and u u uis n × 1, and aaa is 1 × n, then

det( \begin{matrix}U & u u u \\ aaa & 1 \end{matrix}) = det(U − u u u· aaa).  (2.3)

Proof Start with the identity

( \begin{matrix}U & u u u \\ aaa & 1 \end{matrix}) · ( \begin{matrix}I_{n} & 000 \\ −aaa & 1 \end{matrix}) = ( \begin{matrix}U − u u u· aaa & u u u \\ 000 & 1 \end{matrix})

and take the determinant of either side. ⊓⊔

The lemma can be interpreted as follows. Let K be a field, and let V be K^{n+1} . The space of alternating n-forms on V has dimension \binom{n+1}{n}, or n + 1. Now understand V^{n} as comprising the n × (n + 1) matrices over K. The func-

tion ( U u u u) ↦ det( \begin{matrix}U & u u u \\ aaa & 1 \end{matrix}) from V^{n} to K is an alternating n-form on V that takes

( I_{n} 000) to 1, and that takes ( U u u u) to 0 if one of its rows is ( aaa 1). There is only one such function; the function ( U u u u) ↦ det(U − u u u· aaa) has the same properties; (2.3) follows.

Suppose further π_{i} is x x x ↦ x_{i} on V, so π_{i} ∈ V^{∗}. If B ∈ V^{n}, let ΦB be the func-

tion det( \frac{B}{π_{0} ···π_{n}} ) : this is an element ∑ _{i=0}^{n} c^{i}· π_{i} of V^{∗}. Then (c^{0},...,c^{n}) is the

cross-product [16, pp. 83 f.] of (the rows of) B: it is the element ×B of V such that x x x· (×B) = ΦBx x xfor all x x xin V.

Lemma 2.2 Let K be a field, V = K^{n+1} , and B ∈ V^{n}. Say K ⊂ L, and aaa ∈ L^{n+1} , and aaa is linearly independent over K. The following are equivalent:

1. ×B = 0;

2. det( \frac{B}{aaa}) = 0;

3. The rows of B are linearly dependent over K;

4. The rows of B are linearly dependent over L.

Proof The equivalence of (1) and (2) follows from the definition of ×B and the linear independence of aaa over K. The equivalence of (3) and (4) follows from the observation that if the equation x x x·B = 000 has a non-trivial solution at all, it has one in K^{n}. Finally, aaa is not in the span over L of the rows of B: if it were, then ccc·B = aaa for some ccc in L^{n}, which would mean that the n + 1 entries of aaa belonged to the span over K of the n entries of ccc. Hence (2) and (4) are equivalent. ⊓⊔

Theorem 2.2 Suppose L/K is a field-extension, and [L : K] ⩾ n + 1. Then the vector-space (K^{n+1} ,K) embeds in (L^{n},L) so as to preserve linear independence of n-tuples: that is, the embedding is of the structure (K^{n+1} ,K,P^{n}) in (L^{n},L,P^{n}). One such embedding is

x x x ⟼→ x x x· ( \frac{I_{n}}{−aaa} ) ,  (2.4)

where aaa in L^{n} is such that (a_{0},...,a_{n−1} ,1) is linearly independent over K.

Proof Assume that (a_{0},...,a_{n−1} ,1) is linearly independent over K. Treating n vectors from K^{n+1} as the rows of an n × (n + 1) matrix, we can write the result as ( U u u u). By Lemma 2.2, the rows of ( U u u u) are linearly dependent over K if and only if

det( \begin{matrix}U & u u u \\ aaa & 1 \end{matrix}) = 0.  (2.5)

The images of those rows under the transformation in (2.4) are the rows of the

product ( U u u u) · ( \frac{I_{n}}{−aaa} ) . This product is U − u u u· aaa. So the images are linearly

dependent over L if and only if

det(U − u u u· aaa) = 0.  (2.6)

By Lemma 2.1, equations (2.5)and (2.6)are equivalent. Hence the transformation in (2.4) is an embedding that preserves independence of n-tuples. ⊓⊔

Not every embedding of (K^{n+1} ,K) in (L^{n},K) preserves independence of ntuples: Just use an embedding as in (2.4), but replace some—not all—entries of aaa with 0.

Theorem 2.3 For each positive n, the theory VS_{n}^{∗} is the model-companion of VS_{n}; it is not a model-completion of VS_{n} or even of VS_{n}^{m}, but is the modelcompletion of the theory of n-dimensional vector-spaces.

Proof The proof is, in part, as for Theorem 2.1. Since VS_{n} is inductive, every model embeds in an existentially closed model. Such models are models of VS_{n}^{∗}. Indeed, every model (V,K,P^{n}) of VS_{n} embeds in (K^{alg} ⊗_{K} V,K^{alg},P^{n}); so existentially closed models must have algebraically closed scalar-fields. Also, if dim_{K}V = m < n, then (V,K,P^{n}) fails to have a solution to

¬P^{n}x x x_{0}··· x x x_{n−1} ;  (2.7)

but (V,K,P^{n}) embeds in (V ⊕ K^{n−m},K,P^{n}), where (2.7) does have a solution; so (V,K,P^{n}) was not existentially closed. Finally, say dim_{K}V > n, so that there is a linearly independent (n+1)-tuple (aaa^{0},...,aaa^{n}) of vectors in V. Then (V,K,P^{n}) has no solution to

∑_{i=0}^{n} x^{i}∗ aaa_{i} = 000∧ ⋁_{i=0}^{n} x^{i} ≠ 0.  (2.8)

But analyse V as V_{0}⊕ V_{1}, where V_{0} is spanned by the vectors aaa^{i}. By Theorem 2.2, there is a model (W,L,P^{n}) of VS_{n} in which (V_{0},K,P^{n}) embeds, but which has a solution to (2.8). Then (V,K,P^{n}) embeds in (W ⊕ L ⊗_{K}V_{1},L,P^{n}), and the latter has a solution to (2.8). So again (V,K,P^{n}) was not existentially closed.

So the existentially closed models of VS_{n} are models of VS_{n}^{∗}; in particular, every model of VS_{n} embeds in a model of VS_{n}^{∗}. If (V,K,P^{n}) is an n-dimensional model of VS_{n}, then VS_{n}^{∗}∪ diag(V,K,P^{n})is complete, by a categoricity argument as in the proof of Theorem 2.1. Therefore VS_{n}^{∗} is the model-completion of the theory of n-dimensional models of VS_{n}.

However, VS_{n}^{∗} is not the model-completion of VS_{n}^{m} (much less of VS_{n}). Indeed, let (a_{0},...,a_{n}) be an (n+1)-tuple of algebraic numbers such that the (n+2)- tuple (a_{0},...,a_{n},1) is linearly independent over ℚ. By Theorem 2.2, the rowspaces of the matrices

( \frac{I_{n}}{a_{0} ···a_{n−1}} ) and ( \frac{I_{n}}{a_{1} ···a_{n}})

are substructures 𝔄 and 𝔅 of ((ℚ^{alg})^{n},ℚ^{alg},P^{n}). Being (n + 1)-dimensional, they are isomorphic models of VS_{n}^{m}; but no automorphism of ((ℚ^{alg})^{n},ℚ^{alg},P^{n}) takes 𝔄 to 𝔅. ⊓⊔

We can let VS_{∞} be the union of the theories VS_{n}; so it is the theory of vectorspaces in the signature {+,−,000,∘,0,1,∗,P^{1},P^{2},P^{3},...}. Let VS_{∞}^{∗} be the theory, in the same signature, of infinite-dimensional vector-spaces over algebraically closed fields.

Theorem 2.4 The theory VS_{∞}^{∗} is the model-completion of VS_{∞}, but does not admit quantifier-elimination.

Proof Every model (V,K,P^{1},...) of VS_{∞} embeds in the model

(K^{alg}⊗_{K}V ⊕ (K^{alg})^{ω} ,K^{alg},P^{1},...)

of VS_{∞}^{∗}. Also, let (V,K,P^{1},...) ⊧ VS_{∞}, and κ = ℵ_{0} + |V | + |K|. Then VS_{∞}^{∗} ∪ diag(V,K,P^{1},...) is complete, since all of its models (W,L,P^{1}) are isomorphic, provided tr-deg(L/K) = κ and dim_{L}(W /(L ⊗_{K} V)) = κ; but these are just the models of size κ that realize certain types. So VS_{∞}^{∗} is the model-completion of VS_{∞}.

Finally, the example at the end of the proof of Theorem 2.1 shows that VS_{∞}^{∗} does not admit elimination of quantifiers. Indeed, (⟨1,√ 2⟩,ℚ) expands to a substructure of a model of VS_{∞}^{∗} in which 1 ∥ √ 2, but VS_{∞}^{∗}∪diag(⟨1,√ 2⟩,P^{1},P^{2},...) is not complete, since it does not specify which scalars ensure that 1 ∥ √ 2. ⊓⊔

Theorem 2.5 The completions of the model-complete theories VS_{n}^{∗} are obtained by specifying a characteristic for the scalar field. The completions are ω-stable.

Proof Let VS_{n,p}^{∗} be the theory of models of VS_{n}^{∗} whose scalar fields have characteristic p (positive or zero). If n is finite, then VS_{n,p}^{∗} is uncountably categorical, hence complete and ω-stable.

All models of VS_{∞,p}^{∗} have a substructure isomorphic to ({000},𝔽_{p}), where 𝔽_{p} is a prime field of characteristic p. Hence VS_{∞,p}^{∗} ⊢ diag({000},𝔽_{p}). But here ({000},𝔽_{p}) ⊧ VS_{∞}, so the theory VS_{∞}^{∗}∪diag({000},𝔽_{p}) is complete by Theorem 2.4. Therefore VS_{∞,p}^{∗} is complete.

Finally, let (V,K) be a countable, definably closed substructure of a big model of VS_{∞}^{∗}. This implies that, if some vectors in V are linearly dependent, then scalars witnessing this can be found in K. A complete type of x x x over (V,K) says either that x x xis linearly independent from V, or—for some aaa_{i} in V —that x x x= ∑_{i<n} t^{i}∗ aaa_{i} for some scalars t^{i}. In the latter case, the type also specifies a variety over K of which (t^{0},...,t^{n−1} ) is a generic point. If (u^{0},...,u^{n−1} ) is another generic point of the same variety, there is an automorphism of the big model, over (V,K), taking ∑_{i<n} t^{i}∗aaa_{i} to ∑_{i<n} u^{i}∗aaa_{i}. Thus there are just countably many types of x x xover (V,K). Similarly for types of a scalar variable t: If V = {000}, then these types correspond to types over K, of which there are countably many. If V contains a non-zero vector aaa, then for every type p(t) over (V,K), there is a type of x x x that includes {∃t (x x x= t ∗ aaa∧ φ(t): φ ∈ p}; but the union of any two such sets is inconsistent.

⊓⊔

Acknowledgements I read Euclid and Descartes as a student at St John’s College, Annapolis and Santa Fe. At Logic Colloquium 2006 in Nijmegen, Ehud Hrushovski pointed out an error in an earlier version of this work (and informed me of Kamensky’s work [9]). The anonymous referee offered some helpful suggestions and corrections.

References

1. Ahlbrandt, G., Ziegler, M.: Quasi-finitely axiomatizable totally categorical theories. Ann. Pure Appl. Logic 30(1), 63–82 (1986). Stability in model theory (Trento, 1984)

2. Descartes: The Geometry of René Descartes. Dover Publications, Inc., New York (1954). Translated from the French and Latin by David Eugene Smith and Marcia L. Latham, with a facsimile of the first edition of 1637

3. Descartes: The Philosophical Writings of Descartes, vol. I. Cambridge University Press (1985). Translated by John Cottingham, Robert Stoothoff, and Dugald Murdoch

4. Descartes: Règles pour la direction de l’esprit. Classiques de la philosophie. Le Livre de Poche (2002). Traduction et notes par Jacques Brunschwig. Préface, dossier et glossaire par Kim Sang Ong-Van-Cung

5. Euclid: The thirteen books of Euclid’s Elements translated from the text of Heiberg. Vol. I: Introduction and Books I, II. Vol. II: Books III–IX. Vol. III: Books X–XIII and Appendix. Dover Publications Inc., New York (1956). Translated with introduction and commentary by Thomas L. Heath, 2nd ed

6. Hartshorne, R.: Geometry: Euclid and beyond. Undergraduate Texts in Mathematics. Springer-Verlag, New York (2000)

7. Hodges, W.: Model theory, Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press, Cambridge (1993)

8. Jensen, C.U., Lenzing, H.: Model-theoretic algebra with particular emphasis on fields, rings, modules, Algebra, Logic and Applications, vol. 2. Gordon and Breach Science Publishers, New York (1989)

9. Kamensky, M.: The model completion of the theory of modules over finitely generated commutative algebras. Http://arxiv.org/abs/math/0607418

10. Kuzichev, A.A.: Elimination of quantifiers over vectors in some theories of vector spaces. Z. Math. Logik Grundlag. Math. 38(5-6), 575–577 (1992)

11. Macintyre, A.: Model theory: geometrical and set-theoretic aspects and prospects. Bull. Symbolic Logic 9(2), 197–212 (2003). New programs and open problems in the foundation of mathematics (Paris, 2000)

12. Marker, D.: Model theory: an introduction, Graduate Texts in Mathematics, vol. 217. Springer-Verlag, New York (2002)

13. Pillay, A.: Geometric stability theory, Oxford Logic Guides, vol. 32. The Clarendon Press Oxford University Press, New York (1996). Oxford Science Publications

14. Robinson, A.: Complete theories, second edn. North-Holland Publishing Co., Amsterdam (1977). With a preface by H. J. Keisler, Studies in Logic and the Foundations of Mathematics, first published 1956

15. Rothmaler, P.: Introduction to model theory, Algebra, Logic and Applications, vol. 15. Gordon and Breach Science Publishers, Amsterdam (2000). Prepared by Frank Reitmaier, Translated and revised from the 1995 German original by the author

16. Spivak, M.: Calculus on manifolds. A modern approach to classical theorems of advanced calculus. Addison-Wesley Publishing Company, Reading, Massachusetts (1968). Corrected reprint of 1965 edition 17. Tarski, A.: What is elementary geometry? In: The axiomatic method. With special reference

to geometry and physics. Proceedings of an International Symposium held at the Univ. of Calif., Berkeley, Dec. 26, 1957–Jan. 4, 1958 (edited by L. Henkin, P. Suppes and A. Tarski), Studies in Logic and the Foundations of Mathematics, pp. 16–29. North-Holland Publishing Co., Amsterdam (1959)

18. Tarski, A., Givant, S.: Tarski’s system of geometry. Bull. Symbolic Logic 5(2), 175–214