Ax’s Theorem: An Application of Logic to Ordinary Mathematics

There are a number of applications of logic to ordinary mathematics, with the most coming from (I believe) model theory. One of the easiest and most striking that I know is called Ax’s Theorem.

Ax’s Theorem: For all polynomial functions f\colon \mathbb{C}^n\to \mathbb{C}^n, if f is injective, then f is surjective.

Very rough proof sketch: The field \mathbb{C} has characteristic 0, so each of the axioms \psi_p \equiv \overbrace{1 + 1 + \cdots + 1}^{p\text{ 1's}}  \ne 0 (where p is a prime) is true in \mathbb{C}. Suppose that some polynomial is injective but not surjective. Then there is a proof of that fact from the axioms of algebraically closed fields, together with the axioms \psi_p. But a proof can only use finitely many axioms. Therefore, there must be some \psi_p that is not used in the proof. One can then show that there would be a polynomial function which is injective but not surjective from F^n to F^n, where F is a finite field of characteristic p. But this is impossible, because F is a finite set.

More details below.

Fix a language \mathcal{L} = \{+,-,\times, 0,1\}. The set of axioms ACF for algebraically closed fields consists of the field axioms (\forall x\, (x \ne 0 \implies \exists y\, x\times y = 1), etc.) together with, for each d \geq 1 an axiom

\forall c_0 \cdots \forall c_{d-1} \exists x\, x^d + c_{d-1}x^{d-1} + \cdots + c_0 = 0

asserting that all monic polynomials of degree d have a root.

If p > 0 is a prime, then let ACFp be the axioms of ACF together with the axiom

\overbrace{1 + 1 + \cdots + 1}^{p\text{ 1's}} = 0

asserting that the field has characteristic p. Call that axiom \psi_p. Let ACF0 be the set of axioms of ACF together with \neg \psi_p for each p. (This asserts that the field has characteristic 0). We now have the following lemma, provable by (essentially) logical means.

Lemma. All of the theories ACFp and ACF0 are complete, i.e., for any first-order sentence \phi in the language of \mathcal{L}, either the theory proves \phi or the theory proves \neg\phi. \square

Proof of Ax’s Theorem. For each d and n, let \phi_{d,n} be a formula asserting that all n-tuples of polynomials of degree d in n variables which are injective are surjective.

First we show that ACFp proves each \phi_{d,n}. First observe that \phi_{d,n} is true in each finite field of characteristic p just by virtue of it being a finite set. Since the algebraic closure of F_p (the field with p elements) is a union of finite fields of characteristic p, it is true in that field as well: if there is some injective and non-surjective polynomial function, simply pick a finite field of characteristic p large enough to contain all the coefficients of the polynomial and to witness its non-surjectivity in order to get a contradiction. Since ACFp is complete and there is an algebraically closed field of characteristic p in which \phi_{d,n} is true, it follows that ACFp proves \phi_{d,n}.

Now, assume that some \phi_{d,n} wasn’t true in \mathbb{C}. Then ACF0 would prove \neg \phi_{d,n}. But the proof would have to use only finitely many axioms \psi_p. If p_0 is a prime greater than each p such that \psi_p is used in the proof, then ACFp0 proves \neg \phi_{d,n}, contrary to the result of the above paragraph. \square

For more information, see David Marker’s introductory notes on model theory here.

4 thoughts on “Ax’s Theorem: An Application of Logic to Ordinary Mathematics

  1. This is a very nice theorem. One thing that I’ve been wondering about in this context is whether there are any examples of injective polynomials f that aren’t surjective.

    Incidentally, one way to think of this theorem is as a generalization of the fundamental theorem of algebra since in the single variable case all polynomials are surjective. Similarly, one gets from Picard’s theorem that all injective analytic functions are surjective (consider f composed with itself).

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s