98

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.

Community
  • 1
Pierre-Yves Gaillard
  • 4,336
  • 96
    Then the unreasonable effectiveness of mathematics would become slightly more unreasonable – Piero D'Ancona Oct 03 '10 at 11:20
  • 3
    What opinion? That ZFC or even Peano Arithmetic is in fact inconsistent? The trouble is that this sort of thing is not too likely to be put in print by a reputable mathematician, even if he expresses his (perhaps occasional) doubts in private. But yeah, I can think of a few reputable mathematicians who sometimes express sentiments ("opinion" is maybe too strong a word) along these lines. Backing that up is another story altogether. – Todd Trimble Oct 03 '10 at 11:45
  • 3
    Does anyone know what Voevodsky means by the "current troubles between mathematics and physics" in his talk?! – José Figueroa-O'Farrill Oct 03 '10 at 12:11
  • 21
    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 03 '10 at 12:15
  • 9
    +1 just for pointing out this talk. – Michael Bächtold Oct 03 '10 at 12:33
  • @Gerry Myerson - Sorry about the confusion. The question is "What if the current foundations of Mathematics are inconsistent?" A subsidiary question is "Has this kind of opinion been expressed before?"... At least that's how I see it. You're welcome to answer any of the questions, to ask others, to edit the question... - An implicit question is "What do you think of Vladimir Voevodsky's talk?" – Pierre-Yves Gaillard Oct 03 '10 at 12:37
  • 9
    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 03 '10 at 13:36
  • 1
    I think he needs to be a little more specific about what he means by this question.WHICH foundations? ZFC set theory? Categorical foundations a la Lawvere? What? – The Mathemagician Oct 03 '10 at 18:31
  • 13
    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 03 '10 at 20:54
  • 2
    Kevin Buzzard: yup. See http://www.mta.ca/~cat-dist/catlist/1999/zf-010499. – Todd Trimble Oct 03 '10 at 21:30
  • 3
    @Todd: Lawvere points out a few messages in that this was a (slightly irresponsible) April Fool. The final comment of the thread is appropriate: "I suppose that it is possible that somebody, browsing at random, might find it in the CATEGORIES archives, in years to come, and not read ahead to find out what the world had had to say about this discovery back in the mad, exciting days of the late C20." Note that this does not detract from the larger issue that ZF may well be inconsistent. – András Salamon Oct 04 '10 at 00:09
  • 2
    Um, yes, I know all this, Andras?! Was joking around myself?! – Todd Trimble Oct 04 '10 at 00:23
  • @Todd: not fair, you are only allowed to resurrect those jokes once a year! – András Salamon Oct 04 '10 at 12:45
  • @Andras: Joking aside, there is a serious point behind Taylor's post: that the replacement axiom is indeed enormously powerful, even if not strictly speaking necessary for most of core mathematics (which can be developed within a universe of sets whose rank is less than $\omega+\omega$, where replacement fails). In fact, Taylor's book Practical Foundations of Mathematics culminates in a discussion of how to formulate the replacement axiom in the context of dependent type theory. – Todd Trimble Oct 04 '10 at 13:27
  • @Kevin Buzzard: as the (non-joking) background in Todd's link points out, while Bourbaki don't include Replacement in the same form that ZF has it, they do include an essentially equivalent axiom: that the union of any set-indexed family of sets forms a set. ZF with replacement dropped (aka Zermelo Set Theory) is not powerful enough for much mathematics at all: for instance, iirc, it can't construct the free monoid on an arbitrary set, nor hence eg polynomial algebras in noncommuting variables. – Peter LeFanu Lumsdaine Oct 04 '10 at 17:03
  • Actually, my error: Todd Trimble points out to me off-list that you can indeed construct the free monoid on a set $X$ without replacement, with a bit more care (as eg a subset of the set of partial functions from $\mathbb{N}$ to $X$). What I had in mind is that without replacement, one can’t always make constructions of the form $\bigsqcup_n F^n(X)$, (or $\bigprod$, $\bigcup$, $\varinjlim$ etc.) where $F$ is an arbitrary function on sets. I'm fairly sure I've seen at some point a simple, mathematically well-known example which isn't salvageable in the way “free monoid” was; but now I forget… – Peter LeFanu Lumsdaine Oct 04 '10 at 22:10
  • 2
    @Kevin: Replacement will be chopped only if doing so fixes whatever inconsistency happens to shows up. It doesn't make much sense to speculate on what the fix will be when it ain't broke yet. – Timothy Chow Oct 04 '10 at 23:25
  • 3
    Given that ZFC without the axiom of infinity is known to be consistent, it would make as much sense to say that the axiom of infinity would be the first to go, since that will certainly solve the problem :) – Carl Mummert Oct 06 '10 at 17:37
  • ZFC without the axiom of infinity is known to be consistent? – Steven Gubkin Nov 06 '10 at 00:59
  • 3
    @Steven Gubkin: ZFC minus infinity plus its negation can be interpreted into Peano arithmetic, in the formal logical sense of interpreted. Since the latter has been proven consistent (in multiple independent ways, in fact), the former must also be consistent. – Carl Mummert Nov 11 '10 at 23:13
  • 2
    I have added a vote to close, for being no longer relevant. I feel this question is attracting more answers that are not 'adding value', as they say. Discussion at meta if necessary. – David Roberts Feb 20 '11 at 10:33
  • 1
    Dear @Thomas: Is this http://golem.ph.utexas.edu/category/2011/09/voevodsky_on_fom.html the link you wanted to give? – Pierre-Yves Gaillard Sep 12 '11 at 14:41
  • Dear Pierre-Yves, thanks for correcting that! I wonder how that happened. – Thomas Riepe Sep 13 '11 at 01:58
  • 1
    Interesting that this question was closed as "no longer relevant". Does that mean it has been proved that the current foundations of mathematics are consistent? [just kidding - I know the closure options are very limited] – Gerry Myerson Nov 29 '12 at 06:33

16 Answers16

96

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.

Timothy Chow
  • 78,129
  • 20
    Your last paragraph almost made me ruin my (new!) keyboard with coffee. +1, as MO does not do that often enough! – Mariano Suárez-Álvarez Oct 04 '10 at 17:39
  • 7
    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 04 '10 at 20:59
  • 11
    @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: http://mathoverflow.net/questions/36580/is-all-ordinary-mathematics-contained-in-high-school-mathematics or this one: http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture – Timothy Chow Oct 04 '10 at 22:00
  • 7
    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 04 '10 at 22:41
  • @Richard: That's true, but being inconsistent with ZFC makes them rather less interesting from the point of view of foundations. – Timothy Chow Oct 04 '10 at 23:14
  • 7
    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 06 '10 at 16:54
  • 6
    I admit that I didn't listen to Voevodsky's talk. But in any case, while an inconsistency in PA would be truly spectacular, what I said still holds. Most mathematics can be developed on foundations weaker than PA, so we would scale back to some system that avoided whatever inconsistency was discovered. – Timothy Chow Oct 07 '10 at 04:35
82

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.

Andy Putman
  • 43,430
Dick Palais
  • 15,150
  • 4
    +1 for "Wouldn’t it be great to have a god who would do actually infinite searches for me and tell me whether formulas of arithmetic are true or false? But lo! here is a little brass one that will fit nicely on my desk." and "But mathematics used to be fun, and this is more tedious than the income tax. I’ll just mop up the remaining millennium questions and with my six million dollars I’ll abandon mathematics and take up beekeeping." – stankewicz Oct 03 '10 at 15:16
  • 7
    +1 for the link to Nelson's paper -- it's an interesting read. Thanks! – José Figueroa-O'Farrill Oct 03 '10 at 15:26
  • 18
    I'm waiting for Andy Putman to comment on the proper spelling of "antinomy". – Gerry Myerson Oct 03 '10 at 22:18
  • 24
    @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 04 '10 at 01:43
  • 30
    @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 04 '10 at 04:43
  • 20
    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 04 '10 at 04:48
  • 1
    What were the other talks about? Conc. Voevodsky's talk: I wonder if he was stimulated by what seems to by a tradition among russian mathematicians to take physics serious, e.g. the way Drinfeld, Kontsevich and Manin enjoyed taking up concepts from th. physics like Feynman integrals, renormalization, deformation quantization,mirror sym. ... like some "new platonic idea" independent of consistency issues. ... And the "creative" part of the procedure Voevodsky sketches is actually what makes mathematics interesting, without it it would be just very boring. – Thomas Riepe Oct 06 '10 at 09:29
73

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.

Felipe Voloch
  • 30,227
  • 42
    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 03 '10 at 23:14
  • 22
    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 04 '10 at 01:44
  • I agree with Ryan. This is a great idea ;-). – Martin Brandenburg Oct 04 '10 at 08:21
  • 31
    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 04 '10 at 13:13
  • 32
    Randall Munroe, creator of the comic strip xkcd, points out a flaw in your scheme: http://xkcd.com/816 (make sure to mouse over the strip) – Timothy Chow Nov 09 '10 at 20:01
  • 2
    @Timothy :-) You see, the trick is not to reveal the inconsistency. But see Ryan's comment above. – Felipe Voloch Nov 09 '10 at 21:16
33

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.

Daniel Tausk
  • 373
  • 6
    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 07 '10 at 07:26
  • 2
    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 07 '10 at 12:32
  • 1
    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 07 '10 at 13:20
  • 2
    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 07 '10 at 14:05
  • 12
    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 07 '10 at 14:10
28

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.

Jim Conant
  • 4,838
  • 21
    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 03 '10 at 16:24
  • 7
    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 03 '10 at 16:30
  • 1
    Agree. Actually I think you mean antinomy or contradiction, rather than paradox (a harmless thing). – Pietro Majer Oct 03 '10 at 19:15
  • 19
    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 03 '10 at 20:09
  • 6
    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 04 '10 at 04:23
  • @Pietro: Yes, I meant contradiction! – Jim Conant Oct 04 '10 at 11:46
  • 3
    @Harrison: interesting question(s). My first wonder is whether it's even (intuitively) true, that most theories are inconsistent; I can't make up my mind. One could ask similar but perhaps simpler questions like, "are most group presentations presentations of the trivial group?" Here I think my instinct leans more towards saying that "most" group presentations, if not of the trivial group, are undecidable. – Todd Trimble Oct 04 '10 at 12:11
  • 8
    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 04 '10 at 17:17
  • 3
    @Todd : It's actually a theorem that in a precise sense, almost all group presentations are word hyperbolic (see http://en.wikipedia.org/wiki/Hyperbolic_group). In particular, almost all algorithmic problems are solvable within a "random group presentation". – Andy Putman Oct 06 '10 at 19:20
  • @Peter LeFanu Lumsdaine: of course you'd have to remove an axiom from ZFC and replace it with something weaker. – Ryan Budney Oct 06 '10 at 23:36
  • @Andy: thanks! That's very interesting. – Todd Trimble Oct 15 '10 at 12:10
  • "Unlikely" under what probability distribution? – user76284 Aug 19 '20 at 22:14
24

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.
Rob Simmons
  • 141
  • 1
    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 04 '15 at 23:55
24

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.

Taylor Dupuy
  • 360
22

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.

Pietro Majer
  • 56,550
  • 4
  • 116
  • 260
  • 18
    After all, the show must go on. – babubba Oct 03 '10 at 19:27
  • 3
    that's possibly the point of the whole matter ;-) – Pietro Majer Oct 04 '10 at 06:26
  • 1
    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 01:01
12

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.

Todd Trimble
  • 52,336
  • 3
    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 Oct 04 '10 at 07:04
  • 9
    I would fully agree, except that I've heard Conway say similar things in person. – Todd Trimble Oct 04 '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 04 '10 at 11:05
  • Oh, OK, that's another matter entirely then. :) – Pietro Oct 05 '10 at 03:01
9

Mathematics is too big to fail.

tab
  • 1
  • 1
    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 03:44
  • 3
    People were saying the same about the USSR. – Tomasz Kania Mar 01 '15 at 14:44
7

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/

Mathieu Vidal
  • 1
6

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
  • 167
  • 2
    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 01 '11 at 22:51
6

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.

Community
  • 1
Sergey Melikhov
  • 5,525
6

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.

Monroe Eskew
  • 18,133
5

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.")

none
  • 1
-20

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).

Anixx
  • 9,302
  • 5
    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
  • 4
    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
  • 2
    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
  • @Anixx (sorry to bring up such an old thread, but you've got me curious) To second Joël's question, what proof of consistency of PA do you refer to? Your earlier explanation suggests that "finitistic" means that one only works with finite structures, and I find it hard to believe there is a proof of PA like that. – Wojowu May 22 '16 at 18:12
  • @wojowu He's probably refering to Gentzen's proof. I really don't like the term "finitism", as I think at face value you could interpret that a number of different ways, but I think at least under one interpretation it would be reasonable to call Gentzen's proof "finitist" (Though this is not the sense in which Hilbert used the term). – Nathan BeDell Mar 13 '17 at 03:27