# What if Current Foundations of Mathematics are Inconsistent? [closed]

The title of the question is also the title of a talk by Vladimir Voevodsky, available here.

Had this kind of opinion been expressed before?

EDIT. Thanks to all answerers, commentators, voters, and viewers! --- Here are three more links:

Pierre Colmez, La logique c’est pas logique !

EDIT. Here the link to the FOM list discussing these themes.

-

## closed as no longer relevant by Felipe Voloch, Andres Caicedo, Mark Sapir, quid, Simon ThomasDec 25 '11 at 21:24

This question is unlikely to help any future visitors; it is only relevant to a small geographic area, a specific moment in time, or an extraordinarily narrow situation that is not generally applicable to the worldwide audience of the internet. For help making this question more broadly applicable, visit the help center. If this question can be reworded to fit the rules in the help center, please edit the question.

Then the unreasonable effectiveness of mathematics would become slightly more unreasonable –  Piero D'Ancona Oct 3 '10 at 11:20
I'm confused. Is the question, "What if the current foundations of Mathematics are inconsistent?" Or is the question, "Has this kind of opinion been expressed before?" –  Gerry Myerson Oct 3 '10 at 12:15
+1 just for pointing out this talk. –  Michael Bächtold Oct 3 '10 at 12:33
I don't understand his objection to Gentzen's proof at 29:00. Why would someone be skeptical about well foundedness of $\epsilon_0$? –  muad Oct 3 '10 at 13:36
Bourbaki dropped the axiom(-scheme) of replacement in their development of mathemetics, so they don't, I think, have enough mathematics to build the ordinals. However their work seems to indicate that they had enough to do an awful lot of mathematics (probably all of the mathematics I've ever done and will do won't need replacement). My guess is that if ZFC is inconsistent then replacement will be the first axiom for the chop. –  Kevin Buzzard Oct 3 '10 at 20:54

The talk in question was given as part of a celebration (this past weekend) of the 80th anniversary of the founding of the Institute for Advanced Study in Princeton. As you might guess there were quite a few very well-known mathematicians and physicists in the audience. (To name just a few, Jack Milnor, Jean Bourgain, Robert Langlands, Frank Wilczek, and Freeman Dyson, all of whom also spoke during the weekend.) The talk was a gem, and what did come as a surprise, at least to me, was that towards the end of his talk Voevodsky let on that he hoped that someone did find an inconsistency---and that by that time there was no audible gasp from the audience. There was of course a very lively discussion after the talk, and nobody seemed willing to say they felt that the "Current Foundations" (whatever they are) are definitely consistent. Of course Voevodsky was NOT saying that he felt that the body of theorems making up the "classic mathematics" that we normally deal with might be inconsistent, that is quite a different matter. What we should keep in mind is that a hundred years ago an earlier generation of mathematicians were quite surprised by not one but several "antinomies", like Russell's Paradox, The Burali-Forti Paradox, etc., (and that was followed by the greatest century in the history of Mathematics). As to the question "Had this kind of opinion been expressed before?", yes of course it has, but perhaps not so forcefully or in such a high-level forum. One person who has been expressing such ideas in recent years is my old friend Ed Nelson, who was also in the audience. (You can see his ideas in a recent paper: http://www.math.princeton.edu/~nelson/papers/warn.pdf). I spoke with him after the talk and he seemed pleased that it was now becoming acceptable to discuss the matter seriously.

-
+1 for the link to Nelson's paper -- it's an interesting read. Thanks! –  José Figueroa-O'Farrill Oct 3 '10 at 15:26
I'm waiting for Andy Putman to comment on the proper spelling of "antinomy". –  Gerry Myerson Oct 3 '10 at 22:18
@Gerry : Have I really acquired that strong a reputation for pedantry? Not that I'm claiming it's false -- I just asked my wife if I was an obnoxious pedant, and she nodded her head vigorously -- but the only spelling errors I recall correcting on MO involve my last name, which mathematicians seem unable to spell correctly. When I was a grad student, I recall visiting another university to give a talk, and on the drive from the airport a rather prominent mathematician who couldn't spell my last name angrily chewed me out for not posting my papers to the arXiv... –  Andy Putman Oct 4 '10 at 1:43
@Andy, sorry, no implication of pedantry intended - I just noticed that the answer above suffered from the same m and n transposition that affects so many who trip over your last name, and so I thought you'd be the logical person to point out that "antimonies", in this context, should be "antinomies". –  Gerry Myerson Oct 4 '10 at 4:43
Ah, that's actually a pretty clever joke! So clever, of course, that I totally missed it when I first saw it. Well, then, I must insist on the correct spelling! In fact, I'll correct it myself! –  Andy Putman Oct 4 '10 at 4:48

Contrary to popular opinion, there is no single foundation for mathematics. Probably you're referring to ZF or ZFC, but most mathematics can be developed on the basis of axioms that are logically much weaker than that. If an inconsistency in ZF were discovered, we would analyze the inconsistency and then scale back to some weaker system that would avoid the inconsistency yet still suffice for 99%+ of mathematics. Much of the work of finding other candidates for foundations, and figuring out how much mathematics can be developed from them, has already been done by those working in the field known as "reverse mathematics." The basic text in this field is Simpson's Subsystems of Second-Order Arithmetic, but there is a growing literature.

We've already seen a dry run of this kind of instantaneous damage control. When Kunen's inconsistency theorem showed that Reinhardt cardinals were inconsistent, his work was hailed as a major achievement, but all we did was toss out Reinhardt cardinals and restrict ourselves to large cardinals below that bound.

For most mathematicians, "ZFC" is just an arbitrary trigraph that is cited when the need arises to specify a particular foundation for mathematics. I daresay many people who toss the trigraph around couldn't even state all the axioms of ZFC precisely. If we scale back to some other system that goes by some other trigraph, it won't take much retraining to learn the new trigraph. For most researchers, that will be the only impact on their day-to-day work.

-
Your last paragraph almost made me ruin my (new!) keyboard with coffee. +1, as MO does not do that often enough! –  Mariano Suárez-Alvarez Oct 4 '10 at 17:39
Thus Paul Feyerabend's "Great scientists are methodological opportunists who use any moves that come to hand, even if they thereby violate canons of empiricist methodology" translates into "Great mathematicans are foundational opportunists who use any moves that come to hand, even if they thereby violate canons of logical methodology"? –  Bruce Arnold Oct 4 '10 at 20:59
@Bruce: No, the point is that ZFC is way overkill for most of mathematics, so we have tons of slack to scale it down if necessary. See this MO question: mathoverflow.net/questions/36580/… or this one: mathoverflow.net/questions/39452/… –  Timothy Chow Oct 4 '10 at 22:00
Reinhardt cardinals havnt been completely tossed out yet: they are inconsistent with ZFC, but it is unknown if they are consistent with ZF. –  Richard Borcherds Oct 4 '10 at 22:41
But, if I understand that correctly, it appears to me that Voevodsky is concerned about the consistency of first order Peano arithmetic, which is more serious than the non-existence of an "overly large" cardinal. In particular, Voevodsky has stated in his talk that the ordinal $\epsilon_0$ might not exist. –  Greg Graviton Oct 6 '10 at 16:54

If I found an inconsistency in mathematics, I would write up solutions to the six remaining Clay problems, collect my six million, retire and let you guys sort out the mess.

-
If you could write up proofs of those problems where it wasn't obvious you had found a contradiction in ZFC, you'd deserve all the money. –  Ryan Budney Oct 3 '10 at 23:14
Uhm, the Yang-Mills mass-gap problem includes the rigorous mathematical formulation of the problem itself, so you can't get the prize just by using the inconsistency of ZFC... –  Yuji Tachikawa Oct 4 '10 at 1:44
I agree with Ryan. This is a great idea ;-). –  Martin Brandenburg Oct 4 '10 at 8:21
You could collect seven or eight million, not six or seven (depending on Yang Mills): the P=NP prize is the only one formulated in such a way that either a positive or negative answer is guaranteed 1 million (in contrast, if one found a zero of zeta off the line, a committee would have to decide whether this was really a significant achievement worthy of that million). So if you prove inconsistency, you (or your lawyer) can claim P=NP and P<>NP... –  Paul-Olivier Dehaye Oct 4 '10 at 13:13
Randall Munroe, creator of the comic strip xkcd, points out a flaw in your scheme: xkcd.com/816 (make sure to mouse over the strip) –  Timothy Chow Nov 9 '10 at 20:01

I'm annoyed by the careless use of the word "proof" in Voevodsky's lecture. Of course, in the context of everyday mathematical discussions, it is normally sufficiently clear what one means by "proof" (it usually means something like "argument that is formalizable in ZFC"; even though I agree with Timothy Chow that most mathematicians wouldn't be able to explain exactly what ZFC is, they are nevertheless trained to recognize certain things as being "proofs" and I believe that those things that mathematicians normally recognize as proofs correspond to "proofs in ZFC"). But in the context of a discussion about foundations, it is far from clear what "proof" means and it is good practice to be more precise (proof in PRA? proof in PA? proof in ZFC? what?). There is no absolute notion of proof that, once presented, eliminates any possibility of doubt forever.

There doesn't seem to be anything new/interesting about Voevodsky's lecture. Anyone that is mildly educated about foundations has already entertained the question "what if ZFC is inconsistent?" or "what if PA is inconsistent?"; questions like that come around, from time to time, in any forum that discusses foundations of mathematics.

As Voevodsky mentioned, it is possible to present a constructive proof that an inconsistency in PA leads to an ever decreasing sequence in epsilon_0 (he mentioned a proof by Gentzen; there is also one by Gödel himself). Such proof convinces me that PA is consistent, as I find the idea of constructing an ever decreasing sequence in epsilon_0 rather crazy. But, of course, one can say "so what? I'm skeptical" (of course, one could also say that about any proof).

Sadly, Voevodsky's proposal about what to do if PA turns out to be inconsistent seems to me somewhat silly. If I understand him correctly, what he proposes is that we should have a system which is inconsistent, but we should also have some algorithm which separates "unreliable proofs" from "reliable proofs" (in such a way, I suppose, that there shouldn't be a "reliable proof" of both P and not(P); otherwise, I cannot understand what "reliable" could possibly mean). This "two step" scheme doesn't help at all. Instead of having "proofs" that can prove both P and not(P) and "reliable proofs" that do not prove both P and not(P), we could just restrict the term "proof" to the "reliable proofs". But, if one assumes the existence of an algorithm that decides whether something is or isn't a proof, and if the system is sufficiently complex to allow for interesting mathematics to be done within it, then Gödel's arguments would again present the usual obstruction for the existence of finitary proofs of consistency.

-
I think Voevodsky intends to get around your last argument by not actually assuming the existence of an algorithm that separates reliable and unreliable proofs. Rather, it seems that he describes a probabilistic algorithm that given a reliable proof will generically produce a certificate of its reliability in finite time, but given an unreliable proof it will simply not halt. So there would be no way of proving unreliability of a proof using this hypothetical algorithm, and he leaves open the possibility that there will exist reliable proofs whose reliability cannot be proven either. –  Dan Petersen Oct 7 '10 at 7:26
Ok, so normally we have an algorithm that checks whether something is a proof (i.e., the set of all proofs is recursive), which implies that the set of all theorems is $\Sigma_1$ (i.e., recursively enumerable). The new proposal would be: let's have an algorithm that takes a proposed proof as input, sometimes it halts and answers "yes, that is a (reliable) proof" and sometimes it doesn't halt. This makes the set of all (reliable) proofs $\Sigma_1$ (instead of recursive), but this again implies that the set of all theorems is $\Sigma_1$, so I guess Gödel-like arguments would apply just as well. –  Daniel Tausk Oct 7 '10 at 12:32
Probably I misused the word probabilistic algorithm -- I'm no computer scientist. What I meant is that he seems to leave open the possibility that there are reliable proofs for which this hypothetical algorithm would not halt, but that one should get a certificate for "most" reliable proofs. –  Dan Petersen Oct 7 '10 at 13:20
Ok, so maybe we would have "proofs", "reliable proofs" and "certifiably reliable proofs", i.e., those "reliable proofs" for which the algorithm halts in finite time and answers "yes, this is reliable" (actually, it would be semantically less messy to restrict the term "proof" just for the "certifiably reliable proofs"). Since a Gödel-like theorem would block finitary proofs of consistency of the theory in which only the "certifiably reliable proofs" are considered, it would, a fortiori, block finitary proofs of consistency of the theory in which all "reliable proofs" are considered. –  Daniel Tausk Oct 7 '10 at 14:05
Unfortunately, there seems to be no trivial way of getting around Gödel's theorem (otherwise, people like Gödel and Hilbert would have already found a way to do it). Either we work with systems for which no strictly finitary proof of consistency (say, a proof in PRA or less) is possible or we work with systems that cannot handle the vast majority of what we today call "mathematics". –  Daniel Tausk Oct 7 '10 at 14:10

I once heard Mike Freedman (the Fields medalist) say he thinks ZFC is probably inconsistent but that the minimal length paradox is so long no-one has found it yet. Once a paradox is found, he said, we'll just patch it up with a new axiom, and continue. His reasoning seemed to be that it was unlikely that we happened to find a consistent theory.

-
Couldn't it also be the case that the minimal-length paradox is so long that human mathematics will always be able to avoid it? –  Qiaochu Yuan Oct 3 '10 at 16:24
To add to that, if ZFC was found to be inconsistent I doubt the inconsistency would be as interesting as something like Russell's paradox. If it were, I suppose that would be quite informative. –  Ryan Budney Oct 3 '10 at 16:30
Compare Pierre Cartier, as quoted by David Ruelle in Chance and Chaos: "The axioms of set theory are inconsistent, but the proof of inconsistency is too long for our physical universe." –  Todd Trimble Oct 3 '10 at 20:09
I'm curious: Is there a rigorous sense in which it can be said that "most" theories are inconsistent? (I'd imagine the answer here to be yes.) But it might be worth asking if there's some sort of phase transition, such that almost all inconsistent theories have a relatively short contradiction... –  Harrison Brown Oct 4 '10 at 4:23
I'm also intrigued: what does Freedman intend by "patch [the inconsistent theory] with a new axiom"? Strengthening a too-weak theory is easy, and can indeed be patched — at the crudest level, you can just add an axiom doing whatever you want. But weakening an inconsistent theory is harder: all the existing axioms work together in complicated ways, and taking any one axiom out usually makes it break down (it certainly does with ZFC), so you have to rewrite at least parts of the theory from scratch. Hence things like constructive set theories, dependent type theory, etc.. –  Peter LeFanu Lumsdaine Oct 4 '10 at 17:17

Suppose today's news is actually, that in some form "current foundations of mathematics are inconsistent". Would any mathematician stop his-her research work for this? I don't think so. Even an antinomy has a mathematical content; after changing suitably the formal system in which it is formulated, the antinomy would become a positive statement, and the show would go on.

-
After all, the show must go on. –  babubba Oct 3 '10 at 19:27
that's possibly the point of the whole matter ;-) –  Pietro Majer Oct 4 '10 at 6:26
I personally disagree. I mean personally in that, if someone proved that a programming language that I use fails with some probability, then I would take more care with the code that I write. (By fail, I mean that an execution outputs something other than the desired result with some probability.) –  Michael Wehar Sep 14 '14 at 1:01

This didn't work when I tried to post it the first time, hope this won't wind up as a double post.

Thorsten Altenkirch, a constructive logician and computer scientist, made a memorable quote on the TYPES Forum mailing list in June 2008 which is very much in the spirit of Voevodsky's talk:

It seems to me that Type:Type is an honest form of impredicativity, because at least you know that the system is inconsistent as a logic (as opposed to System F where so far nobody has been able to show this :-). Type:Type includes System F and the calculus of constructions and I think all reasonable programs can be reformed into Type(i):Type(i+1) possibly parametric in i. However, sometimes you don't want to think about the levels initially and sort this out later - i.e. use Type:Type. A similar attitude makes sense in Mathematics, in particular Category Theory, where it is convenient to worry about size conditions later...
The system he is tongue-in-cheek questioning the consistency of is System F, which would correspond to second-order, not first-order, arithmetic. Type:type is an axiom that makes constructive type theory inconsistent (Girard's Paradox), so the "honest impredicativity" he refers to is therefore similar to what Voevodsky was talking about: we're admitting that everything is inconsistent and then doing our work anyway.

-
To be fair, what Thorsten refers to as "dishonest impredicativity" is what most constructivists object to: the existence of "from above" constructions in mathematics for which there are more philosophical reasons to have doubts than simple first order arithmetic. In particular, there is no simple Gentzen-like argument for 2nd order arithmetic. –  cody Feb 4 at 23:55

Voevodsky is not the only one who hopes for a proof of inconsistency (as mentioned in Dick Palais's answer): see Conway and Doyle's Division by Three, bottom of page 34, where they express the same kind of skepticism as Nelson.

-
I think it's slightly misleading to represent anything in this paper as Conway's opinion. A footnote on the first page clearly says that he didn't write the paper, nor particularly liked "the exposition", which presumably includes the final remarks on inconsistency. –  Pietro KC Oct 4 '10 at 7:04
I would fully agree, except that I've heard Conway say similar things in person. –  Todd Trimble Oct 4 '10 at 10:48
(I took Doyle's depiction of Conway's objection to the form of the paper -- all the "fluff" -- as referring more to the very discursive expository style.) –  Todd Trimble Oct 4 '10 at 11:05
Oh, OK, that's another matter entirely then. :) –  Pietro KC Oct 5 '10 at 3:01

Using the following table to you convert between propositional logic and arithmetic of multivariate polynomials over $\mathbb{F}_2$: $$\mbox{TRUE} \leftrightarrow 1$$ $$\mbox{ FALSE} \leftrightarrow 0$$ $$X \mbox{ or } Y \leftrightarrow xy+x+y$$ $$X \mbox{ and } Y \leftrightarrow xy$$ $$!X \leftrightarrow x+1$$ So a proposition $P(X_1,X_2,\ldots, X_n)$ can be satisfied if and only if the corresponding polynomial equation $p(x_1,x_2,\ldots,x_n)=1$ has a solution. For example, the proposition $$X \mbox{ and } !X$$ is not satisfiable. This corresponds to the fact the polynomial $x(x+1)=1$ or $x^2 + x +1=0$ has no solutions over $\mathbb F_2$.

We now should do in logic as we do in algebra. Since this proposition isn't satisfiable over our standard logic we create an algebraic extension of logic where truth values now live in
$$\mathbb F_2[x]/(x^2 + x + 1)!$$

I don't know how to extend these ideas to first order logic.

-
I was TOTALLY late to the party. –  Taylor Dupuy Sep 2 '11 at 3:38
This is cute, and I'm voting it up. –  Ryan Reich Dec 25 '11 at 0:52

The inconsistency of mathematics is a quite common option when you consider seriously some non-classical logics.

For an introduction, read the following page from the Stanford Encyclopedia of Philosophy : http://plato.stanford.edu/entries/mathematics-inconsistent/

-

Comment:

Putman says "Of course Voevodsky was NOT saying that he felt that the body of theorems making up the "classic mathematics" that we normally deal with might be inconsistent, that is quite a different matter."

But wasn't he? His conjecture is "I suggest that the corret interpretation of Goedel's second incompleteness theorem is that it provides a step towards the proof of inconsistency of many formal theories and in particular of the "first order arithmetic"."

What I don't understand is this. If classical arithmetic is inconsistent anywhere, then it is inconsistent everywhere (an inconsistency proves everything). So why haven't we found any inconsistencies yet?

What is cool is that the notion of reliability he talked about seems to be a move toward a "local" notion of consistency.

Humm, does this make sense? Let A and B be closed formulas of some formal system. Define the "logical distance" between A and B to be the shortest proof of B assuming A (inculding the data of the number of applications of the rules of inference, etc.) Say that B is "locally consistent" with A if the logical distance between A and B is strictly less than the logical distance between A and not-B. A theory is locally consistent if for every pair (A, B) the logical distance from A to B is not equal to the logical distance from A to not-B. Etc. Etc.

-
Paul, one simple possibility for why we haven't found any inconsistencies yet is that the shortest proof of an inconsistency is too long to write down physically. –  Timothy Chow Sep 1 '11 at 22:51

What if the current foundations of Mathematics are inconsistent?

Had this kind of opinion been expressed before?

The opinion that the Peano Arithmetic is likely to be inconsistent is not uncommon, along with ideas on how to deal with this (targeting the "what if" question). Wikipedia has an article about that, and MathOverflow has a question. These have links to works by Nelson, and to a paper by Sazonov, which among others refer to Parikh (1971) and Yessenin-Volpin (1959). These things have been discussed also in a paper by Rashevski (1973) and a few years ago also (quite extensively, with a number of additional references) at the FOM mailing list.

An implicit question is "What do you think of Vladimir Voevodsky's talk?"

His message is obviously: "Guys, your Peano Arithemetic is something not to be taken too seriously. Which is a good reason to be a bit more serious about Voevodsky's univalent foundations!" I hear this message, in particular, when he speaks of "reliable proofs", and in fact it does resonate with me. His subsequent talk about the univalent foundations is much more substantial; having a separate copy of the "slides" helps to follow the video.

-

Have you ever lay awake at night, terrified of what would happen were the Zermelo-Fraenkel axioms found to be inconsistent the next morning? Would bridges collapse? Would every paper ever published in STOC and FOCS have to be withdrawn? ("The theorems are still true, but so are their negations.")

-
This paper looks very nice, particularly for a non-logician! –  Spice the Bird Dec 25 '11 at 3:49

Mathematics is too big to fail.

-
Although I can see where this may be off topic, I actually think that this has some truth to it. As some other answers have said, if the current foundations are found to be inconsistent, we as mathematicians will step in and fix it by modifying the foundations such that they are still sufficiently rich to deal with math as a whole. At least I hope that this can be done in some manner. Perhaps some paraconsistent logic system will be the needed device that will fix up the foundations. –  Spice the Bird Dec 25 '11 at 3:44
People were saying the same about the USSR. –  Tomek Kania Mar 1 at 14:44

In the discussion of Gentzen's proof, Voevodsky expresses total bafflement at why someone would presume the ordinals are well-ordered. He does not say that he rejects any particular argument but rather seems to suggest there are no arguments. Why? Either he was simply not aware of any kind of reason, or somehow thought the audience didn't need to know about that. Neither option is good.

-

In either case this will not affect any practical applications of mathematics, because practical mathematics deals only with finite quantities, and finite arithmetics has been shown to be consistent. The paradoxes arise only when using abstract axioms, such as axiom of infinity, axiom of choice etc. That is the major body of analysis will survive in a form of constructivist analysis or a stricter approach (depending on where the inconsistency is discovered).

-
PA has only been shown to be consistent using infinite ordinals (whose existence is an extra assumption). In fact there are a (small) number of people who think that PA might be inconsistent. –  David Roberts Feb 20 '11 at 10:30
Peano arithmetic is not finite arithmetic. It includes axiom of potential infinity. If an arithmetic is built over a finite set of numbers, it is consistent. –  Anixx Feb 20 '11 at 12:43
And the group about you said does not accept the proof not because it requires extra assumptions, but because they reject the existence of infinite set of natural numbers (i.e. they just DISAGREE with usefulness of one of the axioms). The proof itself finitistic. –  Anixx Feb 20 '11 at 12:49
To sum it up: 1) the proof that PA is consistent exists, and is finitist. 2) People who disagree are ultrafinitists 3) all mathematical paradoxes so far were discovered outside of finitist realm. –  Anixx Feb 20 '11 at 12:54
What of you mean by "the proof that PA is consistent exists, and is finitist?". To what proof are you referring to? –  Joël Nov 22 '11 at 17:11