An introduction to first-order logic
with emphasis on definability and o-minimality

by Vincent Bagayoko

November 2022

1First-order logic

1.1Structures and signatures

A signature is a family of function symbols with arities , together with of one of two types together with a family of relation symbols with arities . Among the relation symbols, there is always a particular symbol of arity denoted .

Given a signature , a first-order structure for is a set , together with a family of functions and a family of subsets called relations. Each of these defines a specific interpretation of the function and relation symbols. For instance a relation symbol of arity is interpreted by binary relation , a function of arity 0 is interpreted as a constant , a relation of arity is interpreted subset of . The equality symbol is always interpreted as the binary relation of equality on , i.e. as the diagonal .

We will consider certain properties of that pertain to these functions and relations, and which can be stated in a specific language involving symbols for each such function and relation. This language is called a first-order language.

Example 1. For instance, if we want to talk about the properties of the ordered field , then we will take two functions , namely the sum and the product, two constants and , and one binary relation, namely the standard ordering on , seen here as the subset of .

Example 2. If we want to talk about the properties of a vector field over , then we'll have the group operation on and, for each complex number , the scalar multiplication by :

1.2First-order language over a signature

Consider a fixed signature . We then define specific types and sets of words, i.e. finite strings of symbols, as follows:

The first-order language over this signature is the set of all -formulas.

If a symbol of variable occuring in a formula is preceded by a quantifier in one of its occurrences, then we say that it is bound. Otherwise, we say that it is free. Usually, we write denote by an -formula whose free variables are among .

A formula without free variable is called an -sentence. Those are the formulas which can be interpreted as true or false in structures (whereas formulas with free variables may have a truth value depending on the value of those variables).

1.3Prenex form and quantifier-free formulas

An -formula is said quantifier-free if it contains no occurrence of or . Quantifier-free formulas are thus boolean combinations of atomic formulas, i.e. obtained as conjunctions, disjunctions and negations (and combinations thereof) of atomic formulas.

Proposition 3. Every quantifier-free formula is is logically equivalent to a formula of the form

where , and each is either atomic or neg-atomic.

An -formula is in prenex normal form form if it is, up to permutation of the variable symbols, of the form

where is quantifier-free and are symbols of quantifiers (i.e. or ).

Proposition 4. Every -formula is logically equivalent to a formula in prenex normal form.


We fix a signature and an -structure . Given a formula and , we say that holds in if the straightforward interpretation of , where

is true.

Remark 5. Why first-order? Are there higher orders? First here refers to the fact that quantifiers in the language only apply to variables which range in elements, and not subsets of the structure. One could also have symbols of variable denoting subsets of , so that a formula in this higher-order language for the structure could state that has the least upper bound property.

But the first-order language does not allow this. It can be shown that there is no set of sentences in the first-order language over with one binary relation symbol such that -structure in which all sentences in hold are exactly linearly ordered sets with the least upper bound property.

1.5Quantifier elimination

Consider a first-order signature and an -structure . We say that eliminates quantifiers (or has quantifier elimination) if for every -formula , there is a quantifier-free -formula such that the following sentence holds in :

There are many tests in order to show that eliminates quantifiers. One of the most basic ones is the following

Proposition 6. Assume that for each and each quantifier-free formula , there is a quantifier-free formula such that the following holds in :

Then eliminates quantifiers.

Idea of proof. Prenex normal form induction.

2Definability and o-minimality

In this section, we fix a first-order signature and an -structure .

2.1Definable subsets

Given , we say that a set is definable in dimension in if and there are an , a tuple and a formula such that

We say that is definable without quantifiers if can be taken to be quantifier-free.

Example 7. In , the set is definable. Indeed, Lagrange's four squares theorem, an integer is positive if and only if it is a sum of for squares of integers. So

The set is not definable without quantifiers. Indeed, recall that quantifier-free formulas are equivalent to boolean combinations of atomic formulas. In , an atomic formula in one free variable is equivalent to an equality where . Hence it defines either if , or a finite subset otherwise. In particular, it defines a finite or cofinite (complement of a finite) subset of . Since the set of finite or cofinite subsets of is closed under unions and intersections, any boolean combination ot atomic formulas defines a finite or cofinite subset. So defines a finite or cofinite subset. Since is neither finite nor cofinite in , it cannot be defined by .

Remark 8. In fact, in , many things are definable. For instance, every recursively enumerable subset of is definable in dimension in .

2.2Formal-geometric correspondence

Here we fix an , an with , a tuple , as well as -formulas

We have the following list of correspondences between geometric operations on definable sets

and their defining formulas and .

Logical operation on defining formula Geometric operation on definable set
Negation Complement
Disjunction: Union
Conjunction: Intersection
Existential quantifier: Projection on .
Universal quantifier:

Thus the theory of definability can be stated in purely geometric terms. This is the spirit of [2]. However, many important results regarding definability (in particular in o-minimality) crucially rely on the interplay between intuitions coming from logic and geometry, algebra, analysis, graph theory, and so on...


Let be a linearly ordered set. An interval in is a subset of one of the following forms for :

The first four types of intervals are called open intervals.

Example 9. The set is not an interval in , whereas

is an interval in .

Proposition 10. Let be a linearly ordered set. Then the quantifier-free definable subsets of are exactly the finite unions of intervals in .

Definition 11. A first-order structure is said o-minimal if every definable subset of in dimension is a finite union of intervals in .

Corollary 12. If eliminates quantifiers, then it is o-minimal.

The set in Example 9 is definable in the ordered group . This set is not a finite union of intervals, otherwise it would have a least upper bound in . Therefore is not o-minimal.

O-minimal ordered fields. In the Fachseminar and in RAG I, we will see examples of o-minimal ordered fields. Here we consider the case of rational numbers. The ordered field is not o-minimal for similar reasons as above. What's more, by a theorem of Julia Robinson, the set of integers is definable in . So every definable set in is definable in . In view of Remark 8, we see that and are at the opposite ends of the spectrum of “tameness” of definable subsets.

Proposition 13. Assume that is o-minimal, and let where and , as a first-oder structure in the language with signature . Then is o-minimal.

Proof. -formulas are -formulas, and given an -formula and , the definable set is equal to , which is a finite union of intervals by o-minimality of , hence the result.

3Quantifier elimination for unary group representations

Let be a bi-ordered group. A unary representation of is a total order together with a morphism

where is the group under composition of strictly increasing bijections , such that for all , we have

Example 14. We get a unary representation

of by letting it act on itself by left translations, i.e. by setting for each .

Example 15. Consider the group with the reverse ordering defined by

This is still a bi-ordered group. We have a unary representation

of on its underlying linear ordering given by right translations: for each .

We now fix a unary representation of , and we consider the first-order structure in the first-order language with unary function symbols for each and a binary relation symbol . We then have

Theorem 16. (adapted from [1, Theorem 8]) Assume that is dense or that . Then has quantifier elimination in .

Proof. We first note that we have the following equivalences for and :


Now consider an existential formula for . So there are atomic and neg-atomic formulas such that

Each neg-atomic formula among the 's may be replaced by a disjunction of atomic formulas as in (3-4). Then as in (1-2), we may replace all atomic formulas by formulas of the form or for and . So each is equivalent to a formula

where each says that

for some , and . Note that the formula is false (hence equivalent to a quantifer-free formula) if is false. If this last formula is true, then is equivalent to

If is densely ordered, then this last formula is always true.

If and is not densely ordered, then consider the least element of . The formula is equivalent to

So in any case, the formula is equivalent to a quantifier-free formula.

Corollary 17. Any dense total order has quantifier elimination in , and is thus o-minimal.

Corollary 18. The structure is o-minimal.



B. Baizhanov, J. Baldwin, and V. Verbovskiy. Cayley's theorem for ordered groups: o-minimality. Sibirskie Èlektronnye Matematicheskie Izvestiya [electronic only], 4:278–281, 2007.


L. van den Dries. Tame topology and o-minimal structures, volume 248 of London Math. Soc. Lect. Note. Cambridge University Press, 1998.


holds in 2

atomic formula 1

definable subset 3

first-order language 2

first-order structure 1

-formula 2

free variable 2

neg-atomic formula 1

o-minimal structure 4

prenex normal form 2

quantifier elimination 3

quantifier-free formula 2

signature 1

term 1

unary representation 5

variable symbol 1


first-order language over 2

formula with free variables among 2

representation of a group by left translations on itself 5