How is first-order logic a strong enough logic for the foundations of mathematics?

A bit of background: I'm currently taking a logic class whose ultimate goal is to show soundness, completeness, and undecidability of FOL, and which is following this Sets, Logic, Computation book. I've also started to take a look at the next book in the series, Incompleteness and Computability, which starts out by defining theories as closed sets of sentences in a language, treating only the logical framework of FOL.


I've often heard that most of mathematics can use ZFC set theory as a foundation. With ZFC being a set theory in first-order logic, I presume this means that mathematical statements can be written in the language of ZFC and derived from its axioms. However, intuitively I would think that there are mathematical theorems whose statements can only be stated in second-order logic (I can't think of any examples, and some that I've found seem to confuse second-order quantification with quantifying over sets of sets). So how would ZFC be able to even express such statements, being first-order?

I've also heard that ZFC set theory is "stronger" than second-order logic (in this answer, for instance). First of all, how could a theory in first-order logic be stronger than second-order logic if second-order logic is more expressive? And second of all, how is it even possible to compare a theory (a closed set of sentences in some language) to a logic (a framework for languages with canonical semantics for its logical symbols) especially when a logic encompasses many languages, each of which can admit many theories?


The point is that using ZFC we can interpret1 second-order logic. ZFC gives us a way to understand the notion of sets and relations which are necessary for second-order logic.

We can prove, as a first-order statement in the language of ZFC, that there is a unique Dedekind-complete ordered field (up to isomorphism). This is a second-order statement about the real numbers, yes, but we can interpret that in ZFC, which transforms it into a first-order logic statement in the language of set theory.


1. In the non-technical sense.