When reading about the foundations of mathematics, one is bound to stumble upon the notion of “the four pillars of the foundations of mathematics”; namely, proof theory, model theory, recursion theory and axiomatic set theory. But what exactly is it about these areas that makes them get this prestigious title? One can argue that these “pillars” have a metamathematical nature, in that they try to describe methods of existing mathematics instead of describing elements of the mathematical realm. Proof theory about the way of proofs, model theory about how we construct new structures and recursion theory deals with questions about which parts of mathematics can be computed. I would argue that the last “pillar”, axiomatic set theory, does not fall into this category of metamathematics.
Granted, yes, set theory is our foundation for all contemporary mathematics except set theory itself, which then seems like it would have to be a part of metamathematics, to avoid circular arguments. However, the mathematical universe that set theory seems to describe has gaps, and lots of them, which manifest themselves as being the ZFC independent theorems; this includes the well-known independence of the generalized continuum hypothesis as well as the axiom of choice, meaning that the challenge for set theorists at this moment is to try to fill out these gaps by finding new axioms that decide the truth of these theorems. However, as Gödel showed, one could continue finding new axioms ad infinitum, without ever reaching a satisfactory stage.
Whenever set theorists decide on a new axiom, this affects every other branch of mathematics, since these theories are themselves based upon the set theoretical foundation. But if one claims that what set theorists are dealing with is metamathematics, what happens when they agree upon a new axiom? Since such an axiom now becomes a part of regular mathematics, the part of set theory which concerns this axiom would then become a part of regular mathematics as well and thus drift away from the metamathematical status. People opposing this view could then argue that set theory in fact is not about the concrete axioms themselves but instead the search for axioms, the axiomatization of mathematics. This would surely defend the fact that set theory would stand as one of the foundational pillars, since it would then seem like this field is responsible for our means to deduce anything at all, providing the starting point.
However, set theory is not the only area in mathematics with this kind of status anymore; type theory and category theory are themselves approaching, if not already arrived, as being alternative foundational axiomatizations of the mathematical enterprise. Where does this leave set theory? Would this then lead to a common pillar for all theories, which have the power to construct such an axiomatization? If we allow this, we would arrive at a new problem: how could we be sure that the universe of sets, types and categories are of the same size? It seems essential to make them seem equal in this foundational aspect. What would happen when/if more of such theories are constructed, all with the power to provide these axioms for mathematics? Should we merely fit all these into the same group of metamathematics (assuming that they in fact do describe the same universe)? It seems like the choice is either this, or dethroning the fourth pillar of the foundations altogether. Either way, it would seem like set theory doesn’t have the status as one of the essential pillars of foundations.
To pursue the idea of removing the fourth pillar, if we acknowledge the idea that the realm of mathematics can be much more vast than that of the universe of sets, we could acknowledge set theory as another one of the ‘regular’ fields, along with category theory and type theory, providing axiomatizations for a part of mathematics – namely the part in which all of contemporary mathematics are included. Theorems not being decidable in ZFC just means that the axiomatization in set theory is not up to date with contemporary research, and that’s what set theorists are trying to fix. Furthermore, category- and type theorists are joining in, supplying their own axioms corresponding to contemporary maths.
A problem then, which could arrive at some point with these several axiomatizations, would be inconsistencies in between the axioms; a theorem being true in one set of axioms and false in another. This would split mathematicians into making a choice of which axioms to follow, which then in turn would contradict the purpose of the axiom systems they didn’t choose, since those now do not describe contemporary research results. It would then seem to be a requirement that these axiomatizations have to be equivalent before the system would work. Even if we choose to make axiomatization the new fourth pillar of the foundations of mathematics, or simply make it a part of regular mathematics, the problem would remain the same: making sure that all axiomatizations of the mathematical enterprise are equivalent.