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 ACFp be the axioms of ACF together with the axiom
asserting that the field has characteristic . Call that axiom . Let ACF0 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 ACFp and ACF0 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 ACFp 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 ACFp is complete and there is an algebraically closed field of characteristic in which is true, it follows that ACFp proves .
Now, assume that some wasn’t true in . Then ACF0 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 ACFp0 proves , contrary to the result of the above paragraph.
For more information, see David Marker’s introductory notes on model theory here.
Like this:
Like Loading...
Related
XOR's Hammer 
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).