Section 3.1: Natural Numbers with Successor
Consider
.
Axiomatization
Let
be the set of the following axioms S1S4.
 .
 .
 .
 For every , , .
 Alternatively, instead of S3 and S4, we could use the induction axiom for every , a wff (in the language of ) in which no variable except occurs free.
 is not finitely axiomatizable.
Clearly,
. Moreover, every model
of
consists of the standard part isomorphic to
and nonstandard part consisting of
chains of the form
If models
and
of
have the same number of
chains, then they are isomorphic.

Uncountable models
and
of
are isomorphic iff they are of the same cardinality.
 Therefore, is categorical in every uncountable cardinality.
 is complete (Łoś–Vaught test).
 (Exercise 2 of Section 2.6).
 is decidable (axiomatizable and complete).
Elimination of Quantifiers
A theory
admits elimination of quantifiers iff for every wff
there is a quantifierfree wff
such that
.
 In fact, to show that admits elimination of quantifiers, it is enough to show that admits elimination of quantifiers for every wff of the form where is atomic or the negation of an atomic formula.
admits elimination of quantifiers.
 The completeness of follows from the elimination of quantifiers property as well. Indeed, each atomic formula of a sentence is of the form which is either deducible or refutable from the axioms, and so is the quantifierfree sentence logically equivalent to a given sentence.

Any relation definable in
is also definable by a quantifierfree formula.
 A subset of is definable in iff either it is finite or its complement is finite.
 The relation is not definable in .
 Another example of a theory that admits elimination of quantifiers is .