I have a (somewhat tangential) awareness of the "ordinary" statements that use strong assumptions/non-consructive reasonsing, but (perhaps somewhat naively) imagine that one can still "quarantine off" explicit/constructive versions at least of the "ordinary" statements that come up in my own work. E.g. although I always use the result that a non-zero ring has a non-empty Spec (which relies on choice), I don't imagine that it actually requires choice when applied to the contexts in which I am using it (e.g. Diophantine problems). Now this really is a naive view-point, because there is surely no constructive account of the kind of algebraic geometry that is used in modern Diophantine theory. (Witness the fact that it seems to be currently unknown exactly what sort of foundations are really required for the proof of FLT.) Nevertheless, when it comes to considering something like Con(PA), such naively imagined quarantining is not possible by the very nature of the problem, and so certainly it puts my hackles up!

Best wishes,

Matthew

Anyway, perhaps you are happier with the second answer I gave, which was written with the benefit of some data about what kinds of confusions the people following the thread were suffering from.

I have discussed these issues in other comments here and on the MO posting, and I may be harping on the issue somewhat, but it is not just that foundational questions focus attention on the precise logical background. It is that facts such as the Chinese Remainder Theorem, or the irrationality of the square-root of two, admit constructive proofs. Furthermore, very many results in non-foundational mathematics also admit constructive proofs. (Even if the given proofs are not constructive, constructive versions are not so hard to find.) This separates them from problems such as Con(PA), which by its very nature seems to be non-constructive (at least, the proofs in the affirmative are non-constructive; a proof in the negative could of course just involve explicitly constructing a contradicition).

Thus I think it is misleading to suggest that moth mathematicians accept Con(ZF) or Con(ZFC) in their work, and hence should automatically accept Con(PA); they use ZF(C) as a framework, since this is what prevails. But I believe a large amount of everyday non-foundational mathematics truly is independent of the background set-theory. (E.g. I use homological methods all the time, including sheaves, injective resolutions, etc. The way the foundations of these are set up, they typically involve a lot of apparent set-theoretic power, since one is choosing resolutions all over the place, maps between them, natural transformations between functors, etc. But I don't for a minute believe that all that set-theoretic power is actually required to derive the conclusions one draws --- e.g. FLT. It is just a convenient language.) The issue with Con(PA), compared to another problem, such as FLT, is that it exactly requires to contemplate the most nonconstructive aspects of the theory, and ask whether those give any problems. This gives it a metaphysical nature (if I can use the word) which is not present in more workaday problems.

Best wishes,

Matthew

If I posted the question here is because it was about math, relevant to math, and in a level that is not too elementary (perhaps). The vague discussion on the internet is ideal for this question, which is a question that concerns every mathematician.

The fact that vague discussion is ideal for this question is precisely why it is not ideal for MO, which does not do well with vague discussions.

However, the trouble is that assertions that in any other mathematical context would be accepted as proven mathematical facts are, for some reason, challenged brashly at every step in the context of discussing the consistency of PA.

I don't know if this is how anyone else thinks about it, but this is how I think about it. When I accept a particular mathematical argument in an ordinary context, I'm not necessarily agreeing that I think the mathematical facts used in that argument are consistent. Rather, I only have to agree that the length of the shortest proof of a contradiction which uses some form of the mathematical facts used in that argument is so long that human mathematicians will never reach it before the end of the universe (hence it cannot affect the truth value of any mathematics we do until then). But when I am discussing consistency, it seems appropriate to actually discuss consistency rather than this form of "practical" consistency.

@franklin: I've spent quite a lot of time over the past 20 years trying to explain these kinds of issues, and I think that it is very hard to give a succinct answer that will satisfy everybody. Normally, the way one would proceed is to present the basic mathematical facts so that everyone is at least minimally educated about the subject. However, the trouble is that assertions that in any other mathematical context would be accepted as proven mathematical facts are, for some reason, challenged brashly at every step in the context of discussing the consistency of PA. The Bolzano-Weierstrass theorem would be accepted as a proven theorem in the context of answering any other question on MO, but here, we can almost guarantee that someone will raise an objection. (Even the implication "B-W implies Con(PA)", which is provable in RCA_0, got challenged by Sergey; an RCA_0 argument would never get challenged in any ordinary mathematical context.) Nor can one always predict what kind of objection will be raised, because there are all kinds of different kinds of objections possible. It's hard to operate in such an environment. Even if I figure out what a particular person needs to hear, it's hard to communicate that on a forum like MO, where someone else may interject with some comment that derails the discussion. Anyway, I'm glad that you seem to have found some sort of answer to your questions.

I think that your final sentence may be a little uncharitable to Voevodsky. He certainly wouldn't be the only mathematician to embrace a strong form of constructivism, and I imagine a strict enough constructivist would reject the general form of Bolzano--Weierstrass being discussed here; i.e. that they would restrict its validity to sequences of rationals that are constructible in some suitable sense, and would then want to produce the Cauchy subsequence via some constructive process. (Does this sound correct?) In any case, to say that "there is nothing in Goedel's theorem that suggests that all foundational systems will admit Russell-type paradoxes" seems to be somewhat subjective; it obviously suggested this to Voevodsky, even if to no-one else. Personally, I believe (or live my life as if I believe, which doubtless amounts to the same thing) that N and all its possible subsets exist, and hence believe that PA is consistent. But I can certainly see why this would not be convincing to a (sufficiently strict) constructivist.

Best wishes,

Matthew

Every bounded sequence of rationals contains a subsequence such that for this subsequence for all n one has |q_i - q_j| < 1/n for i,j > n.

There is nothing in Goedel's theorems that suggests that there must be a counterexample to this assertion. I think this is just one more example of someone (Voevodsky in this case) drawing conclusions without being properly educated about the relevant facts.

I think that there is an extra issue at work here, though, which you are eliding slightly in your discussion. Namely, the cases of comprehension that are used in normal mathematical argument (e.g. the cases of comprehension that Voevodsky will have ever used) are much simpler than the much more general instances of comprehension that appear in formal theories such as ZF(C) or even in PA (if we interpret formulas in PA as giving subsets of N).

As far as I can tell, Voevodsky believes that Russell's paradox, and then Goedel's theorem (which, I think it is fair to say, is not unrelated to Russel's paradox) are pointing us towards the fact that all foundational systems will admit Russell-type paradoxes, and so are all inconsistent. Indeed, he says as much in his lecture. My impression is that he believes that every day mathematical results survive these paradoxes because they don't actually use the general comprehension axioms that appear in foundational systems. (So I think in practice this could mean rejecting statements about "every differentiable function", but replacing them by suitably constructive variants. Of course, I don't want to put words in his or anybody else's mouth, but I do note that he makes it clear in the question-and-answer section of his lecture, while answering a question of Witten, that he rejects the standard axiomatization of the real numbers.)

Regards,

Matthew

The question of whether PA is consistent is certainly a mathematical question and is not subjective and argumentative. The real question, however, appears to be why people keep arguing about it. This latter question is not a mathematical question and in my view is subjective and argumentative. So I voted to close.

I believe I can partially answer the question of why the question continues to generate debate. One of the main reasons is that a lot of people simply don't understand some of the basic facts and therefore get confused. For example, many people accept, or at least give lip service to, the statement that "if a proof can be formalized in ZF then it is an acceptable mathematical proof and settles the matter definitively." By this standard, the consistency of PA is settled. It's a theorem of ZF, and quite an easy theorem at that, as I sketched in my answer on MO. Formalizing this proof in, say, Mizar would be a routine matter. Moreover, nothing like the full power of ZF is needed. As Friedman notes, one can come up with extremely innocuous mathematical statements whose proofs nobody would normally question, and show that they directly imply the consistency of PA, on the basis of an extremely weak logical system. For virtually any other mathematical statement, all this would be far more than enough to settle the question of whether it's a proved theorem.

Now, even after acquainting themselves with the above facts, some people still feel uneasy about the status of "PA is consistent." Why is this? I believe that part of it is a poorly articulated gut feeling that there is something "circular" about the trivial proof I sketched. There is, of course, nothing incorrect about the proof, or Mizar would complain. Nevertheless, some people get the feeling that exhibiting N, the natural numbers, in order to prove the consistency of PA is "circular." Part of this again stems from ignorance of basic facts; many people don't understand that there is a difference between PA, which posits induction on first-order properties only, and what are often called the "second-order Peano axioms," which are sometimes taken to be a definition of N. Thus they think that PA is being used as a proposed definition of N, and that it makes no sense to then appeal to the existence of N to establish the consistency of PA.

Further confusion results when people decide that to really convince themselves that PA is consistent, they must back off from assuming anything that has the slightest whiff of assuming the existence of N, and try to bootstrap their way up. When doing so, they typically don't realize that they're throwing out a huge baby (i.e., much of ordinary mathematics) with the bathwater; again, this is usually due to lack of experience with foundational reasoning. They then notice that they can't seem to bootstrap themselves back up, and start to worry that maybe the consistency of PA can't be proved after all.

Once you get yourself into this mess, it's easy to get totally confused. You've now suspended your usual mathematical intuition and so aren't sure which way is up any more. You will probably fail to notice that if you really want to back off from assuming the existence of anything that remotely resembles N, then you should also back off from assuming the existence of PA. What is PA, anyway? Doesn't the definition of PA presuppose that it's meaningful to talk about the infinite sequence of strings "0, S0, SS0, SSS0, ..."? How is an infinite sequence of strings any less suspect than N itself?

Now, it is possible to adopt a philosophical position that is generally called "ultrafinitism," whereby one does indeed systematically reject any infinitary assumptions. For the ultrafinitist, "PA is consistent" is a meaningful statement but not proven. The ultrafinitist, however, rejects most mathematical statements, such as "every differentiable function is continuous," as meaningless; only statements such as "the statement that every differentiable function is continuous is provable in ZF" are considered meaningful. So, you could side with the ultrafinitist and declare that the consistency of PA is an open problem, but by doing so you would be taking a minority philosophical position. In this sense, whether the consistency of PA is an open problem is a philosophical issue; but note that in this sense, whether any ordinary mathematical statement makes sense at all is also a philosophical issue.

Hopefully this sketch of some of the issues will show that "PA is consistent" is not an open mathematical problem in any usual sense of the term. People who assert that it is are usually implicitly taking some kind of nonstandard philosophical position and changing the rules of what constitutes an open problem.

Thank you for your answer. What you suggest seems no doubt like a reasonable point of view.

Best wishes.

At this point I am speculating (since Voevodsky hasn't yet answered Friedman's question), but I presume that he will reject statement (1), or rather, will accept as valid only a more limited, sufficiently constructive version of (1). If one takes a formula of PA which determines a non-constructive subset of the naturals (one whose existence Voevodsky rejects), and then takes the corresponding sequence of rationals, one gets a sequence of rationals tending to zero, which I imagine could arise as a candiate sequence q_n in (1). Or alternatively, one could imagine some sequence of rationals such that the subsequence predicted by (1) has indices i which are precisely determined by the condition of belonging to this subset. I would guess that some version of these sorts of constructions is taking place in Friedman's proof relating (1) to consistency of PA.

Note that in the question and answer part of the video, Voevodsky makes it pretty clear that he doesn't really believe in the current formalization of the real numbers (calling them an "overidealization") and so it wouldn't surprise me at all if he rejected (1).

Regards,

Matthew

regarding your suggested answer I am not sure this really solves the problem. If I understand Friedman (in his correspondence with Voevodsky) correctly what, Friedman would like to know from Voevodsky is precisely whether he (V.) really wishes to take such a strong constructivist point of view (that is necessary to maintain that the consitency of PA is open), and (paraphrasing) for example 'deny' that:

(1) every bounded sequence of rationals contains a subsequence such that for this subsequence for all n one has |q_i - q_j| < 1/n for i,j > n

(cf. the very end of the correspondence F-V here http://www.cs.nyu.edu/pipermail/fom/2011-May/015506.html).

And, again if I understand correctly, the situtation is like this:

a. 'I doubt (1) and the consitency of PA' or b. 'I do not doubt (1) and the consitency of PA is proved' are both reasoanble opinions. Yet c. 'of course (1) is true but still I doubt the consitency of PA' is not.

[Except perhaps, based on my limited understanding, if ones opinion is that for (1) 'usual mathematics' standards suffice whereas for con PA one needs 'formal reasoning' standards, which then leads to the question whether or not this opinion is reasonable.]

And the question (to V.) is a long the lines: do you really believe a., and if not please clarify your opinion [which according to the linked correspondence was not yet answered, but an answer was deferred to a later point in time]. So, what I want to say is that your assertion '(as Voevodsky is doing)' is what somehow seems to be the question.

ps. I appologize in advance if I got something wrong; but this discussion lead me to now (also) be really interested in what is going on, and this is still not completely clear to me.

First, the question is asked not in isolation, but in the context of a lecture by Voevodsky. This can (and probably should) inform the answer.

Now, as Timothy Chow notes in his answer on MO (and in his posts on the FOM mailing list), if one accepts the existence of the natural numbers, and of arbitrary subsets of the natural numbers, then one can prove that PA is consistent, by exhibiting its standard model, namely the natural numbers. In short, if you believe in the existence of the natural numbers with their usual properties, and you believe that any formula in PA defines in a meaningful way a subset of them, then you will be forced to believe in the consistency of PA.

On the other hand, listening to Voevodsky's lecture, it seems clear that while he is not rejecting the existence of the natural numbers (as perhaps some extreme finitists do), he does not believe that a general formula in PA defines a meaningful subset of the natural numbers. Thus the standard model argument does not convince him, and in fact he seriously entertains the idea that PA may be inconsistent.

On the FOM list there are various assertions that Voevodsky's position is inconsistent, because he has surely proved, and accepted as proved, more elaborate results than the consistency of PA. This is not clear to me, and it seems that a careful analysis of the situation may be somewhat analogous to the analogous analysis of whether large cardinals are required for the proof of FLT --- see this MO question; that is, what might be deduced by a naive analysis of the theories involved, which would suggest that a lot of strong foundational principles are required for A^1-homotopy and so on, could be misleading upon a more careful investigation. Indeed, it seems quite possible to me that all the arguments that Voevodksy has ever made or signed off on as a referee involve much less comprehension than is required to believe that an arbitrary formula in PA defines a subset of the natural numbers. (The point being that his mathematics will only ever have involved comprehension for rather particular formulas, which are presumably much more concrete than a "general" formula of PA.)

Again, listening to Voevodsky's lecture, it is clear that he makes a careful distinction between mathematical reasoning as carried out by mathematicians, and formal reasoning. Indeed, he seriously entertains the idea that there may not be formally consistent foundations, but at the same time is not rejecting usual mathematics in any sense. Rather, he makes it clear that he believes that the kind of unrestricted nature of constructions required in setting up foundations (e.g. allowing arbitrary formulas in PA to define subsets of the naturals) are likely to always lead to contradictions; but at the same time, he believes that "actual" mathematics will not be affected by this (although a new viewpoint on foundations would be required, a viewpoint that I believe he and his collaborators are actively developing).

So he draws a very strong distinction between "practical" or "natural" mathematical reasoning, and its formalization in a formal system such as PA or ZFC. He seems to believe that Russel-type paradoxes arising from unresricted comprehension will appear in essentially any foundational system, and his rejection of comprehension even over arbitrary formulas of PA seems to me to be a very strong constructivist position (and I hope I'm using this adjective in some approximately correct sense).

So I think the answer to the question should be something like: the consistency of PA can be easily proved using commonly accepted mathematical notions, but not if one limits oneself to sufficiently constructivist notions (as Voevodsky is doing).

This naturally raises the question of how far you can go down this road. This is nontrivial, since weakening the axioms lets you add proof principles which would be inconsistent in the stronger theory. For example, Terui's light affine set theory is only strong enough prove that polytime functions are functions, but on the other hand it consistently allows the unrestricted comprehension principle!

On the FOM list, Voevodsky mentions that he regards the consistency of PA as a settled question (Godel ruled out a solution), but he regards its in-consistency as an open problem. This formulation is clearly designed to provoke, but hopefully the example of light set theory should suggest that there is real meat to his question.

Not quite. The formal background is actually a modified version of dependent type theory.

@franklin: foundations often exerts a kind of religious fascination, but I wouldn't say everyone gets so riled up about it!