Author: Nihal Uppugunduri

After thinking about it more, axiomatic set theory’s value is now questionable to me because it is a program that arises from a “compiler error in syntax” (Russell’s paradox) rather than something “truly insightful about intended meaning and semantics.” It also seems that 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. Of course, we would still use the axioms of ZFC whether we label them explicitly or not, but we can avoid follow-up topics like classes and Grothendieck universes, which to me stem from this “unenlightening syntax issue” rather than offering “meaningful insight,” with tactics like: 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. To my knowledge, we can do all this without missing any parts of math semantics-wise. There are a number of reasons to do this and further question axiomatic set theory’s value, which I’ll discuss now.

First, 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 any more “privileged” then than these other encoding schemes.

Additionally, while technically correct, model-theoretic results on axiomatic set theories like ZFC seem suspect to me with regards to what the original intuitive intention behind the questions were versus what was actually formally proven. As far as I understand (I don’t have deep enough knowledge so I could be wrong here), results like the independence of AC from ZF are proven using set-sized models, which express facts about the logical theory of ZFC independent of the actual meaning of its symbols like in specific cases. While interesting results on their own, from a perspective of applicability to set theory, there is a clear non-set sized model that the question is intended to be asked for, and the result as stated sidesteps this to prove something different. It’s as if someone asked me “has this banana become spoiled?” and I respond with “a fruit’s property of becoming spoiled is technically independent of it being a banana.” While a true statement, the question is clearly talking about a specific banana, not properties of bananas in general. Instead, such results should be treated as “inspired by” set theory, like how abstract metric spaces can be “inspired by” the Euclidean metric, without labeling them as actually part of set theory, which would concern the theory of sets in the specific model corresponding to what we would usually interpret the word “set” to mean. (General metric space results wouldn’t be described as part of real analysis.)

Finally, if we hold that the “domain of all sets” is a “real thing” (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) plus formal arguments, which together 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) introducing notions like classes and Grothendieck universes that arise only from syntactic error resolution in unenlightening ways, (2) mis-labeling or mis-interpreting model-theoretic results, 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 and taking them 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.