Is PA consistent? do we know it?

Question

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.

Answer 1

EDIT: I have written a paper that greatly expands on my answer here, and that in particular contains sketches of Gentzen's proof and Friedman's proof, as well as a discussion of formalism.

---

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 every axiom of PA, and this implication can be proven in the system RCA$_0$, yielding a relative consistency proof. Moreover, according to Harvey Friedman, RCA$_0$ can be replaced by a theory deriving from the program of SRM (strict reverse mathematics).

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.

Answer 2

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

Answer 3

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?

Answer 4

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

Answer 5

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

Answer 6

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.

Answer 7

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.

Answer 8

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

Answer 9

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.

Answer 10

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.

Answer 11

I'll answer your question B

B) Is it a mathematical question?

Normally when we consider it, yes. But we can also consider it as an empirical question.

How so? Well, there are two kinds of models of $PA$:

• Those for which $Con(PA)$ (this includes the standard model)
• Those for which $\lnot Con(PA)$

The issue is that models in both groups are logically coherent, and in fact very similar to one another, empirically (in that true finite statements in both are the same). So ultimately, the question "$Con(PA)?$" can be rephrased empirically "Do we live in a $Con(PA)$ or $\lnot Con(PA)$ universe?". If we find a natural number $n$ that encodes a valid proof of $PA \vdash 0=1$, we know we are in the latter.