Proving theorems about ZFC by proving them for an arbitrary model.

Question

To prove that a statement follows from the group axioms, we typically write:

Let $G$ denote an arbitrary group... Then... Thus, it s a theorem of the group axioms that...

Presumably, this form of argument should be equally useful in set theory. So to prove that a statement follows from ZFC, it would be useful to be able to write:

Let $Z$ denote an arbitrary model of ZFC. Then... Thus, it s a theorem of ZFC that...

What is the appropriate definition of "model of ZFC" such that this kind of reasoning works?

Answer 1

It is the same definition of a model in any other theory.

This is a set which encodes a structure which interprets the language of set theory, in which the axioms of ZFC are true. In this case this means a pair $\langle M,E\rangle$ such that $E$ is a binary relation and $M$ is non-empty, and the axioms of ZFC are true in this structure.

Answer 2

Of course the result holds as you stated, by the completeness theorem (taking as model any structure $(M,E)$ that satisfies the ZFC axioms).

That being said, I am not sure that we actually use this result in full generality in practice. However, what is common is to argue about transitive set models (of enough set theory), and then conclude that the result indeed holds, due to the reflection principle. This approach admits quite a few wrinkles, and it is a powerful technique in infinitary combinatorics and set theoretic topology.