Proving Peano Arithmetic Partially Consistent?

Gödel’s Lost Letter and P=NP 2018-03-12

An approach to consistency that could work…

Kurt Gödel is feeling bored. Not quite in our English sense of “bored”: German has a word Weltschmerz meaning “world-weariness.” In Kurt’s case it’s Überweltschmerz. We have tried for over a month to get him to do another interview like several times before, but he keeps saying there’s nothing new to talk about.

Today we want to ask all of you—or at least those of you into logic and complexity—whether we can find something to pep Kurt up. Incidentally, we never call him Kurt.

Gödel is of course famous among many things for proving that Peano Arithmetic (PA) cannot prove its own consistency—unless PA is already inconsistent. In the latter case, it would be able to prove everything; and this would imply that PA is useless.

This time we want to talk about whether PA might be proved consistent in weaker senses. The senses would escape the result of Gödel, which is usually called his Second Incompleteness Theorem. A hope is that they can be connected to open questions in complexity theory.

PA

Recall that PA is the first order theory of arithmetic with induction. Actually all we say today could be generalized to many other theories, but to help us focus let’s discuss only PA.

The meaning of consistency for PA can be encoded as follows: Let

$\displaystyle \text{Proof}(x,y)$

mean that ${x}$ encodes a proof in PA of the statement ${y}$ . Formally this means that consistency of PA is

$\displaystyle \forall x \ \neg \text{Proof}(x, \ulcorner 0=1 \urcorner).$

Most mathematicians believe that PA is consistent. The best argument for consistency is probably that the axioms of PA all seem “obvious.” That is they seem to conform to our intuition about arithmetic. Even the powerful induction schema—which pumps out one axiom for each applicable formula—says something that seems clear:

Mathematical induction proves that we can climb as high as we like on a ladder, by proving that we can climb onto the bottom rung (the basis) and that from each rung we can climb up to the next one (the induction).

This is from page 3 of the book Concrete Mathematics.

Yet not everyone believes that PA is consistent, and it follows that not everyone believes that PA is robustly useful. We recently covered the late Vladimir Voevodsky’s doubts. Ed Nelson in 2015 wrote a freely-available book titled simply Elements to argue that PA is inconsistent. This work is flawed, but is interesting that a world-class mathematician is seriously interested in showing something that few working mathematicians believe. The work ends with an afterword by Sam Buss and Terry Tao, in which they say:

We of course believe that Peano arithmetic is consistent; thus we do not expect that Nelson’s project can be completed according to his plans. Nonetheless, there is much new in his papers that is of potential mathematical, philosophical and computational interest. For this reason, they are being posted to the arXiv. Two aspects of these papers seem particularly useful. The first aspect is the novel use of the “surprise examination” and Kolmogorov complexity; there is some possibility that similar techniques might lead to new separation results for fragments of arithmetic. The second aspect is Nelson’s automatic proof-checking via TeX and qea. This is highly interesting and provides a novel method of integrating human-readable proofs with computer verification of proofs.

Nelson’s criticism of PA is well summarized in this talk by Buss, while it was Tao who articulated the flaw in Nelson’s particular Kolmogorov complexity argument for inconsistency, which we also covered here.

Weak PA Consistency

Our idea is to examine consistency from a computer science viewpoint and use this to make a weaker notion: a notion that can be proved and avoid the Gödel limit. The idea is the following:

Can we prove that PA is consistent at least for any proof that we are likely to ever see?

We can make this precise via the following simple notion, ${\text{Con}(\text{PA};t)}$ :

$\displaystyle (\forall x : |x| \leq t) \ \neg \text{Proof}(x, \ulcorner 0=1 \urcorner).$

Note that we mean the length of the proof in symbols, not steps; we could alternately treat ${x}$ as a number and state the bounded quantifier as ${(\forall x < 2^t)}$ .

Clearly for any ${t}$ we can determine whether or not ${\text{Con}(\text{PA};t)}$ is true or not. Of course as ${t}$ grows the cost of checking that all proofs of length at most ${t}$ in binary explodes. Yet there is no Gödel limit on this checking. We want to understand the following question:

Can we check that ${\text{Con}(\text{PA};t)}$ is true for large ${t}$ ?

Let’s take a look at this next.

Cost Of Checking Proofs

Given a Boolean string ${x}$ of length ${t}$ we can check that it encodes a correct proof from PA in time nearly linear in ${t}$ . We need only check that steps are either examples of an axiom or following from the usual rules of inference of a first order logic. Suppose for the rest we assume that this checking can actually be done in linear time: we are throwing out log terms, which will just help us avoid technically more complex statements. This assumption will not change anything in an important way.

This assumption shows that ${\text{Con}(\text{PA};t)}$ can be checked in time ${c^{t}}$ for some constant ${c}$ . This means that we cannot hope to check this for even modest size ${t}$ ‘s. But can we check it much faster? If we could check, for example, that ${\text{Con}(\text{PA};1,\!000,\!000)}$ is true, then we would know that all proofs of at most 1,000,000 bits do not led to contradictions. This covers all proofs that most of us will ever write down or even read. Note that the following is true:

Theorem 1 PA can prove ${\text{Con}(\text{PA};T)}$ for any fixed ${T}$ .

Define ${f(t)}$ as the length of the shortest proof in PA of ${\text{Con}(\text{PA};t)}$ . Clearly, ${f(t)}$ is well defined—whether PA is consistent or not. A question is how slow can ${f(t)}$ grow? Or looking at it another way, can there be short proofs that ${\text{Con}(\text{PA};t)}$ is true? We can also ask this when ${T = g(t)}$ for some function ${g}$ such as ${g(t) = 2^t}$ .

Relationship To Complexity

Note that one can prove theorems like this:

Theorem 2 If ${\mathsf{P=NP}}$ then we can prove ${\text{Con}(\text{PA};t)}$ in time polynomial in ${t}$ .

This would allow us, at least in principle, to check huge length proofs. There are other complexity open problems that would allow us to even check much larger proof lengths.

We want, however, to be very concrete. We really want to know about ${\text{Con}(\text{PA};1,\!000,\!000)}$ more than what happens for large ${t}$ . Incidentally, Gödel used the same number 1,000,000 as a factor in his brief and cryptic paper (see this review) titled “On the Lengths of Proofs.” What he implicitly did there was apply the same method as in his incompleteness theorems to create formulas ${\phi_t}$ expressing,

There does not exist a PA proof of ${\phi_t}$ of length at most ${t}$ .

He meant length to be the number of lines, but Wikipedia’s article on it speaks of symbol length. Interpreted either way, the truth of the formulas ${\phi_t}$ is obvious: they don’t have proofs in PA of length ${t}$ . They have proofs of length ${2^{O(t)}}$ by exhaustive enumeration as above. If ${\mathsf{P=NP}}$ then they have shorter proofs asymptotically—indeed this was the context of Gödel’s insight about ${\mathsf{P=NP}}$ in his famous 1956 letter to John von Neumann. But again we want to be concrete.

Note that in a “meta” sense we already proved ${\phi_t}$ . We know how Gödel’s construction works in general from reading only a finite piece of his proof. Then as we said its truth is obvious. We used ${\log t}$ symbols to write down ${t}$ but we can ignore that. So this is really a finite proof, certainly well under 1,000,000 symbols.

This is exactly what Gödel meant about the length-saving effect. The rub however is that our “meta” proof is assuming the consistency of PA—that is, the shorter proof is in the stronger theory ${\text{PA}' = \text{PA} + \text{Con}(\text{PA})}$ . Gödel asserted (without proof) that the same effect can always be had by progressing to the next higher order of logic.

But going back to our sentences ${\text{Con}(\text{PA};t)}$ , clearly assuming ${\text{Con}(\text{PA})}$ is silly and we want to stick with first-order logic. We can consider changing the rules of PA but not that way. So our query becomes:

Is there a formal logic ${\mathcal{L}}$ , that avoids the criticisms of PA referenced above and does not obviously entail the consistency of PA, such that ${\mathcal{L}}$ can economically prove ${\text{Con}(\text{PA};1,\!000,\!000)}$ ?

We can alternatively talk about programs ${P}$ that construct proofs and shift the question to the complexity—concrete or asymptotic—of verifying that ${P}$ is correct. This could lead into questions about the (resource-bounded) Kolmogorov complexity of proofs. Assuming ${\text{Con}(\text{PA};1,\!000,\!000)}$ really is true, the simple enumeration argument describes a proof with Kolmogorov complexity well under 1,000,000 symbols—but more than 1,000,000 steps would be needed to expand it. The verification angle, however, may even apply in cases of “insanely long proofs.” Other formal or “fromal” approaches might be considered.

Changing the Rules on Gödel

There was a flurry of work in this area for a decade-plus after Sam Buss’s innovative work in the 1980s connecting complexity questions to proofs in bounded arithmetics—that is with restrictions on the PA induction axioms or the underlying logic. We talked about his work here and here. For connections to lengths of proofs Sam himself has written two nice surveys and here is another by Pavel Pudlák. The connections extend to the Natural Proofs barrier against circuit lower bounds.

But as with many approaches to core questions in complexity, progress seems to have slowed. Perhaps it is because we haven’t been following as closely. So we are asking for news and opinions on what is important. And this is also why we are talking here about changing the questions and the rules of the game.

We have turned up some recent work on questions like ours that changes the rules. Martin Fischer wrote a 2014 paper titled “Truth and Speed-Up” and another titled “The Expressive Power of Truth.” The object of the latter is to find “natural truth theories which satisfy both the demand of semantical conservativeness and the demand of adequately extending the expressive power of our language.” The former shows that other theories including one called “ ${\text{PT}_{tot}}$ ,” while syntactically but not semantically conservative, give speedups for proving ${\text{Con}(\text{PA};t)}$ .

We are not sure how to assess these results. The theory ${\text{PT}_{tot}}$ stands for “Positive Truth with internal induction for total formulas” and is studied further in this 2017 paper. The emphasis seems however to be philosophical, relating to the effect of allowing truth to be a predicate. We don’t know how to connect these ideas to complexity questions but they do show scope for further action.

Open Problems

There are several open problems. Can we show that ${\mathsf{P=NP}}$ or similar statements are equivalent to results about how far out we can check consistency? That is, if we could check that PA has no short contradictions, does this imply anything about complexity theory?

Another class of questions is: Is it useful to know that ${\text{Con}(\text{PA};1,\!000,\!000)}$ is true? Does the fact that there is no short contradiction help make one believe in PA as a useful tool? I am not sure what to make of this. What do you think? What would Gödel think?