But WHAT is an open problem in mathematics?
UPDATE: This is the second post in a series of three on the same topic; the first one is here and the third one is here.
Two days ago I reported here on an ongoing debate over at the FOM list on some controversial statements made by Fields medalist Voevodsky on the status of the consistency of PA as a mathematical problem. In particular, I mentioned that Harvey Friedman had reported sending a message to Voevodsky, asking for clarifications: "how you view the usual mathematical proof that Peano Arithmetic is consistent, and to what extent and in what sense is "the consistency of Peano Arithmetic" a genuine open problem in mathematics."
Now Friedman reports that Voevodsky has replied:
Such a comment will take some time to write ...To put it very shortly I think that in-consistency of Peano arithmetic as well as in-consistency of ZFC are open and very interesting problems in mathematics. Consistency on the other hand is not an interesting problem since it has been shown by Goedel to be impossible to proof [sic].
So, what do we make of this? I am now more and more convinced that Toby Meadows (in correspondence) has it right when he says that there are different senses of a 'mathematical open problem' floating around. Toby suggested a weak and a strong reading of 'open problem/question' in this context:
On a weak reading of "open question", we might understand it as a question that is worth asking ... perhaps a research programme worth taking up. In this case, the fact that so much mathematical practice presupposes Con(PA) is going to be good evidence that Con(PA) is not open on this way.
The strong reading would be "that it is not the case that the question has been settled one way or the other in such a way that it is "impossible" for it to be otherwise."
On the strong reading, Con(PA) is perhaps not an open question, as Goedel's results have shown that assuming Con(PA) we cannot prove Con(PA) with merely PA; this is exactly what Voevodsky seems to be saying. However, as again noted by Toby, it doesn't mean that ~Con(PA) is NOT an open question; we know we cannot prove Con(PA) in PA, but we don't know yet whether we can or cannot prove ~Con(PA) in PA! Admittedly, this is a *very* unlikely outcome, but there is indeed as of yet no proof that ~Con(PA) cannot be proved in PA. And this is precisely what Voevodsky seems to be saying, at least as I understand him.
Another point worth mentioning is that here he seems to be relying on a Hilbertian sense of proving the consistency of a system T: Con(T) is only proved if it is proved in T itself, and it is perhaps in this sense that he (wrongly, to my mind) dismisses Gentzen's proofs. (I have lots of thoughts on this too, including foundational worries of circularity; if T is unsound, it might well prove Con(T) even though that's not the case, in particular given that Sou(T) --> Con(T), and an unsound T may well be able to prove Sou(T). But that's for another time.)
Anyway, all this to raise the deeply philosophical question: what is an open problem in mathematics? Are there different senses of 'open problem' floating around? Might this be what is behind all the debate between FOM'ers? M-Phi'ers seem particularly well-positioned to discuss these matters, so please go ahead and shoot!
(On this note, I'm off to Rio tomorrow, so internet access is going to be disrupted. But you can of course debate without me!)
The issue about open questions is a subtle one. We know that we cannot prove Con(PA) in PA unless PA is inconsistent. We also know, however, that we cannot prove ~Con(PA) in PA unless PA is omega-inconsistent. So, if PA really is 'correct' (i.e. the standard model is indeed a model of PA) then Con(PA) and ~Con(PA) are on a par, contra Voevodsky's suggestion. Of course, if he is right and arithmetic is inconsistent, then they are also on a par - since both would obviously be provable. So the only way to finesse a charitable interpretation that makes sense of his "consistency is not an open question but inconsistency is" nonsense is if arithmetic is consistent but omega-inconsistent (and thus only had non-standard models).
ReplyDeleteAt any rate, I have now had a chance to carefully watch the video of Voevodsky's talk, and I really can't do any better than see it as the semi-coherent ramblings of a smart, but very ill-informed amateur to foundations. Some highlights (some already noted, some not - approximate time in the video included for the masochistic):
(1) Misstatement of Goedel's theorem. Yeah, Yeah - he says that he has stated it in a stronger form than many might prefer. But the fact of the matter is this: Even if you grant all the crazy to follow about Gentzen and the rest (see below), and even if the claim on this slide might as a result turn out to be true, it isn't in any way what Goedel proved. [4:40]
(2) His fallacious inference from "we can't know that P" to "it's not the case that P" in his discussion of the third response to what he calls Goedel's paradox. Really? [11:25, see also 33:20]
(3) His near incoherent explanation of first-order formal systems. I felt like I knew less about first order logic at the end of this than I did at the beginning. [15:00 - 21:00]
(4) His 'argument' that (as best as I can make it out) the existence of undecidable predicates shows that we cannot interpret formulas of first-order logic as representing sets of natural numbers. I don't have any idea what is supposed to be going on at this point. At best, we have some serious confusions regarding the difference between semantic and epistemic notions. [25:50]
(5) His dismissal of Gentzen's consistency proof: Apparently, our only evidence for the non-existence of a non-terminating decreasing sequence of ordinals is Gentzen's claim that this is self-evident. Voevodsky pithily refutes Gentzen's intuitions with the powerful words "so what"?!? [29:50]
(6) His claim that what distinguishes constructive type theory from other formal systems is the fact that in type theory "a proof becomes an object that one can study inside the system itself" (so what exactly was I doing in my 'Boolos & Jeffrey' course two weeks ago with all those recursive relations and coding functions?) [37:30]
(7) His claim that "It would be wonderful if we could find the inconsistency." Direct quote. [42:00]
(8) His claim that "Such an interpretation definitely cancels out a lot of dubius philosophical noise around Goedel's Theorem" At this point, I laughed out loud. Voevodsky clearly would have benefitted from paying a bit more attention to some of that "dubious philosophical noise". [42:45]
Anyway, I realize this might not seem like a charitable reading. But much ink (or pixel light, at any rate) has been spilled trying to make sense of what this clearly very smart guy might have been up to, and I thought it was worth highlighting the evidence pointing to a less optimistic conclusion.
I watched Voevodsky's video as soon as it came out, since I follow his amazing use of type theory, so far as I can; but I haven't recently watched it.
ReplyDeleteThe lecture was extremely disappointing of course, but it is surprising to see this tempest in a teapot developing eight months later among philosophers and 'fom' types. (There has been quite a lot of water under the bridge in connection with his larger program since then! Coquand has written some nice slides outlining aspects of that program, exhibiting a characteristically philosophical sensitivity http://www.cse.chalmers.se/~coquand/equality.pdf )
Voevodsky's idea for his lecture was clearly to give some account of how his approach, modifying and reinterpreting the type theory used in e.g. Coq and Agda, can preserve the value of mathematical 'proofs' that arise in the development of what are in the end seen to be inconsistent theories. I'm not sure exactly what the point would have been. His title is 'what if the current foundations of mathematics are inconsistent', not 'what if the axioms of PA are inconsistent' -- the familiar results about of consistency and inconsistency in arithmetic were clearly meant to be a point of departure, and one he imagined he could make intelligible to his audience.
No one seems to bother noticing that this was clearly a talk he was forced to give for the sake of visiting benefactors and suchlike people -- it was one of many such talks celebrating the 80th anniversary of the Institute. But he was very much a lecturer poorly prepared for class and gave signs of really bad teaching skills in general. He spent an absurd amount of time on an lame account of syntax, for example. In the end, he got completely bogged down and there were about three sentences devoted to what I take to have been his purpose, the one I speculated about above.
I mentioned this on the FOM mailing list, but I don't think that it's that hard to make sense of Voevodsky's reply to Friedman, if we just imagine what we might say to a question such as, "Is the consistency of measurable cardinals an open problem?" The answer is no, if by "open problem" we mean what we normally mean by the term, namely a question that we can reasonably expect to be settled either positively or negatively by a proof or a disproof using generally accepted mathematical assumptions and logic. We cannot reasonably expect a proof of the consistency of measurable cardinals in this sense, but a disproof is not so crazy a thing to hope for.
ReplyDeleteAt the same time, putting the consistency of PA on the same footing as the consistency of a measurable cardinal is idiosyncratic to say the least, since the consistency of PA is trivially provable by ordinary mathematical means: the natural numbers are a model of PA. (Similarly, the fact that PA doesn't prove ~Con(PA) is trivially provable by ordinary mathematical means, contrary to what you seem to suggest when you say that "there is indeed as of yet no proof that ~Con(PA) cannot be proved in PA.") Idiosyncratic isn't the same as incoherent, though.
Clarification: when I said that "there is indeed as of yet no proof that ~Con(PA) cannot be proved in PA", I was actually trying to unpack what V. may have been thinking. But I realize now that my phrasing was not entirely fortunate, as it may seem to be a claim I am making myself. Since he seems to dismiss Gentzen's proofs of the consistency of PA, it wouldn't seem too strange if he also dismissed such arguments to establish the unprovability of ~Con(PA) in PA. As Roy notices above, we know that we cannot prove ~Con(PA) in PA unless PA is omega-inconsistent, so in many senses the unprovability of Con(PA) in PA (by Goedel) and the unprovability of ~Con(PA) are on a par.
ReplyDeleteCatarina,
ReplyDeleteI certainly didn't mean to be accusing you of a mistake - just further clarifying the issue.
I do want to further respond to a couple of points Michael made. I let this sit a few days to calm myself, since this sort of stuff annoys and frustrates me more than is probably reasonable (by 'this sort of stuff' I mean the content of Voevodsky's lecture, and not Michael's points - while, as will become clear below, I take issue with a few of the things Michael says, his points are at least clearly stated). At any rate, if this still comes across as picky and unfair, well, maybe they are. But I wanted to get them out there anyway.
(1) Michael mentions the fact that this talk was meant to provide philosophical motivation for the larger project in type theory within which Voevodsky is involved. Although I have not worked through the type theory material with the attention that I gave to the philosophical talk, I have no doubt (based on the comments of others I trust and the sort of people who Voevodsky is working with) that this technical work is interesting and mathematically rich, and promises to provide new insights into foundations. Be that as it may, the discussion amongst us FOM types is not about the larger project (at least, the vitriolic response involving comments such as my post above are not focused on this technical project). The worry is about this particular talk, and what can be gleaned about the apparent connections between FOM and the larger mathematical landscape.
(2) Although the talk WAS titled "What if the current foundations of mathematics are inconsistent", the talk itself is clearly intended to provide evidence for the inconsistency of PA and of any formal system as rich as PA (Voevodsky says as much multiple times during the talk). In correspondence with Harvey Friedman, Voevodsky has pretty much admitted that the talk was craptastic, writing "You are right, I was sloppy in my formulation" and, later, when Harvey mentions one (of many) proofs of the consistency of PA, asking "Could you give me a reference on this result about sub-sequences" (making it clear that he didn't really do his homework). The correspondence also, I think, makes it clear that Voevodsky doesn't understand that Goedel's theorem doesn't show that any system that can prove Con(PA) must be stronger than PA, but merely shows that any system that proves Con(PA) cannot contain PA (i.e. the two systems might be proof-theoretically incomparable, a point clearly explained in one of Catarina's original posts).
The full correspondence can be found here:
http://www.cs.nyu.edu/pipermail/fom/2011-May/015477.html
(3) The point about it being a talk he was 'forced' to give to benefactors, etc., really irks me (to be fair, this is both the result of reading more into the comment than Michael probably intended, and some very strong opinions of my own regarding bad presentation skills in academia). Voevodsky is, after all, a professor at the IAS. Presumably, giving talks to benefactors and suchlike people is part of his job - what they are paying him for. Further, when giving a talk to the public (as opposed to the ten or so people who might actually read one's publications), there is all the more reason to make sure the talk is clear and not misleading. Voevodsky's talk failed in this respect, regardless of what other flaws it had, and as a result, members of this audience, who likely have some influence in how funding for IAS and related endeavors is apportioned, now have a horribly inaccurate idea of the current state of foundations of mathematics.
Continued:
ReplyDelete4) My real worry here (and the real reason I am somewhat riled up about this - I can't speak for anyone else) is that it seems like a particularly striking example of a general tendency amongst non-philosophers to assume that philosophy is easy. After all, philosophy is just sitting in an armchair thinking hard about some problem until the answer becomes apparent to you. As a result, these scholars (usually someone working in X, who suddenly decide they want to work in philosophy-of-X) decide to do some philosophy, but make no effort to actually understand the huge amount of honest toil in philosophy-of-X that has occurred previously. Instead, they just walk into the room with the attitude that their obvious intelligence, plus their deep knowledge of X, will allow them to quickly and decisively clear up all the confusions that philosophers of X have been suffering from until now.
Now, I am not accusing Voevodsky of explicitly holding anything like this condescending view philosophy (after all, I have no more access to his inner mental states than he has access to an actual argument for the inconsistency of PA). Nevertheless, the content of the talk is, in fact, consistent with this sort of reading (just plug in "mathematics" for X).
Hi Roy,
ReplyDeleteGood points (btw, they don't seem exceedingly unfair to me). I was thinking of a follow-up post on the subsequent correspondence between Voevodsky and Friedman, but in your comments here, you seem to have raised the main points already, besides providing the link to the full correspondence (maybe YOU should write a follow-up post? :) )
It's funny indeed; this assumption that only a system strictly stronger than PA could prove Con(PA) seems to be an example of the attitude you were describing in your point 4).
Also, as for my clarification, I was replying to T. Chow's comment: "the fact that PA doesn't prove ~Con(PA) is trivially provable by ordinary mathematical means, contrary to what you seem to suggest when you say that "there is indeed as of yet no proof that ~Con(PA) cannot be proved in PA.""
I certainly don't think that "trivially provable by ordinary mathematical means" applies here (depending on what one means by 'trivially' and 'ordinary mathematical means'), but it's true that my original formulation was a bit unclear. Hence the need for a small clarification :)
Curiously, Chow has *just* posted a message on FOM on what he means by "trivially provable by ordinary mathematical means" (referring to the consistency of PA, not the inconsistency).
ReplyDeleteI'm not convinced, as he seems to have in mind a proof of consistency by means of the existence of a model, whereas obviously what we are talking about when discussing Goedel, Gentzen etc., is a proof-theoretical proof within a particular formal system. So I'd say 'trivially' doesn't apply to the latter cases. But maybe I'm missing something.
Oops, forgot the link to Chow's post:
ReplyDeletehttp://www.cs.nyu.edu/pipermail/fom/2011-May/015490.html
Hi Catarina,
ReplyDeleteThe formal system Q + Con(PA) proves the consistency of PA - so, it's easy to find a formal system F which proves Con(PA). (I can (informally) show that F is itself sound - and therefore consistent!). So, I think the discussion is not about where Con(PA) is provable-in-F for some formal system F. The discussion is about provability in the ordinary epistemological sense - demonstrating that something is so. Or, equivalently, whether Con(PA) is a theorem of some F we *accept* as sound.
Like Tim, I entirely agree that one can demonstrate the consistency of PA by pointing out that PA is sound (and this is a perfectly ok mathematical argument).
I took the discussion not to be whether there is some system F (whatever system) that proves Con(PA), as we already have several proofs of Con(PA) in all kinds of systems, including Gentzen's PRA+. Rather, the question may be, given a *specific* system F, can we prove Con(PA) in it? This question, relative to specific systems F, may well be non-trivial in some of these cases.
ReplyDeletePersonally, I find many of the proofs of the consistency of PA in particular systems entirely compelling (in an absolute sense, 'that something is so' to quote Jeff), because many of them are based on very 'thin', plausible assumptions. So in that sense I join those who think that, in an 'absolute' sense, the consistency of PA is NOT an open question; PA is consistent, period.
But at the risk of sounding annoying, how do we know (for sure!) that PA is sound, without relying on its consistency? :)
Just a quick, very vague thought: I suspect there are some very subtle issues involving the distinction between what we find mathematically compelling (i.e. what sorts of proofs would be taken by the relevant mathematically informed community of practicioners to be convincing proofs) and what we ought to find mathematically compelling. I suspect that any disagreement over the simple model-theoretic argument stems from this sort of deeper disagreement. The proof is obviously compelling in the former sense, but given its reliance on the soundness of first-order logic (which takes some arithmetic to prove), it might not be compelling in the second sense.
ReplyDeleteCatarina, "Rather, the question may be, given a *specific* system F, can we prove Con(PA) in it? This question, relative to specific systems F, may well be non-trivial in some of these cases."
ReplyDeleteYes, but in practice the systems weaker than PA (e.g., the subsystems ISigma_n and things with no induction) don't, unless we do something funny with induction or add Con(PA) (or an equivalent) by hand. And the usual proper extensions of PA (i.e., systems of second-order arithmetic) are always set up so that one can define Tr(x) and prove "All theorems of PA are true". E.g., predicative comprehension (ACA) allows this.
"But at the risk of sounding annoying, how do we know (for sure!) that PA is sound, without relying on its consistency?"
Nah - it's not annoying! It's easy to prove that PA is sound: all of its axioms are true, and the rules of inference preserve truth. Consistency doesn't help at all!
But I need to add that I'm a fallibilist about all claims, and therefore agree with Hume and Popper: we know nothing for sure. But we do know things. So, "know for sure" and "know" aren't equivalent. In particular, "A knows that p" doesn't imply "A cannot doubt that p". I can't rule out that the sun won't rise tomorrow or even that I have a body and am sitting typing on a computer. So, the criterion "can it be ruled out that p?" is too strong a condition on knowledge.
Roy, "The proof is obviously compelling in the former sense, but given its reliance on the soundness of first-order logic (which takes some arithmetic to prove), it might not be compelling in the second sense."
ReplyDeleteYes, maybe that's along the right lines. The average mathematician, who doesn't work in logic, might feel that something a bit 'odd' is going on here (models, truth, derivations and whatnot).
Catarina, "So in that sense I join those who think that, in an 'absolute' sense, the consistency of PA is NOT an open question; PA is consistent, period."
ReplyDeleteYes, all things considered, someone who gets the main background here and isn't a generic sceptic has:
(i) good reasons to assert "PA is consistent".
(ii) good reasons to assert "It cannot be absolutely ruled out that PA is not consistent".
Some people might find this situation incoherent! How can we assert that PA is consistent unless we can *rule out* that PA is inconsistent? Surely in mathematics we can't assert A unless we've ruled out ~A?
Jeff,
ReplyDeleteI think you hit the nail right on the head here. Another way of putting the point (or a similar point, at least) is that knowledge outstrips proof (as is evident to anyone that thinks we have genuine knowledge outside mathematics). Knowledge requires (among other things) a certain kind of warrant (or some such), whereas proof requires a much more specific kind of warrant (a proof, of course). So we can know that a mathematical claim is true without there being a proof of that claim. Thus, proof implies knowledge, but not vice versa.
I think this might provide a fruitful way of understanding what is going on here. If we adopt a very strict sense of 'proof', where we have a proof of P if and only if we can prove P based on assumptions that are no more in doubt than P itself, say, then the situation might be described as follows (when I am talking about a derivation that doesn't necessarily meet this strict understanding of "proof" in what follows I will use the term "pruf"):
(a) We know Con(PA).
Why? Well, look at all the different 'prufs' of Con(PA) listed by Harvey Friedman in his correspondence with Voevodsky. If Con(PA) were false, then most of basic mathematics would also be faulty. But that seems highly unlikely, and this - plus maybe the informal model-theoretic argument - provides a sufficient warrant for knowledge that Con(PA).
(b) We can prove that we can't prove Con(PA).
This is, I think (on a chariatable interpretation), Voevodsky's understanding of Goedel's thoerem (obviously, this is still too loose, as the discussion of proofs of Con(PA) in systems that are 'incomparable' to PA makes clear, but for the moment we can grant this understanding of Goedel's theorem to Voevodsky).
These two claims are not incoherent at all, however. Consider a formal system consisting of PA supplemented with a knowledge operator "K" satisfying the S4 axioms and:
K(F) -> Pr(F)
Such a system cannot have any theorems of the form:
K(P) & Pr(~PR(F))
[since the theoremhood of K(F) would entail the theoremhood of F would entail the theoremhood of Pr(F) would entail the theoremhood of Pr(Pr(F)), rendering Pr(x) trivial]
But there don't seem to be reasons for thinking that there are not unprovable truths of that form in such a system (in fact, I would be surprised if we CAN'T obtain one as a clever Goedel-style fixed point in such a system - I will have to take a look at Stu Shapiro's old anthology on this stuff to be sure, however).
So perhaps this is what Voevodsky should have said:
We know that PA is consistent, but we also can prove that we can't prove that PA is consistent.
(On the aforementioned strict understanding of "proof").
Oh wow. The formula linking "K" and "Pr" should be:
ReplyDeletePR(F) -> K(F)
not:
K(F) -> Pr(F).
A particularly embarrassing gaffe, given my complaints about other people's sloppiness! (After all, the whole point of this is that knowledge DOESN'T in general entail provability!) Apologies.