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 , if is injective, then is surjective.

Very rough proof sketch: The field has characteristic 0, so each of the axioms (where is a prime) is true in . 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 . But a proof can only use finitely many axioms. Therefore, there must be some 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 to , where is a finite field of characteristic . But this is impossible, because is a finite set.

More details below.

Fix a language . The set of axioms ACF for algebraically closed fields consists of the field axioms (, etc.) together with, for each an axiom

asserting that all monic polynomials of degree have a root.

If is a prime, then let ACF_{p} be the axioms of ACF together with the axiom

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

*Lemma*. All of the theories ACF_{p }and ACF_{0 }are *complete*, i.e., for any first-order sentence in the language of , either the theory proves or the theory proves .

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

First we show that ACF_{p }proves each . First observe that is true in each finite field of characteristic just by virtue of it being a finite set. Since the algebraic closure of (the field with elements) is a union of finite fields of characteristic , 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 large enough to contain all the coefficients of the polynomial and to witness its non-surjectivity in order to get a contradiction. Since ACF_{p }is complete and there is an algebraically closed field of characteristic in which is true, it follows that ACF_{p }proves .

Now, assume that some wasn’t true in . Then ACF_{0 }would prove . But the proof would have to use only finitely many axioms . If is a prime greater than each such that is used in the proof, then ACF_{p0 }proves , contrary to the result of the above paragraph.

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

I linked to your proof. One of my favorite theorems/proofs. So cool that such a simple idea can be made to work.

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).