Quantifier elimination — theory of successor

Every assertion about the structure ⟨ℕ,S,0⟩ of the natural-number successor is trivial, being equivalent to a quantifier-free assertion in this language.

Recall from our earlier post that a theory admits quantifier-elimination when every assertion is logically equivalent over the theory to a quantifier-free assertion, a Boolean combination of atomic assertions.

We had said that this is quite a remarkable property when it occurs, because it reveals a severe limitation on the range of concepts that can be expressed in the theory—a quantifier-free assertion, after all, is able to express only combinations of the immediate atomic facts at hand. We are therefore generally able to prove quantifier-elimination results for a theory only when we already have a profound understanding of the theory and its models.

In this post, let us prove the quantifier elimination result for the theory of the successor operation in the natural numbers.

Enjoy this installment from A Panorama of Logic, an introduction to topics in logic for philosophers, mathematicians, and computer scientists. Fresh content each week.

Please consider subscribing as a free or paid subscriber.

Theory of successor

Consider the first-order theory of a successor function, as realized for example in the Dedekind model, ⟨ℕ,S,0⟩, where S is the successor operation Sn = n + 1.

The theory has the following axioms:

1. Zero is not a successor.

   \(∀x (Sx ≠ 0)\)

2. The successor function is one-to-one.

   \(∀x,y (Sx = Sy → x = y)\)

3. Every number is either zero or a successor.

   \(∀x (x = 0 ∨ ∃y (x = Sy))\)

4. There are no cycles in the successor operation.

   \(\begin{align} &∀x (x ≠ Sx)\\[2ex] &∀x (x ≠ SSx)\\[2ex] &∀x (x ≠ SSSx)\\[2ex] &\qquad\vdots \end{align} \)

The third axiom is also sometimes known as the very weak induction principle, for it expresses an elementary consequence of induction in the classical theory of Dedekind arithmetic. Namely, by induction every natural number is either 0 or a successor, since this property is had by 0 and is passed from every number to its successor. The no-cycles axiom continues with all axioms of the form ∀x (x ≠ Sⁿx) for each metatheoretic natural number n > 0.

In the Dedekind model ⟨ℕ,S,0⟩, every individual is definable, since x = n just in case x = SS···S0, where we have n iterative applications of S. So this is a pointwise definable model, and hence also Leibnizian. Note the interplay between the n of the object theory and n of the metatheory in the claim that every individual is definable.

What definable subsets of the Dedekind model can we think of? Of course, we can define any particular finite set, since the numbers are definable as individuals. For example, we can define the set {1, 5, 8 } by saying, “either x has the defining property of 1 or it has the defining property of 5 or it has the defining property of 8.” Thus any finite set is definable, and by negating such a formula, we see also that any cofinite set—the complement of a finite set—is definable. Are there any other definable sets? For example, can we define the set of even numbers? How could we prove that we cannot? The Dedekind structure has no automorphisms, since all the individuals are definable, and so we cannot expect to use automorphism to show that the even numbers are not definable as a set. We need a deeper understanding of definability and truth in this structure.

Quantifier-elimination for the theory of successor

Theorem. The theory of a successor function admits elimination of quantifiers—every assertion is equivalent in this theory to a quantifier-free assertion.

It will be a hands-on proof.