The discussion centers on the search for a first-order axiomatization of Zermelo-Fraenkel set theory with the Axiom of Choice (ZFC). Participants note that ZFC is typically expressed in higher-order logics, while first-order formulations exist and can be found in top search results, including Wikipedia. The first-order version requires an infinite number of axioms, as it utilizes axiom schemas to define sets based on unary predicates. In contrast, first-order Neumann-Bernays-Gödel (NBG) set theory is mentioned as an equivalent theory that only requires finitely many axioms. The conversation emphasizes the distinction between first-order and higher-order formulations of set theory.
