ZFC — Zermelo-Fraenkel set theory with the Axiom of Choice — is a collection of nine basic axioms about what sets are and how they behave, from which essentially all of modern mathematics can, at least in principle, be rigorously built up. Developed between 1908 and 1922 in response to a genuine crisis (paradoxes discovered in earlier, naive attempts to define sets), ZFC remains the standard, near-universally accepted foundation of mathematics used today.
Every mathematical object you've ever encountered — numbers, functions, shapes, equations — can, remarkably, be built entirely out of sets (see the Set entry): simple collections of things. But what exactly is a set allowed to be? What operations are you allowed to perform on sets? Answering these seemingly basic questions with full precision turns out to require a carefully chosen list of foundational rules — the ZFC axioms — which quietly underlie essentially every other branch of mathematics, whether or not the mathematicians working in those branches ever think about them directly.
The discovery of paradoxes like Russell's threatened to undermine confidence in the entire logical foundation of mathematics at the turn of the 20th century. Ernst Zermelo's original 1908 axioms, later refined and extended by Abraham Fraenkel (1922) and others, restored that confidence by providing a precise, carefully restricted set of rules — sufficiently permissive to reconstruct all of ordinary mathematics, yet sufficiently restrictive to avoid the known paradoxes.
Whenever you write down a mathematical proof about numbers, functions, or geometric objects, that proof can — in principle, though almost never in explicit practice — be translated all the way down into a sequence of purely logical steps built directly from the ZFC axioms alone. Working mathematicians essentially never do this translation explicitly (it would be extraordinarily tedious for even simple results), but knowing that it's possible in principle provides the deep logical bedrock underlying confidence in mathematics as a whole.
The other eight axioms are widely considered self-evidently reasonable by essentially all working mathematicians. The Axiom of Choice, by contrast, has historically been more controversial: it guarantees that a certain kind of selection is possible, without providing any explicit rule or method for actually making the selection — an existence claim without a corresponding constructive recipe. It leads to some famously counterintuitive consequences (most notably the Banach-Tarski Paradox, where a solid ball can be decomposed and reassembled into two balls identical to the original), yet it's also indispensable for proving many important, widely-used mathematical results elsewhere. Zermelo-Fraenkel set theory without Choice is called simply "ZF"; adding Choice gives "ZFC" — the standard, near-universally adopted default in modern mathematics.
Gödel's Second Incompleteness Theorem (see the Gödel's Incompleteness Theorems entry) proves that ZFC — assuming it actually is consistent (free of internal contradiction) — cannot prove its own consistency using only its own internal resources. This means mathematicians' confidence that ZFC is genuinely free of hidden contradictions ultimately rests on extensive practical experience (no contradiction has ever been found despite over a century of intensive use) and on carefully reasoned philosophical judgment, rather than on any absolute, fully self-contained mathematical proof of consistency.
As detailed in the Continuum Hypothesis entry, certain precisely stated mathematical questions (like the Continuum Hypothesis itself) are formally independent of ZFC — neither provable nor disprovable from these nine axioms alone. This was established through Kurt Gödel's 1940 consistency proof and Paul Cohen's 1963 independence proof (using his powerful forcing technique), together demonstrating that ZFC, despite its remarkable overall success, does not settle literally every mathematically meaningful question a mathematician might reasonably wish to ask.
ZFC is not the only foundational system ever proposed, though it remains overwhelmingly the standard default. Alternatives and extensions include Von Neumann–Bernays–Gödel (NBG) set theory (which handles certain very large, "proper class" collections slightly differently, while proving exactly the same theorems as ZFC about ordinary sets), various large cardinal axioms (additional axioms postulating the existence of certain extremely large infinite sets with special properties, actively researched as potential candidates for resolving some independence results), and entirely different foundational approaches such as type theory and category theory (see the Homomorphism & Isomorphism entry for a glimpse of the category-theoretic perspective), which some mathematicians and computer scientists argue provide more natural foundations for certain specific purposes, particularly in areas connecting closely to computer science and formal verification.
Modern formal proof assistants (such as Lean, Coq, and Isabelle — see the Kepler Conjecture and Four Colour Theorem entries for examples of their real-world use in verifying major theorems) typically implement some variant of set theory or type theory closely related to, or directly built upon, ZFC's foundational ideas, allowing entire complex mathematical proofs to be checked by computer down to the most basic logical steps — a modern, practical realisation of the once purely theoretical 20th-century dream of grounding all of mathematics in a single, fully explicit, mechanically checkable foundational system.