How is second-order ZFC defined?

I know the first-order version of ZFC, but not second-order ZFC. Can anyone explain how axioms (and other things) of second-order ZFC differ from the first-order version?

Solution 1:

Second-order logic allows us to quantify over subcollections of the universe. This allows us to write things like "For every class which contains all the ordinals ..." within the theory, whereas in first-order logic these sort of sentences are actually schema of sentences (where class becomes a definable class).

It is important to point out that there are two [common] ways to interpret second-order logic, the first is with Henkin semantics where the classes are allowed to be definable classes only; this results in something resembling first-order logic. The second way is to full semantics which allows the classes to be any collection.

In second-order ZFC instead of the replacement schema we have one axiom which says that every function whose domain is a set then its range is a set.

For example we don't have countable models of second-order ZFC when interpreted in full-semantics, because those "hide" a very [first-order] undefinable bijection between $\omega$ and their universe. Second-order replacement can see this bijection, so the model cannot satisfy replacement (The range of a function whose domain is a set is everything).