Must all models of ZFC (in a standard formulation) be at least countable?

[mpitluk]

Must all models of ZFC (in a standard formulation) be at least countable?

Why I think this: there are countably many instances of Replacement, and so, if a model is to satisfy Replacement, it must have at least countably many satisfactions of it.

Does my question only apply to first-order formulations of ZFC, or are there second-order formulations of ZFC that can be finite?

Thanks.

 

[AKG]

Yes, they're all at least countable, because they all have an empty set, a set containing just the empty set, a set containing just the set containing just the empty set, etc. Your argument using Replacement doesn't work, since there's no guarantee that two different instances of Replacement generate different sets.