Zermelo–Fraenkel set theory is the usual first-order axiomatization of sets by extensionality, empty set, pairing, union, power set, infinity, separation, replacement and foundation.
ZFC is Zermelo–Fraenkel set theory together with the axiom of choice.
Articles by others on the same topic
One of the first formal proof systems. This is actually understandable!
This is Ciro Santilli-2020 definition of the foundation of mathematics (and the only one he had any patience to study at all).
TODO what are its limitations? Why were other systems created?