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.