An actual first-order formulation of ZFC?

[mpitluk]

Can someone point me to a first-order axiomatization of ZFC?

As I've mostly seen ZFC expressed in higher-order logics.

 

[AKG]

ZFC is a first order theory, where have you been seeing second order formulations? I'm sure every one of the top Google results for "ZFC axioms" will give you a first order formulation. In particular, Wikipedia.

 

[Hurkyl]

Can someone point me to a first-order axiomatization of ZFC?

As I've mostly seen ZFC expressed in higher-order logics.

The higher-order axioms are replaced with axiom schema. e.g. the axiom schema of subsets is collection of statements

{x in A | P(x)} is a set,​

one for every unary predicate P in the language of first-order set theory.First-order ZFC requires infinitely many axioms to specify. First-order NBG, however, is an 'equivalent' set theory in an important sense, but only requires finitely many axioms.