31
$\begingroup$

Why are there seemingly so many who want to use ETCS, or HoTT, or similar as a foundation of mathematics? I'm aware that HoTT has a good few good aspects, but that doesn't entirely explain the strong desire to find something other than ZFC to use, so I ask:

What is actually wrong with ZFC that drives this desire?

I've heard a few arguments already, though they were a bit vague - I'll list them below.

  1. As all the objects of ZFC are sets, in ZFC questions such as "is $\pi \in 3$" may be asked, and for some reason just the fact that that may be asked is a problem...but I can't really see the issue. You never need to ask those questions so where would they cause a problem?

  2. Another argument is that ZFC has too much "baggage" caused by the cumulative hierarchy - we don't want to have to worry about the set theoretical aspects of the elements of the real numbers, for example. This, again, is lost on me - can anyone give an example of where we ever actually feel the need to say anything at all about such aspects? Surely once you've got your definitions and you have a few properties that you want you can proceed to deduce using only those properties and may safely ignore those you don't want to think about?

You'll never get a false theorem from ignoring an axiom - when one proves something about groups in general it does not matter what extraneous properties individual groups have, they follow the group axioms so the conclusion is valid. Similarly we know what properties we want the real numbers to have, so surely we can deduce from those without any real issue once we have an object with those (though possibly other) properties?

  1. The last apparent issue I'll mention is categories. Apparently ZFC (let's assume with Universes) is a headache for category theorists. Something about ZFC makes category theory harder than it would be in, say, homotopy type theoretic foundations. So far all I've seen is hand waving - can anyone give an example of where ZFC(+U) truly makes life so much more difficult for category theorists? What is the problem?

I know that this is a negative post, asking what is wrong with ZFC rather than what is right about HoTT, ETCS, etc, it's just that I've seen many vague references from those disgruntled with the set theory, but not yet any concrete grievances.

As with many of my unusual questions, the tags are guesswork.

$\endgroup$
22
  • 2
    $\begingroup$ One might complain that questions like "Is $3 \subseteq \pi$?" are problematic because some ZFCers will answer yes (e.g. fans of Dedekind cuts) while other ZFCers will answer no (e.g. fans of Cauchy sequences.) But I agree that it's no big deal. As you observed, nobody's interested in theorems about Dedekind cuts or Cauchy sequences. People are interested in theorems about complete ordered fields. $\endgroup$ Sep 7, 2015 at 9:23
  • 2
    $\begingroup$ I sort of feel that I kinda answered that already. $\endgroup$
    – Asaf Karagila
    Sep 7, 2015 at 11:21
  • 1
    $\begingroup$ @Miha: Those people don't understand the point of a foundational theory, then. I wonder how they feel when they think about how all the data types in their code, all the different objects... are just bitfields in the RAM/pagefile. Do they plan on shunning away computers too for this reason? :-) Or the fact that you can inject asm snippets to directly manipulate whatever data type you want as bitfields... Those damn bitfields! $\endgroup$
    – Asaf Karagila
    Sep 7, 2015 at 13:19
  • 2
    $\begingroup$ @SixWingedSeraph: I don't even recall it was set theory that was used to show that real numbers are Dedekind cuts, or equivalence classes of Cauchy sequences, both the constructions came before set theory existed. I do recall that it was part of the need to show why there is such an object to begin with. ZFC has absolutely nothing to do with your complaint. You're pointing it at the wrong issue here. Not to mention, that unlike ETCS, ZFC is interpretation agnostic. So once you've shown there is a model for the real numbers, nobody cares which sets you've used anymore. $\endgroup$
    – Asaf Karagila
    Sep 8, 2015 at 0:08
  • 2
    $\begingroup$ It's not a philosophical difference between two people as much as it is between two theories. In ZFC it makes sense for an "ordered pair" to be simply something whose equality is detected by equality of its components (or whatever your definition is); but in ETCS it does not, because there is no relevant "global equality" to even phrase such a definition with. You can only phrase it inside a model of Z that you build inside ETCS, and the result is not a "native" definition to ETCS, only something that you've coded inside of it. $\endgroup$ Sep 11, 2015 at 15:50

1 Answer 1

27
$\begingroup$

As many of the commenters have said, nothing is "wrong" with ZFC at a practical level; it's just that other theories have certain advantages. I'm not sure what you're referring to by "the strong desire to find something other than ZFC to use" — for the most part I've only seen people pointing out advantages of particular other theories rather than complaining that ZFC is broken on its own.

The first two disadvantages you point out are, as you say, not of practical importance for using ZFC as a foundation for mathematics. But they are not worthless observations either. If nothing else, they are important philosophical observations that there are ways in which ZFC doesn't match the everyday practice of mathematicians, so it ought to be of philosophical interest that there are other foundations that do match it better.

There is also a pedagogical point to make: the working mathematician may have no trouble ignoring an axiom, but a student just learning mathematics may get the wrong impression about how sets are actually used in mathematics from a ZFC-oriented introduction. (Indeed, pedagogical considerations were what first let Lawvere to invent ETCS.)

And there is also a question of extensibility: as we try to interpret a foundational theory in "nonstandard" models (I put the word in quotes because it has an undesired negative connotation), it is significantly easier if we use a foundational theory that looks more like the models that we are interested in as they arise naturally — namely, as categories, not as cumulative hierarchies. One can, with some effort, build a cumulative hierarchy from a category, but it doesn't always capture exactly what one wants, and why force oneself to go through the pain when there are other perfectly good foundational theories that we could use instead of ZFC?

As for category theory, there are at least two reasons a category theorist might be dissatisfied with set theory. One is the awkward treatment of universes used to deal with "large categories", but the alternative foundations that you mentioned (ETCS, HoTT) don't really do anything to solve that problem. (There are other alternative foundations, such as those proposed by Feferman, which do attempt to address that question, but I don't know as much about them.)

Another issue with set theory for category theory is that any two objects in set theory can be equal, whereas in category theory we generally only want to consider objects up to isomorphism, or categories up to equivalence, and so on into higher dimensions. You might think this is just like the question of nonsense statements $3\in \pi$, since you can just ignore the notion of equality and use isomorphism. However, technically you then incur an obligation to prove that all theorems and constructions respect isomorphism (or equivalence). Nobody actually does this in everyday mathematics, it being regarded as obvious; but when you start formalizing mathematics in a computer, it becomes necessary and tedious. ETCS and HoTT do have some advantages here: in ETCS formulated appropriately, one can prove a metatheorem that everything transports across isomorphism; whereas in HoTT this transportability is part of the basic theory (the univalence axiom).

To be fair, I should note that ZFC itself has some advantages over other foundational theories. In particular, it is very well-adapted for what the mathematicians who call themselves "set theorists" use it for, namely the study of well-founded relations. Most of the results of modern set theory could be formulated and proven in alternative foundations, but they often become significantly more awkward.

$\endgroup$
17
  • 1
    $\begingroup$ I should add to your final remark that set theorists study structure of models of set theory, but a lot of it reflects back down to the real numbers and their subsets. So these results are ultimately not isolated from the rest of mathematics. $\endgroup$
    – Asaf Karagila
    Sep 8, 2015 at 16:29
  • $\begingroup$ Thank you, that certainly clears up most of my confusion over this. Out of interest, has any work been done on the ability of isomorphisms to transfer theorems (couldn't think up a better term) between sets of ZFC? It can't quite work the same as equality, of course, but there must be some translation that occurs? Maybe for objects $A$, $B$, with $f: A\to B$ an isomorphism allows $\Phi (x) \Leftrightarrow \Phi (f(x))$ for $x\in A$ and logical formulae $\Phi$? I highly doubt it would be anywhere near that simple, I'm almost certain that it isn't as universal, but has anything been shown? $\endgroup$
    – Nethesis
    Sep 8, 2015 at 16:58
  • $\begingroup$ @Nethesis: It is in fact almost trivial just by the definition of Tarskian truth (induction, induction, induction). Even in $\sf ZFC$. It's true that usually we don't check that and we don't care about that very much. $\endgroup$
    – Asaf Karagila
    Sep 8, 2015 at 17:22
  • $\begingroup$ @AsafKaragila Can you direct me to some source for this so I know exactly how it is stated? Or a least a pointer about what to search for? I'm curious about this $\endgroup$
    – Nethesis
    Sep 8, 2015 at 19:26
  • 1
    $\begingroup$ @Nethesis No, SEAR is not subsumed by HoTT, any more than ETCS or ZFC is; they are different systems. I have been spending more of my time on HoTT recently, but of course SEAR still exists. $\endgroup$ Nov 16, 2015 at 20:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .