51

As someone self-taught in set theory beginning with Donald Monk’s excellent book on MK set theory, $ZFC$ has always seemed like a weak set theory.

Despite this, the majority of professional contemporary mathematicians still seem to view it as a very powerful theory, providing more than is necessary for their work.

Are there any professional mathematicians who seriously doubt the consistency of $ZFC$, and if so, why?

I wrote a few papers this year proposing set theories much stronger than $ZFC$, and as the year draws to a close I’m finding myself taking the consistency of $ZFC$ for granted as a ‘religious belief’. Are there any heretics present?


EDIT: The responses to this question have all been fascinating, and amount to one of the best christmas presents I’ve ever woken up to. Thank all of you, and merry christmas!

Alec Rhea
  • 9,009
  • 2
    Surely this is an opinion-based question. – LSpice Dec 24 '22 at 20:28
  • 4
    I don't believe $\mathsf{ZFC}$ is inconsistent, but I don't assign its inconsistency that low a probability. Put another way, I would be extremely shocked if $\mathsf{ZFC}$ turned out to be inconsistent, but I can definitely imagine it. – Noah Schweber Dec 24 '22 at 20:32
  • 16
    @LSpice Nevertheless, it is a question that is interesting to research mathematicians. – Joel David Hamkins Dec 24 '22 at 20:32
  • 10
    @JoelDavidHamkins Agreed. Also, it’s not technically opinion-based, since it doesn’t ask the opinion of the person who answers, it asks about a fact, concerning the community of mathematicians in the field. – Alessandro Della Corte Dec 24 '22 at 20:35
  • 1
    One might tag it [reference-request], as well – David Roberts Dec 24 '22 at 20:37
  • 1
    @JoelDavidHamkins, re, there are opinion-based questions that are of interest to research mathematicians; that alone does not make them suitable for MO. Of course in the end what makes a question suitable for MO is the vote of the community, but at least the existence of an "opinion-based" close reason suggests that that's a reason to call a question unsuitable. (Of course @‍AlessandroDellaCorte's right that, as asked, the question is not literally opinion-based; but also presumably "yes, such a person exists" is not an interesting answer.) – LSpice Dec 24 '22 at 21:19
  • 45
    @LSpice Personally, I don't care about any rigid rule about what kind of question is suitable for MO, whether opinion based or whatnot. If a question is interesting to serious research mathematicians, then I am supportive. In my view, squabbles about closing questions tend to be harmful to the site—just leave questions open if serious people are engaged with them. – Joel David Hamkins Dec 24 '22 at 21:28
  • 10
    @LSpice Surely it's not an opinion-based question. Whether there exists a professional mathematician who seriously doubts the consistency of ZFC is a factual question. Such a person either exists or doesn't exist. – Timothy Chow Dec 24 '22 at 22:12
  • "I’m finding myself taking the consistency of ZFC for granted as a ‘religious belief’.", As Gödel (in)famously showed, every theory we would want to consider will require some "leap of faith" (Ignoring the ""boring theories""). Calling the belief of Con(ZFC) "religious" means that Con(ZFC) dictates the way we act, for mathematicians this is a weird statement think about, as even if someone believes in a platonic universe of sets that satisfy ZFC it does not prevent them from from exploring the vast amount of incompatible set theories/weaker set theories. – Holo Dec 24 '22 at 22:40
  • 4
    @TimothyChow did you just assumed LEM in this server?? – Holo Dec 24 '22 at 22:44
  • 8
    @Holo No, the set $H$ of humans is bounded by, say, 1 trillion, so LEM is intuitionistically valid for $H$. – Timothy Chow Dec 24 '22 at 23:59
  • 3
    @TimothyChow But over the course of any actual attempt to completely survey $H$, the set $H$ itself will change. I'm not sure boundedness is the main issue here. (OK I'll stop.) – Noah Schweber Dec 25 '22 at 00:06
  • 20
    Surely we can muster enough literary competence to read the question as an allegory for "what are some mathematical reasons for doubting consistency of ZFC"? – Andrej Bauer Dec 25 '22 at 11:15
  • 2
    @AndrejBauer If that were the question, then I'd suggest rewriting it to ask the more objective question, "Who, among professional mathematicians, has publicly doubted the consistency of ZFC, and what reasons, if any, have been given?" – Timothy Chow Dec 25 '22 at 12:48
  • 9
    "Who, among professional mathematicians, secretly discussed the consistency of ZFC, and what cabal are they a member of?" would be even more fun. – Andrej Bauer Dec 25 '22 at 13:38

7 Answers7

43

When I was a graduate student Jack Silver was famous for trying to refute first, the existence of measurable cardinals, and second, the consistency of ZFC. His attempt at refuting measurable cardinals led directly to the theory of ordinal indiscernibles over $L$ and $0^\sharp$, which are now a core part of our understanding of the nature of the constructible universe in the presence of large cardinals. What an amazing and valuable contribution to the subject he had made that way, even though he had never achieved his initial goal of refuting measurable cardinals.

And although I have heard many people speak against Silver's inconsistency research program, my view has always been:

Main observation. We cannot show that Silver's ideas about inconsistency are incoherent.

Because of the incompleteness theorem, we know that even if ZFC is consistent, then it is consistent with ZFC to hold that they are inconsistent. Thus, Silver's world view will be as consistent as his opponent, and there will never be an argument against the view that ZFC is inconsistent that does not beg the question by assuming that this theory is consistent or something stronger.

Meanwhile, of course, many set theorists, including almost every large cardinal set theorist (but not quite all, like Silver), believe not only that ZFC is consistent, but that consistency rides much higher in the large cardinal hierarchy. There is no proof, for the reasons I gave above.

Another part of my view, however, is that it is precisely because we cannot prove that ZFC and large cardinals are consistent that we are interested in them. Namely, Gödel had identified with his theorem the incompleteness phenomenon, and from that we know of the existence of a tower of theories standing transfinitely above any foundational theory we might entertain. We know there is a tower of stronger theories above whatever theory $T$ we might have. One way of constructing such a tower of theories is to form the theories $T+\text{Con}(T)$ and $T+\text{Con}(T+\text{Con}(T))$ and so on.

But how remarkable that the large cardinal theories themselves instantiate the predicted tower of increasing consistency strength. These theories are not formed by some trivial closure under consistency statements, but rather express profound statements of infinite uncountable combinatorics. These axioms thus have independent interest, and yet fulfill the predicted tower of consistency strength.

So we are glad to have found in the large cardinal hierarchy the predicted tower of consistency strength, and it is not worrisome that we cannot prove consistency — rather, this was just the feature that we were seeking.

Disclaimer. Although I heard Silver talk about set theory at length, having taken several of his graduate courses, I never once heard him discuss his inconsistency research program. All my knowledge about it is second-hand, from other senior set theorists whom I have no reason to doubt. I suppose that in light of the extent of opposing views, it might have made some sense or was at least understandable for Silver to keep his research program relatively private. But actually I wish he had given a series of talks about his research program and his views on the matter — that would have been fascinating! (From my current perspective, I chalk this up to the differing cultural norms about the tolerable levels of disagreement in mathematics vs philosophy.)

  • 1
    Do you happen to know why Silver suspected inconsistency? I've not heard anything about the details of his intuition. – Noah Schweber Dec 24 '22 at 20:49
  • 12
    What I heard (and this is all second hand) was that he thought (and I agree with the concern) that we might be making a fundamental logical mistake in the too-often conflation of internal object theory notions with metatheoretic notions. For example, Con(ZFC) uses the object theory notion, but we are thinking about the metatheory. To my way of thinking, this is related to the reluctance of many large cardinal set theorists to take illfounded models seriously, since insisting on well-founded models is exactly to identify the object theory notions with the meta-theoretic notions. – Joel David Hamkins Dec 24 '22 at 20:52
  • @JoelDavidHamkins: If I am not misunderstanding the motivation, I think that this specific concern should lead to an unsound theory, rather than an inconsistent one. (Because the issue at its core seems to be the very formalization of our intuitive notions themselves as objects in the formal theory.) Why taking the extra step and claiming inconsistency? – Burak Dec 24 '22 at 21:55
  • 7
    I don't want to speak for Silver, but I think the view was that this conflation of object theory with metatheory was pervasive, in the separation axiom, in replacement, reflection, and so on, and that we were just making a mistake about it in a way that could cause a contradiction. – Joel David Hamkins Dec 24 '22 at 22:01
  • 11
    Well, this answer certainly makes me glad the question wasn't closed. – Steven Landsburg Dec 25 '22 at 04:50
34

For decades I was not particularly suspicious about the consistency of ZFC but I was rather surprised about how it had become the standard choice when it contained axioms such as Replacement, which seemed to be unused by all mathematicians other than logicians. Relatively recently I learnt how to use interactive theorem provers, and the prover I use uses a dependent type theory as its foundations. My impression of dependent type theory is that it doesn't have any "exotic" axioms, and so it always felt to me to be "much more likely to be consistent" in some sense: it just seemed to have the bare minimum to do mathematics and nothing more. So I was rather surprised to learn later on that Lean's dependent type theory is equiconsistent with "ZFC + for all naturals n, there exists n inaccessible cardinals", a theory manifestly stronger than ZFC; whilst I would imagine most mathematicians are happy to believe that ZFC is consistent, some do express concern about large cardinals. So for me this felt like another version of the "Zorn's lemma is clearly true, but the well-ordering principle is clearly false" (or whatever the saying is) dichotomy: when presented in the right way ZFC can look even more "obviously consistent". In some sense this other viewpoint on ZFC made me a really solid believer in its consistency, because type theory actually models mathematics in a way far more closely aligned to how I mentally model it (e.g. I don't actually believe that $\sqrt{2}$ is a set, and no doubt Gauss/Euler didn't either).

One final comment regarding large cardinals -- people seem to be nervy about them because existence of an inaccessible implies ZFC is consistent, which can't be proved within ZFC by Goedel. However as Jeremy Avigad pointed out to me, if we're doing mathematics in ZFC (as many of us are -- I don't use Lean's higher universes for example) then we are implicitly assuming it's consistent (because otherwise we'd be wasting our time) so why are we fussing about people assuming something we believe anyway?

Kevin Buzzard
  • 40,559
  • 12
  • 2
    Re:the first sentence, In cases you didn't read it already, the paper What do we want a foundation to do? Comparing set-theoretic, category-theoretic, and univalent approaches by Penelope Maddy is a great read about the different values each foundational approach gives to the table – Holo Dec 24 '22 at 23:35
  • 5
    Arguably, Replacement is actually used by mathematicians. Just because it is eliminable in most cases, by reworking the argument using other axioms, doesn't mean it isn't used. – Timothy Chow Dec 25 '22 at 00:03
  • 10
    FWIW, I don't think that the main reason that people are nervy about large cardinals is that they imply that ZFC is consistent per se. Rather, I think it's that people desire a fixed foundation, rather than one that fluidly adjusts up or down as the need arises. The perception is that ZFC is the "standard" choice, so people get nervous if you deviate from the standard. While set theorists might take the attitude that "the nice thing about standards is that there are so many to choose from," the mathematician in the street prefers a house built on a rock to a houseboat. – Timothy Chow Dec 25 '22 at 01:30
  • 2
    A thing to point out is that LEM significantly boost up the strength of type theories, as opposed to the case of first order logic, where Peano arithmetic is about as strong as Heyting arithmetic. – Trebor Dec 25 '22 at 05:23
  • 5
    You very likely have used replacement and more than one universe, you just haven't noticed it. – Andrej Bauer Dec 25 '22 at 11:18
  • 2
    Can you give a hint as to why type theory leads to inaccessible cardinals? I would expect such a thing to require second-order closure requirements on the universe concept (like Zermelo's universes), that they are closed under actual power sets, instead of just satisfying the power set axiom, but this is contrary to your remark about them seeming the "bare minimum and nothing more." I guess closing under types is essentially a second-order process, rather than a first-order requirement? – Joel David Hamkins Dec 25 '22 at 14:01
  • 5
    "if we're doing mathematics in ZFC then we are implicitly assuming it's consistent (because otherwise we'd be wasting our time)" — I don't understand this comment. Proofs are proofs, no matter whether the system is consistent. If we find an inconsistency of ZFC, we try to fix it and check whether our proofs work in the new foundation. After all, Russell's paradox did not invalidate all mathematics before (and it seems to me that very few mathematics were invalidated by that). – Z. M Dec 25 '22 at 14:30
  • 2
    @Z.M If "proofs are proofs" then even if we found an inconsistency in ZFC, why wouldn't we just keep using ZFC even though we know it's inconsistent? If you articulate an answer to this question, then I think you've answered your own question about what Kevin Buzzard meant by his comment. – Timothy Chow Dec 25 '22 at 17:33
  • 2
    @JoelDavidHamkins I think the short answer is that that Lean uses dependent type theory in a way that leads to a contradiction if you formulate it naively, and the way it avoids contradiction is to use universes ($\approx$ inaccessible cardinals). – Timothy Chow Dec 25 '22 at 17:39
  • 2
    @JoelDavidHamkins: Lean’s type theory (and Coq, and some others) assume universes in a form corresponding quite closely to Grothendieck universes/inaccessible cardinals. The motivation for assuming such universes is mostly analogous to the motivation for them in set-based foundations (e.g. to talk about a “category of all small groups” or similar), but one wants them slightly sooner since most versions of dependent type theory have no analogue of set theory’s unbounded quantification — so without universes, a theorem about, say, “all groups” can only be given as a theorem schema. – Peter LeFanu Lumsdaine Dec 25 '22 at 23:06
  • Thanks, Peter and Timothy. It seems that just as there are weaker universe concepts suitable for their uses in category theory, there should be consistency-strength-free universe concepts suitable for dependent type theory. For example, it is equiconsistent with ZFC to have an elementary chain $W_0\prec W_1\prec W_2\prec\cdots$ each a model of every axiom of ZFC and an element of the next model. These would look rather like universes, but without the inaccessible cardinals. – Joel David Hamkins Dec 25 '22 at 23:11
  • @JoelDavidHamkins: I find your comment intriguing. How does it relate to the fact that “HoTT + AC + LEM“ constructs a model of “ZFC + $n$ inaccessibles“, for every (meta-theoretic) $n \in \mathbb{N}$? François G. Dorais has a nice post about universes and inacessibles in HoTT. NB: The constructon of $\mathrm{ZFC} \models V$ employs higher-inductive-inductive types (a very strong form of well-founded induction and recursion). I would expect “vanilla Martin-Löf type theory" with universes to be much tamer. – Andrej Bauer Dec 26 '22 at 10:18
  • I don't really know anything about universes in HoTT or type theory at all, but I am basing my remark mainly on the usage of Zermelo-Grothendieck universes in category theory, which seem eliminable by weakening the second-order closure aspects of the universe concept to first order in the manner I described, and I would have expected a similar phenomenon in HoTT/type-theory. I view this as similar to the move from Zermelo's original second-order set theory (which requires inaccessibility) to first-order ZFC. – Joel David Hamkins Dec 26 '22 at 15:23
  • There is an axiom of replacement in type theory which specifically applies to universes. It is used in Egbert Rijke's textbook on HoTT to construct quotient sets. Replacement also follows from certain higher inductive types such as homotopy pushouts. – Madeleine Birchfield Dec 27 '22 at 18:50
  • @JoelDavidHamkins You could use weaker universe concepts in HoTT. A universe which is closed under identity types, dependent sum types, and natural numbers, but not dependent product types, corresponds to the regular cardinals in set theory. – Madeleine Birchfield Dec 27 '22 at 18:58
  • 2
    My explanation for why dependent type theory uses universes is rather different to @PeterLeFanuLumsdaine's. The way the theory is set up, everything has to have a type. So the type of pi is real, the type of real is Type, and now the type of Type has to be something so they call it Type 1, the type of Type 1 is Type 2 etc etc. You can't let the type of Type be Type or else you can pull off a version of Russell's Paradox. So you're stuck with all these universes from the beginning, even though I don't really want them and never use them in my teaching (or indeed teach them). – Kevin Buzzard Dec 28 '22 at 14:53
  • 1
    @KevinBuzzard: good point — I agree that’s also part of the picture in those systems, but it’s certainly not how dependent type theories have to be, it’s a design choice made in some versions of dependent type theory, including Lean and Coq and book-HoTT, but not in a lot of more economical presentations, especially in the theoretical literature. My impression is it’s a popular choice in implementations mainly because they usually take a more “maximalist” stance, “give users everything they might want”. – Peter LeFanu Lumsdaine Dec 28 '22 at 17:16
  • @PeterLeFanuLumsdaine This is an interesting discussion. It has prompted me to post another question, asking whether Feferman universes could be used to avoid going beyond ZFC, for those who are uneasy about large cardinals. – Timothy Chow Dec 29 '22 at 13:53
26

We have enough experience with ZFC that I think we can say it is consistent with some confidence.

This isn't too surprising --- I don't know if there's a way to say this precisely, but morally speaking consistency is "easy". Any collection of axioms is inconsistent only if the negation of one of them is a provable consequence of the others. Thus for a system to be inconsistent there must be some special interaction between the axioms, and again, I don't know how to say this rigorously, but to me that says consistency is "normal" and inconsistency is "abnormal".

What people who ask this question sometimes miss, though, is that there is a difference between consistency and soundness. ZFC could prove false statements about the natural numbers but still be consistent. I made this argument here. In contrast to consistency, soundness is not generally to be expected; in order for a collection of axioms to be set-theoretically sound, every one of them must be true. If the axioms were chosen randomly this would be highly unlikely. So the question becomes "what grounds do we have for thinking that ZFC is not merely consistent, but also (to keep things simple) arithmetically sound?"

I personally don't think we have strong reasons to think ZFC is arithmetically sound. Although a (purported) philosophical justification was developed later, when Zermelo first presented his axioms his justification was wholly, and explicitly, pragmatic. They weren't chosen because he thought they were "true". Maybe the thing that bothers me the most is that virtually all of normal, mainstream mathematics can be formalized in much weaker, essentially number-theoretic systems that do have a clear philosophical justification. What ZFC adds to this is a raft of set-theoretic pathology. To me, that suggests (but only suggests) that ZFC might not be arithmetically sound.

Nik Weaver
  • 42,041
  • 3
    Could you explain a bit more fully and defend your remarks about Zermelo's introduction of his axioms? My understanding of the history is that Zermelo had presented his proof of the well order theorem in 1904 (that every set is well orderable), but critics wanted further clarification, and so he formulated his axioms in 1907 to identify precisely the set-theoretic principles he was using. I would describe this situation as him basing his argument on set-theoretic principles (including AC) that he found to be true. But perhaps that is what you meant by pragmatic? – Joel David Hamkins Dec 25 '22 at 00:45
  • "At present, however, the very existence of this discipline seems to be threatened by certain contradictions, or "antinomies," that can be derived from its principles --- principles necessarily governing our thinking, it seems --- and to which no entirely satisfactory solution has yet been found. In particular, in view of the "Russell antinomy"... of the set of all sets that do not contain themselves as elements, it no longer seems admissible today to assign to an arbitrary logically definable notion a set, or class, as its extension ..." – Nik Weaver Dec 25 '22 at 01:03
  • "Under these circumstances there is at this point nothing left for us to do but to proceed in the opposite direction and, starting from set theory as it is historically given, to seek out the principles required for establishing the foundations of this mathematical discipline." (Investigations in the foundations of set theory I) – Nik Weaver Dec 25 '22 at 01:03
  • 3
    Regarding the idea that consistency is "easy," I remember that Torkel Franzen once made the colorful claim that "consistency is a piddling condition." I think his point was more or less the same as your point; namely, consistency is a weak condition, and what people are usually interested in is soundness. In fact, maybe even Alec Rhea is interested in belief (or disbelief) in soundness, rather than "mere" consistency. – Timothy Chow Dec 25 '22 at 01:47
  • @NikWeaver Yes, but does this support the claim that he didn't think they were true? I read the first quote as him merely pointing out the falsity of general comprehension, and the second as him saying he is founding a new set theory, which he did quite successfully. Are you saying he had a mainly instrumental view of the axioms? That certainly wasn't his later view (e.g. 1930). – Joel David Hamkins Dec 25 '22 at 01:58
  • 3
    @JoelDavidHamkins Nik Weaver didn't say that Zermelo didn't think his axioms were true. He said, rather, that truth wasn't the reason Zermelo chose those particular axioms. In other words, Zermelo's self-appointed task was not capturing truth per se, but rather capturing the principles required for set theory "as it is historically given." – Timothy Chow Dec 25 '22 at 02:07
  • 1
    Zermelo was identifying the foundational principles of the subject of set theory as it was known. As far as I can tell, this is the same as what someone motivated by truth (whatever that might mean here) would do. – Joel David Hamkins Dec 25 '22 at 02:19
  • 4
    @JoelDavidHamkins that is a reasonable point. My interpretation of the passage I quoted is "we don't have a conceptually satisfying solution to the paradoxes, so we have to just find some axioms that enable us to do set theory the way we have been doing." – Nik Weaver Dec 25 '22 at 02:26
  • I would agree with that interpretation, but I would view it somewhat less perjoratively. I view him as struggling to find out what the right theory is, in light of the failure of general comprehension. – Joel David Hamkins Dec 25 '22 at 02:30
  • 2
    @JoelDavidHamkins I don't disagree. On the "pejorative" aspect, I actually think as a general principle the pragmatic approach is superior to a philosophical search for truth. Because it's so easy to be wrong about philosophy. – Nik Weaver Dec 25 '22 at 02:38
  • 7
    One reason to think ZFC arithmetically sound is the difficulty of articulating an intuitively coherent way for its arithmetic consequences to differ from true arithmetic. –  Dec 25 '22 at 06:23
  • 7
    @MattF. Oddly enough, to me, that's almost a reason for diminished confidence in arithmetical soundness. Most people have trouble wrapping their heads around the possibility that $\mathsf{ZFC}$ is consistent yet $\mathsf{ZFC}\vdash\neg\mathsf{Con}(\mathsf{ZFC})$. That indicates to me that our intuition about the possibility that $\mathsf{ZFC}$ is consistent but arithmetically unsound is so awful that we shouldn't trust our intuition. – Timothy Chow Dec 25 '22 at 16:40
  • @TimothyChow That may also come from people usually not working with consistent axioms that prove their own inconsistency. It may be hard to wrap one's head around the idea that ZFC proves its own inconsistency because it does not. – Michael Greinecker Dec 25 '22 at 19:58
  • 13
    It's worth pointing out, however, that if $\mathsf{ZFC}$ is consistent, then it is in fact arithmetically $\Pi_1$-sound (in that any arithmetical $\Pi_1$ statement it proves is indeed true; because otherwise we could find a numeric counterexample, which would give a contradiction in $\mathsf{ZFC}$). So if you believe it's consistent, then you actually believe that all its consequences that we can actually test are indeed true. – Gro-Tsen Dec 25 '22 at 22:02
  • 1
    @Gro-Tsen I might quibble a bit with your last claim about "consequences that we can actually test." Consistency doesn't imply $\Sigma_1$-soundness, so if $\mathsf{ZFC}$ is "merely" consistent, then it could prove "Turing machine $M$ halts" when $M$ doesn't halt. To me, simulating $M$ is a "test" of a sort, which provides more and more evidence that $\mathsf{ZFC}$ is wrong the longer $M$ runs without showing any signs of halting. (Though I admit that this "test result" is not as definitive as exhibiting a machine that $\mathsf{ZFC}$ says doesn't halt when in fact it does.) – Timothy Chow Dec 31 '22 at 13:55
23

I interpret the question factually: Do there exist professional mathematicians who seriously doubt the consistency of ZFC? The answer is yes. Here are two examples (though sadly, both mathematicians in question passed away not too long ago).

Vladimir Voevodsky has said, regarding the possibility of an inconsistency in first-order Peano arithmetic, that "I'm quite seriously suspecting that such an inconsistency can at some point be found."

Edward Nelson at one point seriously believed that he had proved that primitive recursive arithmetic is inconsistent. Though he acknowledged his error when it was pointed out, he continued to believe that first-order Peano arithmetic was probably inconsistent, and certainly that its consistency was an open question.

Nik Weaver has written a number of essays, such as Mathematical conceptualism, in which he appears to cast doubt on the consistency of ZF. But since he is an active member of MathOverflow, I will not put words in his mouth, but will allow him to state his own opinion on the matter, if he so chooses. (Deleted because Nik Weaver has already responded.)

Timothy Chow
  • 78,129
  • 5
    I like the timeline here. By the time you finished writing your answer, Nik had posted his. – Asaf Karagila Dec 25 '22 at 00:05
  • 2
    This makes me wonder whether there is anyone out there who seriously doubts Con(ZFC) but not Con(PA). – Nik Weaver Dec 25 '22 at 02:41
  • 3
    @NikWeaver I believe it is likely that there are, but I don't know offhand of solid references to back up that belief. For example, on the Foundations of Mathematics mailing list, Martin Davis once said that the only good argument for the consistency of ZF is the cumulative hierarchy, and "To someone who has no doubt that the properties of this construct are objective (even if only partially determinable by us) the matter is unproblematic. Others have to live with the uncertainty that is with us in most aspects of the human condition." – Timothy Chow Dec 25 '22 at 03:42
  • 4
    (continued) In a follow-up post, Bill Taylor construed Martin Davis as saying that "you might allow that some reasonable and rational doubt is possible on this point [i.e., the consistency of ZF]. Whether I personally have such doubts I'm not sure, (HAH!); but it seems reasonable to me too, that one might do so." Both of them firmly believed in the consistency of PA, but were cagey about whether they actively doubted the consistency of ZF. But there are surely others who have serious doubts about ZF but not PA. – Timothy Chow Dec 25 '22 at 03:47
17

George Boolos, eminent philosopher and logician, wrote as follows (perhaps slightly tongue-in-cheek):

enter image description here

He continued for a bit, and then...

enter image description here

(From G. Boolos, Logic, Logic, and Logic, Chapter 8: "Must we Believe in Set Theory?")

So, there you are: the answer to your question is "yes". At least he suggests that perhaps "set theory is not true" (not the same as "formally inconsistent"). The cardinal he mentions is not normally regarded as "large": it isn't even weakly inaccessible. The proof that it exists is easy.

My personal knowledge of formalising mathematics in the proof assistant Isabelle/HOL suggests that ZFC is much, much stronger than necessary for most mathematics with the obvious exception of the study of ZFC itself. A great body of advanced mathematical constructions – even Grothendieck schemes, thought by some to require more than ZFC – went easily into Isabelle/HOL. Higher-order logic is weaker even than Zermelo set theory, which (lacking the axiom of Replacement) is itself much weaker than ZFC. So if ZFC were somehow found to be inconsistent, mathematics would survive.

  • 9
    Boolos seems to be questioning soundness – Benjamin Steinberg Dec 25 '22 at 15:54
  • As an expert in HOL, can you please provide a reference for this statement: "Higher-order logic is weaker even than Zermelo set theory"? – Jonathan Julian Oct 31 '23 at 17:24
  • I don't have a rigorous proof of this claim (especially the claim that it is strictly weaker, which I have heard). On the other hand, it's obvious how to interpret all the types and terms of higher-logic as constructions within Zermelo set theory. We don't need the replacement or foundation axioms to express functions and function spaces. – Lawrence Paulson Nov 02 '23 at 09:55
13

This is basically a long comment. I like Nik Weaver's careful distinction between the question of whether ZFC is consistent and the question of whether it is (e.g. arithmetically) sound, and would like to further propose a refinement of the question to not just whether people think ZFC might be inconsistent or unsound, but rather: if you were told that ZFC was inconsistent or unsound, which axiom would fall under your suspicion as something to be thrown out (edit: or weakened) first?

  • Finding replacement suspect is something that's already been brought up.
  • A finitist might find the axiom of infinity suspect, but probably not anyone else.
  • Of course there has always been an air of suspicion around the axiom of choice. Personally I do not believe that e.g. non-measurable sets exist in any reasonable sense so I am sympathetic to this sort of thing.
  • Nik Weaver has argued against the power set axiom, e.g. in The concept of a set, which I personally found quite eye-opening.
Qiaochu Yuan
  • 114,941
  • 23
    Regarding your third bullet, we already know by Gödel that Con(ZF) iff Con(ZFC) and more to the point, ZFC is conservative over ZF for arithmetic assertions. So the axiom of choice can't be the cause either for inconsistency or arithmetic unsoundness. – Joel David Hamkins Dec 25 '22 at 02:57
  • 8
    Without seeing the actual proof of inconsistency, I'd be inclined not to throw out any of the axioms or axiom schemata lock, stock, and barrel; rather, I'd expect that the inconsistency could be addressed by a suitable restriction. Maybe Separation or Replacement applies only to certain types of formulae, or only certain sets have power sets. – Timothy Chow Dec 25 '22 at 04:08
  • 7
    The possible arithmetic unsoundness of ZFC need not be due to a specific axiom but rather due to the whole apparatus/approach itself. In ZFC, the set $\mathbb{N}$ is defined as the smallest inductive set, so the "arithmetic assertions" are actually assertions about the smallest inductive set. It is possible (and actually, consistent once formalized) that the smallest inductive set does not capture our intuitive notion of the set of natural numbers (that is, the set supposed to consist of 0,S0,...) So it may be that the formalization/objectification of natural numbers as a set is problematic. – Burak Dec 25 '22 at 11:50
  • 1
    @Burak That sounds a lot like a suggestion that the problem is the axiom of infinity, right? – Timothy Chow Dec 25 '22 at 12:43
  • 2
    @Burak, that is very interesting. You are saying that arithmetic unsoundness might be the result of our using a wrong interpretation of arithmetic in set theory. We already know there are other wrong interpretations. See eg https://mathoverflow.net/q/423328/1946. – Joel David Hamkins Dec 25 '22 at 12:57
  • 4
    To add onto Joel's point in his first comment: the construction of $L$, whence we get the relative consistency of a strong form of choice, goes through in much weaker theories than ZF. E.g. Mathias has shown (https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf) how to do it in Mac Lane set theory. So even if one is skeptical of Replacement or Powerset or whatever other strong axiom, we still know that AC is harmless when it comes to consistency. – Kameryn Williams Dec 25 '22 at 16:23
  • 3
    @TimothyChow: That depends. If our expectation from Inf is to only create a set that we would consider as an "infinite" set, then I wouldn't say that Inf is problematic; because it is doing what it is supposed to. If our expectation from Inf is to indirectly allow the creation of the "correct" set that represents $\mathbb{N}$ somehow, then, yes, I'd blame it on Inf, in case of unsoundness. – Burak Dec 25 '22 at 18:59
  • @Burak In the MO question that JDH linked to, Emil Jeřábek quoted a result that PA is faithfully interpretable in ZFC if and only if ZFC is $\Sigma_1$-sound. Is that the sort of thing you're referring to? In particular, your suggestion applies only if ZFC fails to even be $\Sigma_1$-sound? – Timothy Chow Dec 25 '22 at 19:55
  • 3
    @TimothyChow: Yes. The scenario I was suggesting is basically about the smallest inductive set containing "unexpected" elements because all inductive sets do. (I don't want to say "non-standard" because here we are talking about the natural numbers of the metatheory/background theory itself, unless you also have another theory in mind, the natural numbers of which you take as the "standard" one.) In this case it is perfectly possible that ZFC proves an assertion $\exists n \in \omega\ \varphi(n)$ but none of $\varphi(0),\varphi(1),...$ – Burak Dec 25 '22 at 20:27
  • 2
    @Burak That said, I think it's worth noting that the usual $\mathsf{ZFC}$-implementation of $\mathbb{N}$ is the best possible given $\mathsf{ZFC}$ as our "implementer," in the following sense: (much less than $\mathsf{ZFC}$ can prove that) given any $\mathcal{M}\models\mathsf{ZFC}$ and any (say) discrete ordered positive semiring $\mathcal{P}$ interpretable in $\mathcal{M}$, $\omega^\mathcal{M}$ is $\mathcal{M}$-definably isomorphic to an initial segment of $\mathcal{P}$. So we don't have a situation with many "candidate implementations" of $\mathbb{N}$ - there's only one plausible choice. – Noah Schweber Dec 26 '22 at 05:06
  • 3
    Of course this in no way should increase our confidence in $\mathsf{ZFC}$, I just think it's an interesting point; I don't know of any natural foundational-ish theory which $(i)$ doesn't have a "best possible" implementation of $\mathbb{N}$ but $(ii)$ doesn't involve actively destroying all possible such implementations (I'm thinking of Hamkins' multiverse with "well-foundedness mirage" here, IIRC). I guess this is unsurprising since we expect foundational-ish theories to be able to implement some amount of second-order logic, and "pre-theoretic $\mathbb{N}$" is second-order characterizable. – Noah Schweber Dec 26 '22 at 05:08
7

Some more detail about Nelson's work:

For most of his life, Ed Nelson tried to show that Peano Arithmetic (and weaker systems) was somehow inconsistent.

This was (initially) based on the idea that one could take the enumeration of all partial recursive functions and somehow make this construction total, thereby deriving a contradiction (via a diagonal argument).

Ed later refined this to an attempt at showing that the exponential function led to inconsistency. This was motivated by the Bellantoni-Cook framework of safe recursion in which the exponential function stood out for being the 'first' function with exceptional properties.

Sam Sanders
  • 3,921