[cruegge]

That's a good intuition for first order PA, where the completeness theorem holds, but not the full story either. PA in second order logic only has a single model, but is still incomplete: there are statements that are true in the only model, but not provable.

[bedman12345]

Yeah but second order logic itself is incomplete. ZFC doesn't have a single model, too, btw. In the end unprovable sentences exist because there are multiple models satisfying your axioms.

[cruegge]

What I meant to say is that multiple models are not the only reason for something to be true but unprovable, the incompleteness theorem also holds in more general conditions.

Concerning multiple models of ZFC: I'm always confused by such statements about the foundations of set theory itself, they seem weirdly self-referential. ZFC certainly can't prove that it has multiple (or even any) models. Does such a statement need additional axioms, or is there a general theorem like "If a first order theory has any model, then it has multiple ones."?