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:
Question arising from Voevodsky's talk on inconsistency by John Stillwell,
Nelson's program to show inconsistency of ZF, by Andreas Thom,
Pierre Colmez, La logique c’est pas logique !
EDIT. Here the link to the FOM list discussing these themes.
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.
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.
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.
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 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.
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.
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.
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.
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.
Mathematics is too big to fail.
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.
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.
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.
From http://www.scottaaronson.com/papers/pnp.pdf p. 3 since I had the link handy from another thread:
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.")
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).