# Drawing Blanks

Premature Optimization is a Prerequisite for Success

## Doubting the Consistency: infinite vs. unimaginably large

“The consistency of P remains an open problem.”

Ed Nelson.

“There was also a Beaver, that paced on the deck,
Or would sit making lace in the bow:
And had often (the Bellman said) saved them from wreck,
Though none of the sailors knew how.”

L. Carroll, “The Hunting of the Snark”.

So, how could anyone doubt the consistency of PA? Isn’t $\mathbb{N}$ a model of PA, which is almost “material” and can be used to verify the truth of all the axioms? And didn’t Gentzen prove the consistency of PA using induction up to $\varepsilon_0$, which is obviously true because it simply says that finite trees can be well-ordered?

If you believe in all those “true” and “exists” above (which most people and mathematicians do), then you have no reason to doubt the consistency of PA. But there are people who study foundations of math in more depth than regular mathematicians do. They learn that the structure of the natural numbers is far more complex and mysterious than even what Gödel uncovered. They run into stuff that makes them doubt all those “true” and “exists”. Or I should rather say, to doubt that the current established formalism justifies all those “true” and “exists”.

I’d like to give a few examples.

You can avoid Gödel’s Second Incompleteness theorem by doing away with the 2nd Hilbert-Bernays condition , which is so subtle that no one cares about it. And you don’t even need to change anything in PA, you just need to change the numbering in the proof of Gödel’s 1st Theorem. After that the formula “PA is consistent” will become provable in PA. That would be a slightly different formula than the G statement, but its meaning will be almost exactly the same. (I believe this was first noticed by Solomon Feferman). [this particular fact is not related to Nelson’s attempt to prove inconsistency, I just want to demonstrate how subtle the 2nd Theorem is]

For any n, you can easily define an inconsistent theory in which the shortest proof of a contradiction has the length of the order $2^{2^n}$ .

For any n, you can (not so easily) define an inconsistent theory in which the shortest proof of a contradiction has the length of the order $2^{2^{2}...^2}$ with exponentiation repeated 2n times. (The latter result is due to George Boolos, I believe). This number is so unimaginably large, that this theory would be consistent for all practical purposes not only of gods themselves, but of creators of creators of gods as well.

You don’t need no induction. For any computable property P of natural numbers, there exists a number B such that if $P(0) \wedge P(1) \wedge \dots \wedge P(B)$ then $\forall n : P(n)$. Seriously, it is always sufficient to check if the property holds for a finite segment of the naturals in order to prove that it holds for all naturals. But it is not possible to compute (derive in a mechanical manner) the numbers B or their upper bounds. Some lower bounds are known, and guess what – they are unimaginably large  (See http://en.wikipedia.org/wiki/Busy_beaver#Applications). See also this popular essay by Scott Aaronson http://www.scottaaronson.com/writings/bignumbers.html

Those are some of the facts that make me believe that there might be indeed something wrong with Peano Axioms. This believe is a reason to be excited and not a reason to be worried. I am not an ultrafinitist for two reasons: I believe in Church Thesis (and even more in the informal Church-Turing Thesis) and I think that to be an ultrafinitist one needs to possess way more knowledge about the Foundations of math than I do.