Is PA consistent? do we know it?

1) (By Goedel's) One can not prove, in PA, a formula that can be interpreted to express the consistency of PA. (Hopefully I said it right. Specialists correct me, please). 2) There are proofs (although for the purpose of this question I should putt it in quotations marks) of the consistency of PA.

The questions are: A) Is it the consistency of PA still a mathematical question that can be considered open? B) Is it a mathematical question? (To this I dare to say that it is a mathematical question. Goedel himself translated it into a specific formula, but then I have question C) C) Is it accepting the proofs of the consistency of PA as conclusive a mathematically justified act or an act of taking a philosophical stance?

Motivation: There is a discussion in the mailing list FOM (Foundations Of Mathematics) about this topic, in part motivated by this talk link text . I thought a discussion about this fundamental matter concerns most mathematicians and wanted to bring it to a wider audience.

Edit: It is simple. Either: 1) Consistency of PA is proved and has a proof (as claimed by some in FOM) as valid as any other theorem in math, or 2) On top of the existing proofs a philosophic choice is needed (which explains the length of the discussions in FOM, justifies closing this question but contradicts what is being claimed emphatically by some in FOM)

But you see. If 1) is the case then there is no need for the lengthy discussions and this is a concrete math question as any other, terminating with a proof.

........................................................................................

Edit 2: Thank you all. Although I had seen some of these arguments at FOM now I think I have my ideas more organized and I can make my question more concrete. I would like to try to put aside what involves 'believes'. In, I think, all the answers shown there has been this action entering the argument quite soon, e.g. In Chow's: (approx.) If you believe in the existence of the naturals then con(PA) follows. In Friedman's (approx.) If you believe in (About a dozen Basic axioms) + (1/n subsequences) then con(PA) follows.

I want to put aside that initial action because (1): It is a philosophical question and that is not what I want to discuss, (2): Because of: If I believe (propositional logic) + (p/-p) then I believe ... for example (everything you can say) and maybe (3): Because I, personally, don't do math to believe what I prove. When I show P->Q, in a sequence of self imposed constrained steps I don't do it with the purpose of showing that, and at the end I don't have a complete conviction that, Q is a property of whatever could be a real world. But that is just philosophy and philosophy allows for any sort of choices. That is why I want to put it aside, at least until the moment in which it is inevitably needed.

My question is: Is any of the systems that prove con(PA) a system that has itself been proven consistent?

Why to ask this question? Regardless of how your feelings are about the ontological nature of what you prove. We can say that, since an inconsistent system proves everything, a consistent system is a bit more interesting for not doing so. At least if it is because there is not always a proof in which you use modus ponens twice (after you have found p/-p) for everything that you want to prove.

I guess that also, to answer the question above, it should be clarified what to accept for a consistency proof. Let's leave it kind of open and just try to delay the need for a philosophic stance as much as possible.

-
Given the rather lengthy debate on FOM, and the fact that MO is not for debates or discussions, I don't know that this question is a good fit. Although if someone posts a contradiction in PA I guess that would give a definite answer... – Steven Gubkin May 26 '11 at 22:42
I have voted to close, even though I think this is an interesting question, because, as Franklin points out, there is extensive and impassioned discussion on a mailing list already, and that is a far better forum than MO for this discussion. – David Roberts May 27 '11 at 0:09
And, in addition, the moderators of FOM has said that he will not post any more mailings about the Con(PA) debate unless they add something new. MO is not the place to continue fruitless discussion. – David Roberts May 27 '11 at 0:23
Especially after reading (Matthew) Emerton's long and cogent message on meta, I've decided to cast the last reopening vote. But I please remind everyone to "keep a civil tongue" -- respond coolly and factually. – Todd Trimble Jun 1 '11 at 11:10
Meta thread is at:  tea.mathoverflow.net/discussion/1057/…  – Will Jagy Jun 1 '11 at 23:15

I have already posted an answer but in light of the discussion and the kinds of confusions that have emerged, I believe that this additional answer will be helpful.

Let us first note that the consistency of PA, or more precisely a certain formalized version of it that I will call "Con(PA)," is a theorem of Zermelo-Fraenkel set theory (ZF). Conceptually, the simplest ZF proof is obtained by formalizing the easy and almost trivial argument that N, the natural numbers, is a model of PA.

ZF is an extremely powerful system, and the full power of ZF is not needed for proving Con(PA). Famously, Gentzen showed that primitive recursive arithmetic (PRA), a very weak system, can prove Con(PA) if you add the ability to do induction up to the countable ordinal $\epsilon_0$. Other ways to prove Con(PA) are available. Let B-W denote the statement that "every bounded sequence of rational numbers contains a subsequence $(q_i)$ such that for all $n$, $|q_i - q_j| < 1/n$ for all $i, j > n$." Then B-W implies Con(PA), and this implication can certainly be proven in the system RCA$_0$, and (according to Harvey Friedman) actually much less than RCA$_0$ is needed.

Most mathematical statements are no longer considered "open problems" once a proof has been published or otherwise made widely available, and checked and confirmed by experts to be correct. Note that published proofs, and expert verification, usually make no explicit reference to any particular underlying formal system such as ZF or PRA. Mathematicians are trained to recognize correct proofs when they see them, even if no set of axioms is explicitly specified. If pressed to specify an axiomatic system, a common choice is ZF, or ZFC (ZF plus the axiom of choice). If a proof is available that is explicitly formalizable in ZF, that is normally regarded as more than sufficient for settling an assertion and removing its "open problem" status.

In the case of Con(PA), the aforementioned "normal conditions" for removing its "open problem" status have been met, and in fact exceeded. Nevertheless, some debate continues over its status, most likely because Con(PA) is widely perceived to be a somewhat unusual mathematical statement, having connections to philosophical questions in the foundations of mathematics. For example, some people, whom I will loosely call "formalists" or "ultrafinitists," maintain that many ordinary mathematical statements (e.g., "every differentiable function is continuous") have no concrete meaning, and the only concrete thing that can be said about them is whether they can or cannot be proved in this or that formal system; however, a statement such as "PA is consistent" is regarded as having a direct, concrete meaning. Roughly speaking this is because "PA is inconsistent," unlike infinitary mathematical statements, can be assigned a quasi-physical meaning as the existence of a certain finite sequence of symbols that we can physically apprehend. While the formalist agrees with all the above facts about the provability of Con(PA) in this or that formal system, such formal proofs don't necessarily carry any weight with the formalist as far as establishing the consistency of PA (in what I've called the "quasi-physical" sense) goes. Formalists will generally agree that explicitly exhibiting a contradiction in PA will definitively establish its inconsistency, but may differ regarding what, if anything, would definitively establish its consistency.

There are others who are not formalists but who reject the commonly accepted standard of ZF(C) and only accept proofs that are formalizable in much weaker systems. For example, someone with strong constructivist leanings might only accept proofs that are formalizable in RCA$_0$. For such a person, the proof of Con(PA) in ZF carries no weight. Roughly speaking, the usual ZF proof, that proceeds by showing that N is a model of the axioms of PA, assumes that any first-order formula defines a set of natural numbers, and this assumption is unprovable on the basis of RCA$_0$ alone. In fact, one can prove that Con(PA) is unprovable in RCA$_0$. Such a person might regard the consistency of PA as permanently unknowable (in a way similar to those who regard the continuum hypothesis as permanently unknowable since it has been proved independent of ZFC). Note, by the way, that this person would also regard a sizable portion of generally-accepted mathematics (including Brouwer's fixed-point theorem, the Bolzano-Weierstrass theorem, etc.) as being "unproved" or "unprovable."

To summarize, the consistency of PA is not an open problem in the usual sense of the term "open problem." Some people do nevertheless assert that it is an open problem, or that it has not been proven. When you encounter such an assertion, you should be aware that most likely, the person is using the term "open problem" in a somewhat nonstandard fashion, and/or holds to certain standards of proof that are more stringent than those that are commonly accepted in the mathematical community.

Finally, to answer the new question that Franklin has asked, about whether the consistency of any of the systems in which Con(PA) has been proved has been proved: The answer is, "not in any sense that you would likely find satisfying." For example, one can "prove" that PRA + induction up to $\epsilon_0$ is consistent, in the sense that the consistency proof can be formalized in ZF, which as I said above is the usual standard for settling mathematical questions. If, however, the reason that you're asking the question is that you doubt the consistency of PA, and are hoping that you can settle those doubts by proving the consistency of PA in some "weaker" system that can then be proved consistent using "weaker" assumptions that you don't have any doubts about, then you're basically out of luck. This, roughly speaking, was Hilbert's program for eliminating doubts about the consistency of infinitary set theory. The hope was that one could prove the consistency of (say) ZF on the basis of a weak system such as (say) PRA, about which we had no doubts. But Goedel showed that not only is this impossible, but even if we allow all of ZF into our arsenal, we still can't prove the consistency of ZF. For better or for worse, this tempting road out of skepticism about consistency is intrinsically blocked.

-
wow! thank you. – Mlazhinka Shung Gronzalez LeWy Jun 3 '11 at 3:06
Following up on the last paragraph: this is in no way unique to Con(PA). We know in an informal and somewhat trivial way that "to prove a theorem you have to make assumptions at least as strong as the conclusion." This is reflected formally in the Lindenbaum algebra of each formal theory. It is reflected philosophically in the debate whether mathematical truth is analytic. In this sense every mathematical proof (of a non-logical validity) is circular. This is noticed most often in the context of consistency proofs but I do not see them as special in this way. – Carl Mummert Jun 3 '11 at 12:50
"(according to Harvey Friedman) actually much less than RCA0 is needed." Can someone ask him to please write this down/up? This is too interesting a result to lurk as claims in fom postings and as hearsay by others in other internet forums. – David Roberts Jun 30 '15 at 0:54
In FOM posts cs.nyu.edu/pipermail/fom/2015-May/018744.html and cs.nyu.edu/pipermail/fom/2015-May/018752.html Friedman has said that he has the best of intentions to write this stuff up Real Soon Now. – Timothy Chow Jun 30 '15 at 14:54

As Mirco Mannucci's answer suggests, the alternatives labeled 1) and 2) in the question are (for some people) not mutually exclusive. The consistency of PA indeed "has a proof as valid as any other theorem in math" (as Timothy Chow's answer pretty much shows) --- alternative 1. Nevertheless, if one doesn't believe the integers exist, then the bottom drops out from that and also from almost everything else in math. So to be really convinced by the proof, one makes a philosophical choice to accept the existence of integers and the meaningfulness of quantification over them. What strikes me as strange is that people who have made that choice (or at least act as if they had made it) and are perfectly content with theorems that rely on the availability not just of integers but of far more complex entities (real numbers, sets thereof, etc.) suddenly develop philosophical qualms about such reliance when used to prove the consistency of PA.

Let me also comment on Gentzen's proof. Note that Timothy didn't invoke that argument but gave instead a much more natural and understandable proof. So what is Gentzen's proof good for? As far as I can see, its primary value from a philosophical point of view is that it can be used if one doesn't accept arbitrary first-order sentences about the integers (with possibly lots of quantifiers) as meaningful. The induction axiom scheme of PA says that such sentences can be proved by induction (ordinary induction on natural numbers), which is true but presupposes that these sentences are meaningful. Gentzen's proof uses induction on ordinal numbers up to $\varepsilon_0$ but only to prove very simple, finitary statements. (His proof can be formalized in the system PRA of primitive recursive arithmetic plus the assumption that there is no primitive recursive decreasing sequence of ordinals below $\varepsilon_0$.) The upshot is that there's a trade-off: If you want to prove the consistency of PA by induction on only extremely simple statements, then you need a long induction, of length $\varepsilon_0$.

-
Andreas, yes, if someone doubts that natural numbers exist, almost everything else in math also drops out, at least as far as ontological beliefs go. But that does not mean that the skeptic fellow will stop loving and/or doing math, or worse, act as a censor and try to obliterate some of its branches, such as for instance set theory. I do not believe in the number 5, yet I am fascinated by the theory of extremely large cardinals. To me, that is another gorgeous game with precise syntactic rules, and some folks play it well and build excellent works of art in Cantor paradise – Mirco A. Mannucci May 27 '11 at 12:10
"...suddenly develop philosophical qualms..." So you don't suddenly develop an increased attention to rigor when doing math, as opposed to the rest of your daily life. For this reason you never use any medicine (because its action hasn't been proved), never attend seminars (because it hasn't been proved that the talks will run as scheduled), etc. I see. Well, I'm proving my theorems only to better understand world; so I feel comfortable using induction because I'm confident that it's at least very, very close to being true, and any potential problems with PA will not change my proofs too much. – Sergey Melikhov May 31 '11 at 19:53
@Sergey: The position you seem to be defending, being uncertain about mathematics in the same sense (though less intensely) as about "real life", seems coherent to me. What I consider strange, though, is to accept some parts of mathematics (e.g., real analysis) without expressing any doubts, while expressing doubts, based on ontological issues (doubts whether the integers exist), about statements like Con(PA) that seem to require far less ontological commitment than real analysis. The analog in your real-life examples would be someone who is ... (continued in next comment) – Andreas Blass Jun 1 '11 at 12:51
Dear Andreas, Regarding the issue that "strikes [you] as strange": after listening to Voevodsky's lecture, my impression is the following: while he (and most mathematicians) work with concepts much more complex than PA, on the other hand, in practice they only use rather limited examples of comprehension, i.e. the formulas they work with are typically of a very limited kind. Voevodsky's position seems to be a strongly constructivist one, and it is not the level of complexity of objects that he seems to be rejecting, but rather non-constructive assertions about them. I think that ... – Emerton Jun 1 '11 at 13:08
... this point of view might be hard to formalize with standard foundations (because it might be hard to distinguish formally between the concrete formulas which one admits as having a meaning, and the more general formulas which one rejects as meaningless), and this is in part motivating Voevodsky's attempts to develop new foundations. (I am speaking as an interested non-expert here, and I apologize if I'm blundering in my analysis of the situation.) Regards, Matthew – Emerton Jun 1 '11 at 13:11

For some reason, this question generates more confusion than it really should. My belief is that if you understand the question properly, then you should be able to answer it yourself.

So let me ask the following question: Suppose $P(n)$ asserts a mathematical property of the nonnegative integer $n$, and suppose we can prove $P(0)$ and we can also prove that for all $n$, $P(n)$ implies $P(n+1)$. Does $P(n)$ hold for all $n$?

This is just mathematical induction, and the answer is so obviously yes that you must wonder if it's a trick question. But I'm not asking a trick question. The answer is yes.

Now let me ask if a first-order formula in the language of arithmetic (e.g., $\exists y: y+y=x$) defines a mathematical property of the integers. Again, the answer is so obviously yes that you must wonder if it's a trick question. But it's not a trick question. The answer is yes.

If you're with me so far, then you have just agreed that PA is consistent. You should now be able to ask yourself, did you make any philosophical assumptions just now? Is the validity of mathematical induction a philosophical question or a mathematical one? If it's a mathematical question, is it still an open problem?

-
There is something I didn't understand. Answering yes to both questions is the act of assuming induction (taking it as an axiom and using it). How does that answer the question of whether taking different P's and using induction with them you never get the formula Q/\-Q for some Q? Making a set (an entity that encapsulates in some way) all the elements satisfying a property is as intuitively obvious and acceptable as assuming induction, except for the fact that if you do it carelessly it is not difficult to create Q/\-Q. (continued in a second comment) – Mlazhinka Shung Gronzalez LeWy May 26 '11 at 23:42
Now, Gentzen's proof, or any other. Very naively, induction up to $\epsilon_0$ implies Con(PA). But again, if from assuming that induction you can get Q/\-Q then you can get anything and in particular Con(PA). That is why I don't understand in what sense is that a proof. It is indeed a proof that induction up to $\epsilon_0$ implies Con(PA) but to get Con(PA) you have to get settle down the induction first. What I get from the discussion is that something is wrong in what I said. What is it I would like to know? – Mlazhinka Shung Gronzalez LeWy May 26 '11 at 23:48
The question of whether every formula with one free variable determines a property is exactly what has to be proved. The failure of this is exactly what goes wrong in naive set theory with expressions such as $\{ x: x \not \in x\}$. However, we have two completely different proofs of consistency: Gentzen's and Goedel's. These show that, in fact, formulas of PA do determine sensible predicates, at least in the sense that the axiom scheme of induction is consistent. – Carl Mummert May 27 '11 at 1:45
The failure of formulas to do sensible things is also what enables Curry's paradox that shows that certain type theories stronger than PA are inconsistent. It seems odd, but somehow the second-order induction axiom seems less worrisome in this way than the first-order axiom scheme. – Carl Mummert May 27 '11 at 1:53
@Franklin: Your definition of proof runs counter to normal mathematical standards for proof. E.g., mathematicians regard it as proved (not an open problem) that every differentiable function is continuous, even though there's no way to "experimentally check" an uncountable number of differentiable functions at uncountably many points for continuity. By normal mathematical standards, PA is provably consistent. You can of course introduce unconventional philosophical standards and declare that the consistency of PA is an open problem, but then you shouldn't be surprised if people argue with you. – Timothy Chow May 30 '11 at 22:18

Here is an attempt to answer the question that I posted on the meta discussion, and which I am reposting here now that the question has been reopened. [Note: I am a non-expert with an interest in foundational issues, and I am doing my best to understand the situation. I hope that my lack of technical expertise in the area has not led to too many stupidities, and welcome any such being pointed out.]

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

Now, as Timothy Chow notes in his answer here (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 $\mathbb 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).

[The next part of my answer is based on an exchange with an_mo_user on the meta discussion.]

On the FOM mailing list, Friedman posted some correspondence with Voevodsky, in which Friedman explain that the consistency of PA follows from fifteen (if I remember correctly) generally accepted mathematical principles together with the following statement:

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

He then asks for Voevodsky's reaction to this: does he continue to maintain that PA is inconsistent, and (hence) reject (1), or does he have some different position?

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 (probably much more sophisticated) 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).

-
You're right about (1) -- it is a slightly disguised form of the Bolzano-Weierstrass Theorem. Over the base system $RCA_0$ of second-order arithmetic, this statement is equivalent to arithmetic comprehension $ACA_0$ (i.e. all arithmetical formulas define a set of natural numbers). Another option to completely rejecting (1), is to reject the possibility of iterating (1) arbitrarily often. Indeed, when applied to computable sequences of rationals, (1) only allows the comprehension of sets with Turing degree $\leq 0'$, so one needs to iterate (1) a lot in order to get all arithmetical sets... – François G. Dorais Jun 1 '11 at 14:34
... However, I have yet to see a sensible formulation of "not being able to iterate" in this and similar contexts. – François G. Dorais Jun 1 '11 at 14:36
I think Harvey Friedman's claim was somewhat stronger, in that he doesn't assume the base theory $RCA_0$. Instead, he says he relies on some very basic mathematical (meaning not looking like logic or set theory) facts. This is an aspect of what he calls strict reverse mathematics, and it may well be relevant in the present context, since Voevodsky might reject $RCA_0$. – Andreas Blass Jun 1 '11 at 15:15
@Andreas: Thanks for the precision. @Sergey: You may find these drafts by Friedman of interest: math.osu.edu/~friedman/pdf/StrictRM012305.pdf math.osu.edu/~friedman/pdf/InevLogStr082907.pdf math.osu.edu/~friedman/pdf/StrictRevMath110709.08.pdf – François G. Dorais Jun 2 '11 at 22:50
François: thanks for the links. Andreas: It's not clear to me if the role of Strict RM in this context would be to reveal essential "facts" being used or rather to hide those ones revealed by ordinary RM behind a heavy ideology. In François' last link, under "Strict RCA$_0$" there is the following disguised form of second-order induction axiom: "every sequence [of integers] has a term of least magnitude" (and also some obscure "extensionality for sequences"). – Sergey Melikhov Jun 4 '11 at 20:01

I am a little baffled by some of this discussion. It seems everyone agrees that consistency of PA is a theorem, if you accept some stronger system, such as ZFC. So, PA is consistent relative to ZFC. Just as obviously, you need something to prove consistency of PA; it could be $RCA_0$ plus some presumably innocuous-looking axiom, but obviously $Con(PA)$ doesn't come for free.

Where it gets baffling to me is where the words like "believe", "suspicious", "doubts", etc. enter the discussion; those words properly belong to philosophy. If you take a platonist line, then you may be fairly asked what you "believe", and under those circumstances there is a kind of conventional belief that ZFC is simply true. But if you take a formalist line, then there is no commitment to belief; you just take some set of axioms and merrily apply first-order logic$^1$. (But if you are honest about that, then of course you declare what axiom system your theorems are relative to.)

For instance, what Andreas Blass finds "strange, though, is to accept some parts of mathematics (e.g., real analysis) without expressing any doubts, while expressing doubts, based on ontological issues (doubts whether the integers exist), about statements like Con(PA) that seem to require far less ontological commitment than real analysis." It's not clear to me what 'ontological commitment' a skeptic of $Con(PA)$ would have to particular statements of analysis$^2$, but a formalist will have none, and as Emerton points out (in his speculations on Voevodsky's likely reaction to one of Friedman's questions), there are plenty of seemingly innocent-looking analytic statements subject to constructivist 'doubt', if 'doubt' is indeed the right word to use here. (A formalist might prefer to say instead, 'constructively invalid'.) I can't see why any of this would be controversial.

1. First-order logic is a kind of bottom line for most formalists. There are some divergences as to whether one uses the principle of the excluded middle, or whether one treats equality as intensional or extensional -- much of Voevodsky's fascinating recent work is in intensional type theory and what might be termed its "homotopical semantics".

2. If someone is observed not to express doubts about certain analytic statements but express doubts about $Con(PA)$ -- as has no doubt happened in the history of mathematics -- it doesn't necessarily mean that person is confused. It could simply mean that the person has decided to "go along with" ZFC in one discussion -- maybe he is "suspending disbelief" just for the sake of an interesting discussion -- but in another discussion with manifestly metamathematical overtones, he has decided to "reactivate disbelief". Or, maybe he is just being mum about his having or not having beliefs.

-
Dear Todd, I think that one reason for your confusion is that while (I want to guess) you are a formalist, many others are platonists. In particular, I think it is at least a priori possible to imagine that mathematics takes place prior to foundations of mathematics (this is at least historically true), and then it is harder to phrase results as being of a relative nature in a formalist nature; they instead are relative to certain basic beliefs. E.g. I believe that the real number as a complete ordered field exists, and then I deduce xyz about them; I believe that the natural numbers ... – Emerton Jun 2 '11 at 22:27
exist, with all their subsets, and so obtain a model of PA. (But not a model in ZFC; a model in some less formal sense, a mental model if you like.) Perhaps what I want to say is that Platonist beliefs can occur prior to foundational beliefs, so that one can admit certain beliefs without (necessarily) believing in ZFC. In fact, I think that this is close to how many practicing mathematicians work (they may say they believe in ZFC, but I'm not sure that that isn't just a social convention) --- I should say that I don't have anything but anecdotal evidence for this, though, so don't take ... – Emerton Jun 2 '11 at 22:30
... it too seriously as an assertion. So let me close by saying that since I started reading online math forums, and so getting a broader cross-section of mathematical points-of-view than I get in person, I have been surprised at how many formalists there seem to be! (So, while you seem to find the formalist position more natural, and the platonist position perhaps less so, my situation is somewhat the reverse.) Anyway, none of this is meant as any criticism at all of your answer, which I think is very lucid; just as some commentary that might shed light on the aspects of the ... – Emerton Jun 2 '11 at 22:33
Timothy, while I may profess agnosticism about all such matters, I confess that I actually believe Con(PA). :-) I'd not heard the controversy you refer to; do you know some place in the literature where this is discussed? I admit that I'm not too sympathetic to the second of those two positions: it would carry little weight in the disastrous event that a formal deduction in PA of 0 = 1 were actually produced! – Todd Trimble Jun 3 '11 at 1:33
Timothy: (1) I was being serious, and (2) I believe you've made this point several times by now. I'm not sure which formalists you're imputing this behavior to, but I understand the point you're making. At the same time, surely for any theory T, "T is inconsistent" has the direct meaning that there is a deduction of the sequent $\top \vdash \bot$ in T. – Todd Trimble Jun 4 '11 at 1:51

To be specific, I'll focus on the second question of the title, "Is PA consistent? do we know it?"

As noted by Noah Snyder on the meta thread, this question itself already uses "philosophical" language like "know". So I think it may be viewed it as

$\bullet$ a question in mathematics, if you accept a specific philosophical position such a form of platonism, formalism, constructivism, or ultrafinitism; or

$\bullet$ a question in philosophy of mathematics, if you remain ignostic regarding the meaning of "know".

So as to stay on-topic, I will only consider the first possibility, and only those four positions that it explicitly lists. In fact, for a constructivist's view I absolutely support what Emerton said (only I'm not sure about the border between what Voevodsky actually claimed in his talk vs. what he might have meant), and for a formalist's view I agree completely with Todd Trimble's answer. (Indeed, before these two answers appeared I had felt something of those kinds was badly missing from this discussion.) Regarding an ultrafinitist's view, I think Mirco Manucci has a point, and I'll incidentally elaborate on another important point made by Qiaochu Yuan on the meta thread.

So I will now pretend that I'm a platonist (which is what I usually do when attacking some problem - but certainly not when writing up a proof) and in doing so I'll try to argue that Timothy Chow's first answer is simply wrong. ("Wrong" in platonist's absolute, undefinable sense.)

The problem with Timothy's argument is that it unfairly exploits our subconscious reading of some words in a mathematical text.

When I'm stating a theorem, in a paper or in a talk, I almost never put it like "Theorem (ZFC)." or "Assume ZFC. Then ..." because my area of geometric topology is (or at least is commonly thought to be) very far from foundations, and such pronouncements, commonly seen as tautological, would be very distracting. But I do mean it. (Not that I like ZFC too much, especially so with the uncountable "C" which strikes me as really awful in the context of ZF. But I recognize that socially and in terms of the existing literature to refer to, I don't have much choice - so all my results are, alas, meant to be in ZFC by default.) I also don't start papers and talks by saying that everything will be in ZFC, for the same reason that this information is (as long as my field is concerned) obvious and distracting, and hence is likely to be a repelling factor; and moreover because of my personal negative emotions towards ZFC. I did, in fact, on one occasion stated a "theorem (ZFC)" in a talk, but only to emphasize that I'm not assuming CH or PFA like some previous authors did.

I'm assuming that other authors may have somewhat similar considerations, so in papers, books and talks in my area, I'm reading every "theorem" as a "theorem (ZFC)", or at least as what could have been meant by the author to be a theorem in ZFC. There seem to exist people who don't read theorems in this way (I'm thinking, in particular, of applied mathematics and mathematical physics; of Vladimir Arnold; and of experimental mathematics and computer science) but certainly N. Bourbaki and his faithful readers do read them in this way; I also suspect some countries including France and Poland to have more of this tradition than some other ones. The same of course applies to lemmas, problems and conjectures.

Now the situation is different in foundations. You certainly don't read "Problem. Is PA consistent?" as "Problem (ZFC). Is PA consistent?" - at least if you have ever heard of Hilbert's, Goedel's and Gentzen's work on this subject. In set theory, authors usually make it clear what formal system is assumed in their book, chapter or theorem. In other subjects such as proof theory and model theory I understand that the situation is rather complex, but it seems that the prevalent convention in some areas where PA or the second-order arithmetic are more relevant than ZFC is that by default, a "Theorem" could read as "Theorem (no hypotheses whatsoever)." What exactly "no hypotheses whatsoever" means is a separate question, but for the moment I'd like to note that the linguistic/pshychological issue of the clash of conventions for reading words like "theorem", "problem" and "proof" is not mentioned in Timothy's first answer, yet is central to its understanding. For this reason I dismiss his argument as pure sophistry.

This doesn't yet address his conclusion - that Con(PA) is true (in the sense of Plato) because we know (in the sense of Plato) a model of PA. (By the way, this purported knowledge usually turns out to be an implicit hypothesis in the "no hypotheses whatsoever" reading.) But how could we possibly know that what we usually refer to as "1,2,3,..." (I will abbreviate this as $\Bbb N$) is indeed a model of PA? (Note that "1,2,3,..." is only a name, and not a model itself, due to the presence of the undefined/circularly defined symbol "...".) I see only 3 possibilities:

1) by virtue of a religious belief;

2) we could know it from experience, by having a physical model of PA;

3) we could know it from the mind, by demonstrating logically that $\Bbb N$ must be a model of PA.

In connection with the off-topic possibility (1), which I'm not denying, let me only mention some sources: (a) Poincare has devoted quite a few interesting pages to argue for his view that the axiom of induction is a synthetic a priori judgement, (b) Goedel, and in more detail Roger Penrose used the hypothesis that $\Bbb N$ is a model of PA to argue rather convincingly for certain philosophical propositions related to religion.

The off-topic possibility (2) would have strong consequences for physics, which have not been established yet: given a physical model of PA, apparently either the "physical universe" (the past light cone) is a non-compact 3-manifold; or there can be an infinite amount information within its bounded region, which would contradict the holographic principle (which holds in some flavors of string theory) and also some rivals of string theory such as loop quantum gravity (which involves a quantized, rather than Euclidean, space-time).

Finally, the possibility (3). Parikh and Sazonov have shown (assuming our knowledge of a model of PA) that there exist "truncated" versions of PA which are contradictory due to the truncation, yet the shortest proof of contradiction is too long to fit within the theory; thus the theory doesn't "see" itself as being contradictory. Now imagine a finite computer $X$ on which a Peano-Sazonov arithmetic is implemented. If we happen to have a model of PA, or a bigger computer $Y$ (without tricks) at hand, we could be able to use $Y$ to verify that $X$ does not emulate PA correctly, and so $X$ could be finite. But without $Y$, I don't see how to do it. So it looks like $X$ must seem infinite to its user (unless the user's mind is bigger than $X$).

Could our $\Bbb N$ be just a kind of the computer $X$? That is, could God have faked Sazonov integers for us, and kept Peano integers for himself? I don't see any reason why this couldn't have happened. Please correct me if I'm wrong. (I can't resist recalling that while most people are aware nowadays that the Earth is not flat, the notion of $3$-manifolds other than $\Bbb R^3$ still does not occur to many people outside academia in connection with the physical universe.)

The conclusion is that we don't know that $\Bbb N$ is a model of PA; it is an open problem (in platonist's sense, no hypotheses whatsoever, in particular no assumptions regarding our knowledge of a model of PA). Hence there's also no known reason why Con(PA) couldn't be an open problem (in the same sense).

-
As noted by Noah Snyder on the meta thread, this question itself already uses "philosophical" language like "know". This is high in criticism, for Many MO questions do this, with the word Why. As a timely simple example, there is "Why do $H_4$ and $M_4$ have the same virtual Euler characteristic?" and I can't dread the poster wants an answer like "because computation X shows it as -1/1440 for each case". I do not count, but I suspect ~25% or more of MO questions are really aimed more philosophical in nature, as the sense of being explanatory of a fact, than just directly what the fact is. – Junkie Jun 5 '11 at 4:33
Junkie: I didn't intend this as a criticism, but only to point out that the question can have many correct answers. Thank you for clarification. – Sergey Melikhov Jun 5 '11 at 11:06

The following is a (I hope correct) adaption of an argument of H. Friedman made on the FOM list, which I found very instructive.

The following statements are esentially equivalent:

a. The consistency of PA is proved.

b. It is proved that for every bounded sequence of rational numbers there exists a subsequence $q_i$ such that for every $n$ one has $$|q_i - q_j| < 1/n$$ for $i,j \ge n$.

So, I understand that one can have doubts about b. too, but still I think it clearly demonstrates that if one doubts that the consistency of PA is proved, then one has to doubt all kinds of other classical mathemtical facts.

-
Dear unknown, I agree with this answer, and my impression, from listening to Voevodsky's lecture, is that he does reject a lot of classical mathematical facts, in so far as he adopts an extremely constructivist stance. (See my answer for a slight elaboration on this). Best wishes, Matthew – Emerton Jun 1 '11 at 13:00
The Friedman correspondence is in cs.nyu.edu/pipermail/fom/2011-May/015506.html – Junkie Jun 1 '11 at 14:02
This is not quite what Friedman said. Firstly, I find your "proved" misleading (proved in what formal system?). Secondly, your b involves quantification over sets of integers, so I don't think that your assertion that a implies b corresponds to any actual theorem. What Friedman said is that RCA_0 + (your b without "proved") is equivalent to a system that interprets PA. Thirdly, and I think most importantly, the system RCA_0 allows induction over formulas involving universal quantification over sets of integers (which PA doesn't). – Sergey Melikhov Jun 1 '11 at 18:24
Added: I did not see the second comment of Sergey Melikhov before finalizing my comments. However, it seems this does not have to severe consequences, except that I should add (again) that I am not qualified to 'defend' Friedman's argument. As said I tried to 'quote' him. In case, I should misrepresent his views I will of course modify my answer. If this is not so, please consider my answer as more-or-less a (free) quotation that I found instructive. – user9072 Jun 1 '11 at 19:28
Timothy: I would be interested to see this deduction when it appears. – Sergey Melikhov Jun 2 '11 at 10:08

Dear Tim, I read your same argument (up to homotopy) on FOM a couple of days ago and I must say: NOT convincing. You may ask why, and I am glad to tell you: the $n$ in the induction formula and the x and y in the ∃y:y+y=x are not integers, but TERMS in the language of PA. I certainly have no problems manipulating terms using PA, but about integers I know nothing, in fact I doubt they actually exist (and by the way, I am not alone: Nelson, for one, doubts them too). And I do not mean I doubt that 2^10^10^100000000 exists -in fact it does, just another fancy term), I mean I doubt that even the NUMBER 5 exists. In fact, let me tell u more: what is 5? Answer: the (infinite) equivalence class of terms in the language of PA which are provably equal to SSSSS0. Do you REALLY know this class? I doubt. Perhaps some incredibly complicated term will eventually be proved equal to SSSSS0, and nobody now knows it, or even fancies about it. Bottom line, your argument is basically this: IF there is such a thing as the integers and I know them, THEN PA is (obviously) consistent. A small IF for you, a gigantic one for me.

Coda: do I believe that PA is inconsistent? I would not bet my house on that. But I would not bet my life on PA being consistent either...

-
Dear Mirco, I don't see the difference between faith in numbers and faith in symbols. The one unique (symbolic) entity that we always refer to when we write down something like "SSSSS0" does not strike me as any less mysterious than the equivalence class of all 5-element sets. If you give numbers to the devil, he's going to take the free semigroup generated by the letters used in mathematical discourse. – SJR May 27 '11 at 2:19
I agree with SJR. If you don't believe in numbers, then I don't see why you believe in PA. You ask me, what is 5? I reply, what is a symbol? – Timothy Chow May 27 '11 at 2:43
To work with PA, one has to be able to tell the difference between SSSS0 and SSSSS0. How are you able to tell the difference? I personally do so by counting the number of symbols and noting that one has 5 symbols and the other doesn't. Since you don't know what 5 is, this technique is unavailable to you. And if you can't keep track of the difference between SSSS0 and SSSSS0 then you certainly can't determine whether an alleged PA-proof is correct, or whether your computer program is debugged. So I don't even know what you mean when you say that "PA might be inconsistent." – Timothy Chow May 27 '11 at 15:39
As for your argument, it is you that seem not to accept the obvious, for instance Andreas Blass above understood immediately my position (read again his answer), though he probably will not agree. But at any rate, I try to explain it to you: certainly I know $0, here it is: I write down 0, then S0, then SS0,.. then SSSSS0, and then SSSSS0. BINGO! Now, as I mentioned above, my laptop can be programmed to do just the same, and even to check whether a sequence is well formed or not. For instance, it would reject SS0SSSS0 as invalid. Now, does my laptop know the natural numbers? I doubt it. – Mirco A. Mannucci May 30 '11 at 23:10 5 is the number of fingers on my right hand. Now for everybody's sake I should be really careful not to get into a nasty accident involving my fingers, because that would make PA inconsistent. – Andrej Bauer Jun 1 '11 at 14:12 I'd been very interested in foundational questions for a long time so I think I can say something about it. To understand the question I think it is necessary make some comment: mathematical logic is the study of mathematical theories via mathematics itself. To make theorem about theories first you have to define what is a formula, a theory and a proof, so first you need a (meta-)theory in which you make your demonstration about your theory: usually this (meta-)theory is Zermelo Fraenkel set theory without infinite axiom. This means that every proof of a theorem about a theory is valid if the meta-theory is consistent, if that's not the case then we cannot say anything because in a inconsistent theory you can deduce everything (that if you use classical logic). This says that we cannot prove the consistency of a theory in an absolute sense but we can only reduce consistency of a theory to the consistency of another theory: so I think today is pointless wonder if PA is consistent, unless you don't believe in the existence of natural number which satisfy all of the Peano Axioms, such existence is the proof of consistence of PA, because it's well know (or I hope so) that a theory with a model is consistent. (In particular if you accept the consistence of ZFC the you can prove PA consistency in this theory). Just one more thing: if you don accept the existence of natural numbers which satisfy PA (and so of a universe which is a model of ZFC) then you cannot accept lots of mathematics that is derived from it. I hope this answer your question. - Dear ineff, Regarding "you cannot accept lots of mathematics that [is] derived[d] from it"; it may be that you instead accept some constructivist versions of standard mathematical theorems. I think there are many (or at least some) working mathematicians who go along with ZFC (so to speak) but have something of a constructivist view, in that they believe that their theorems are of a sufficiently constructive nature that it doesn't really matter what the background foundational theory is. Regards, Matthew – Emerton Jun 2 '11 at 22:24 Note that PRA is sufficient for most meta-theoretic purposes. (You can do pretty much everything except model theory.) Also, PRA is considerably weaker than PA. – François G. Dorais Jun 2 '11 at 22:34 @Emerton: thanks for the correction, I edited; @Emerton and F.G. Dorais: I didn't mean that ZFC is the only system we can use, anyway it's well know that a lot of mathematics cannot be derived without those systems or without something with the same deductive power. By the way the point of my discussion was that: 1. a proof of consistence is just a reduction of the consistence of a theory to the consistence of the meta-theory (so in the end we have to accept some theory without any proof of is consistence); 2. if we accept the existence of a model for PA we also have to accept its consistence. – Giorgio Mossa Jun 3 '11 at 7:38 Here are four quotes: Quote 1. Vladimir Voevodsky "To put it very shortly I think that inconsistency of Peano arithmetic as well as inconsistency 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 Gödel to be impossible to prove." Quote 2. Vladimir Voevodsky "In fact, one would obviously expect that it will be easier to prove the inconsistency of principles which can be used to prove consistency of PA than inconsistency of PA itself." Quote 3. Todd Trimble "It seems everyone agrees that consistency of PA is a theorem, if you accept some stronger system, such as ZFC. So, PA is consistent relative to ZFC. Just as obviously, you need something to prove consistency of PA; it could be$RCA_0$plus some presumably innocuous-looking axiom, but obviously$Con(PA)$doesn't come for free." Quote 4. Tim Chow "Finally, to answer the new question that Franklin has asked, about whether the consistency of any of the systems in which Con(PA) has been proved has been proved: The answer is, "not in any sense that you would likely find satisfying." For example, one can "prove" that PRA + induction up to$\epsilon_0\$ is consistent, in the sense that the consistency proof can be formalized in ZF, which as I said above is the usual standard for settling mathematical questions. If, however, the reason that you're asking the question is that you doubt the consistency of PA, and are hoping that you can settle those doubts by proving the consistency of PA in some "weaker" system that can then be proved consistent using "weaker" assumptions that you don't have any doubts about, then you're basically out of luck. This, roughly speaking, was Hilbert's program for eliminating doubts about the consistency of infinitary set theory. The hope was that one could prove the consistency of (say) ZF on the basis of a weak system such as (say) PRA, about which we had no doubts. But Gödel showed that not only is this impossible, but even if we allow all of ZF into our arsenal, we still can't prove the consistency of ZF. For better or for worse, this tempting road out of skepticism about consistency is intrinsically blocked."

Here are two questions:

Question 1: Is there a proof of Con(PA) in ZFC?

Question 2: Is Peano arithmetic consistent?

I think everybody (including Voevodsky) agrees that the answer to Question 1 is Yes, and in particular that Question 1 is not open.

Is Question 2 open?

As explained in Quotes 1 and 2, Voevodsky thinks that Question 2 is open.

Quotes 3 and 4 suggest (in my opinion) that Todd Trimble and Tim Chow agree with the premise of Voevodsky's argument.

Voevodsky's argument looks very compelling to me.

Also I think it is unlikely that Voevodsky made a mistake in such a simple reasoning; that, if he had made such a mistake, somebody would have pointed it out to him; and that, if somebody had pointed out such a mistake to him, he would have been clever enough to understand it, and honest enough to acknowledge it.

-
'Explicit proof of Con(PA) in ZFC'? Do you mean one where all the details in ZFC-language are written out? Or in a proof assistant? – David Roberts Nov 8 '14 at 6:40
@DavidRoberts - Sorry, I didn't express myself well. I shouldn't have said "explicit". I edited. Thanks! – Pierre-Yves Gaillard Nov 8 '14 at 6:51