After thinking about it more, the currently prevalent approach to and interpretation of axiomatic set theory seem questionable to me. Of course, the strict logic of the results is not in dispute, but it seems we should be able to assume axioms like ZFC implicitly (as most mathematicians in practice do anyway) and move on. There are a number of reasons to do this, which we will discuss now.
First, the question of a result’s dependence on a certain axiomatic set theory axiom, like the Axiom of Choice, is not as consequential as it is often presented to be. The axioms that have been controversial are those with unintuitive consequences, even when the axioms themselves seem reasonable, but rather than framing those consequences as dependent on choice of axiom, we should understand them as exposing unintuitive but “real” truths about reality. (Technically, this is implicitly assuming Platonism.) For example, the Banach-Tarski paradox is not something we can just “turn off” by rejecting the Axiom of Choice; instead, it results from using non-measurable sets in the process of deriving something about measure. In general, we should expect that if a process’s steps don’t explicitly preserve an invariant, then that invariant may not hold in the end, though the application of this to that particular scenario is hard to grasp at first.
Second, we should be able to perform the rest of math without ever really mentioning axiomatic set theory anyway, by simply reworking our language to avoid such issues. In this way, we can avoid follow-up topics like classes and Grothendieck universes, which stem from an “unenlightening syntax issue” rather than offering additional “meaningful semantic insight.” For example, instead of talking about the class of all sets satisfying a property P, take an arbitrary “universal working” set U and talk about all the subsets of U satisfying P, or talk about P itself and mention particular sets satisfying P without mentioning the whole class of such sets (for example, in universal algebra, it seems we can avoid talking about equational classes by just focusing on equational theories.) And we don’t need to mention the “larger collection” that all these sets and sets derived from them (e.g. via the power set operation) are in (aka the Grothendieck universe), just as we don’t need to mention the collection of all sets but can still pick out and work with any set in that collection (like we do in abstract algebra and other abstract math subjects: “let S be any set satisfying these axioms …”) To generalize that last point, for any proper class we can talk about as many individual members of that class as we please, without mentioning the full collection of all those members. In this way, we should be able to avoid axiomatic set theory-derived language in all further math without missing anything semantics-wise.
Concerning axiomatic set theory’s ability to formalize the mathematical universe, as I mentioned in my article on separating mathematical logic and set theory, no axiomatic theory can capture all the properties of a type of mathematical object like the integers. The most it can achieve is completeness in a particular logic, which fundamentally doesn’t correspond to the full theory of a concept. But it further happens to be the case that because of Godel’s incompleteness theorem, any “practical” system, including all currently prominent axiomatic set theories, must be incomplete. (“Practical” here corresponds to a particular formalization, which may or may not fully capture an intuitive intended meaning. Nevertheless, the point stands.)
Also, encoding in terms of sets is not the only way to encode mathematics. For example, we can encode mathematical language and thus mathematical information (expressed via language) via bits or numbers, as we do all strings. Sets are not really more “privileged” then than these other encoding schemes.
Finally, if we hold that the “domain of all sets” is a “real thing” (again implicitly assuming Platonism), then statements like the Continuum Hypothesis must have a truth value — we just don’t know the answer yet. Over-emphasizing ZFC or another system as being the “complete list” of axioms hinders progress in coming up with proofs of statements like these that can involve “rigorous informal reasoning” (which I consider to still be rigorous, see my post on the definition of mathematical rigor), which together with formal arguments form the practice of math, not one without the other. This is true more generally: an over-reliance on motivating a particular concept as an intended-to-be-complete formalization of a particular intuition misses a more accommodating approach of making the intuitive idea the “primitive” and then treating various formalizations of its properties as just different avenues to glean information about it. This is more historically accurate (as definitions have evolved over time), as Richard Hamming discussed, and opens up the possibility of different formalizations down the road that can yield additional insights.
From a perspective of how to reconcile this point with formal proof checking software (such as Lean), which we would like to serve as a basis for automated verification of math in the future, we have always had a history in software engineering of modifying interfaces when user preferences / intended feature sets change (see my article on the non-mathematical aspects of real-world systems), and we can always do so here as well when we come up with new axioms that we prove outside of formal logic, but that can then be great tools for further formal proofs on top of them.
To summarize, the main aspects of current approaches to axiomatic set theory that seem “not semantically valuable” to me are: (1) over-emphasizing its importance, (2) introducing notions like classes and Grothendieck universes that arise only from syntactic error resolution in unenlightening ways, and (3) treating set theory axiom lists as “full.” We can avoid these points in treatments of math by simply showcasing Russell’s paradox (and its variants), showing methods for avoiding such issues, mentioning “reasonable” and “intuitively clear” axioms like ZFC, taking these axioms as self-evident, and moving on. I hold that if we do this, we can elucidate math better for both researchers and students, helping accelerate progress further.
Written February 2026, edited April 2026 for clarity.
—
Edit (March 2026): After thinking more about my points on model-theoretic results on axiomatic set theories, I have some further questions in that area too. Note that I’m not familiar with all the details of the proofs of these results, so my thinking could be wrong here.
As far as I understand, the proof of a statement like “Choice is independent of ZF” relies on set-sized models of ZF, and in fact has been established only for set-sized models. But it is then unclear how applicable such a result is to the standard model of ZF (ordinary sets), as it is unclear whether a collection of sets satisfying ZF with the standard interpretation of could be set-sized. Indeed, this is equivalent to the question of existence of a Grothendieck universe, which is tricky (as the Wikipedia article elaborates.) Of course, the question of independence is moot for a specific model — any specific statement is either true or not true in the model — which traces back to my point above that over-emphasizing independence hinders progress in determining the truth value of statements for specific models. But independence established model-theoretically is often interpreted in a proof-theoretic way: I can’t use these axioms to decide this statement, so additional properties of my specific model are needed to decide it. But how accurate is this really when applied to ordinary sets, when the independence result, dealing with any possible interpretation of
and a set-sized model, is effectively about a kind of system that we don’t even know sets form?
Instead, more proof-theoretic arguments that don’t point to set-sized models (just don’t mention the whole collection that the axioms take as domain) would be preferable in truly helping us understand how we can get closer to a resolution of a statement like the Continuum Hypothesis, helping elucidate which proof paths would definitely not work so we could eliminate them.
