This is the great mathematician Terry Tao explaining how he spotted the error in Prof. Nelson's proof purporting to show Peano Arithmetic to be inconsistent- thus refuting 'Logic's Lost genius' Gerhard Gentzen 1936 result.

Actually, Nelson's proof was relatively easy to understand, in part because he took the trouble to write out a short outline which make clear the general strategy of proof while omitting most of the technical details (though it was ambiguous at one very crucial juncture), and also because I had already previously thought about the surprise examination (or unexpected hanging) paradox and the Kritchman-Raz argument (see the last section of http://terrytao.wordpress.com/2011/05/19/epistemic-logic-temporal-epistemic-logic-and-the-blue-eyed-islander-puzzle-lower-bound/ ).

From the outline one could already see that the main idea was to adapt the Kritchman-Raz argument to the theory Q_0^*, which "almost" proved its own consistency in that it contained a hierarchy of theories Q_1, Q_2, Q_3, ..., each of which could prove the consistency of its predecessor.

Now, I did not at the time fully understand the definition of Q_0^*, nor was I fully aware of the Hilbert-Ackermann result which guaranteed this chain of consistency results, but I was willing to accept the existence of such a hierarchy of theories. (I've since read up a bit on these topics, though.) The question was then, given such an abstract hierarchy, whether one could use the arguments of Chaitin and Kritchman-Raz to establish the inconsistency of at least one of these theories.

These arguments were simple enough (they were basically formalisations of the Berry paradox and surprise examination paradox respectively) that I could then try to do that directly, without any further assistance from the outline. And, indeed, when I attempted to do this, I did at first seem to obtain a contradiction (much as paradoxes such as the Berry or surprise examination paradoxes also lead to absurdity if one reasons somewhat carelessly using informal naive argument). So I could see where Nelson was coming from; but then I spent some time trying to expand out my arguments in detail to find the error. The key, as I found out, was to specify exactly what proof verifier would be used for the Chaitin portion of the argument (this was an issue that was left ambiguous in Nelson's outline), and in particular whether it would accept proofs of unbounded complexity or not. Since Nelson wanted to keep all proofs at bounded complexity, I used a proof verifier that enforced such a bound, and eventually worked out that this could not be done while keeping the length of the Chaitin machine constant; this was the objection that I raised in my first few comments. However, after Nelson responded, it became clear that he was using an unrestricted proof verifier, and this led to a different problem, namely that the proofs produced by Chaitin's argument were of unbounded complexity. So there was not a single "flaw" in the argument, but rather there were two separate flaws, one of which was relevant to one interpretation of the argument, and the other of which was relevant to an alternate interpretation of the argument.

Aside from this one ambiguity, though, the outline was quite clear. Certainly there have been other manuscripts claiming major results that were much more difficult to adjudicate because they were written so badly that there were multiple ambiguities or inaccuracies in the exposition, and any high-level perspective on the argument was obscured.

Nelson's quickness to recant after examining Tao's objection has been commented on in a post titled 'why do Mathematicians always agree'?

In response, Catarina Dutilh Novaes, writes-

In my current research project on deduction, I am working on the idea of a dialogical reconceptualization of deduction. One of the upshots would be that the mathematical method itself is able to counter our tendency towards confirmation bias, in virtue of what I call the 'built-in opponent' feature. When formulating a mathematical proof, proponent has to ensure that there are no counterexamples to any of her inferential steps, as if anticipating possible objections by an opponent. In this way, she is 'forced' to adopt the position both of someone who is convinced of the cogency of the claim and of someone who is not.

My response, from the socioproctological perspective is-

In this specific case, all the mathematicians involved relied for their work on a specific highly developed theory- call it a module- and none was prepared to bear the cognitive cost of re-writing the entire module which is why there could be a quick resolution. Surely this happens all the time in other disciplines as well? Indeed the less 'rational' or alethic the subject area the lower the cognitive pay-off for rewriting entire modules so we might find even faster resolution, without even the pause for critical thought. Prof. Nelson was quick to see his error precisely because he is one of the brightest people in his discipline. A lesser mind, even if capable of formulating Nelson's thesis, would have taken much longer to concede the disputed point.

Still, suppose there was a big cognitive pay-off, currently available, for entirely rewriting the Chaitin/ Kolmogorov 'module' re. complexity, then it may be that some one or other of those involved in this dispute might have taken that tack.

Surely an 'in-built opponent' is a feature of all social communication? It weighs down most heavily where the cognitive cost of re-writing modules are high or the reward is miniscule? I suppose statements about fashion or syntax or what is considered politically correct, have this feature and thus in most social sub-sets there is going to be very quick recantation simply because the cost greatly outweighs any possible benefit.

At this point, I'd like to introduce a notion of ontologically dysphoria- the feeling of being in the wrong Universe, the intuition that the Cartesian duality of mind and body points to something more troubling, bizarre or tragic. It may be that there is a sort of genotypal canalisation towards a widespread feeling of this sort- perhaps, rather than a malaise attributable to the welgeist, ontological dysphoria is the driver for the necessary-but-not-too-much preference diversity needed to drive trade, but also communication and the elaboration of Knowledge systems.

It may make a sort of collocational sense for us to agree that Math represents a limit case of one sort and philosophy, with its distinctions without differences, as the limit case of its opposite.

Godel and Von Neumann, both Theists on their death beds, who agreed on so much in the way of mathematics yet had ontological dysphorias of opposite tropism. It may be that the latter type of 'madness'- or stark solipsistic discontinuity- is as important a driver for breakthroughs in Maths as the great powers of 'reason' both possessed which enabled Von Neumann to grasp Godel's result, perhaps, more thoroughly and more quickly than the latter had done himself.

Nelson's motivation is his formalist critique of finitism- http://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html

ReplyDelete'In his book Elements, in the chapter Against Finitism, Nelson explains his doubts about the principle of mathematical induction:

'Induction is justified by appeal to the finitary credo: for every number x there exists a numeral d such that x is d. It is necessary to make this precise; as someone once said, it depends on what you mean by “is”. We cannot express it as a formula of arithmetic because “there exists” in “there exists a numeral d” is a metamathematical existence assertion, not an arithmetical formula beginning with ∃.Induction is justified by appeal to the finitary credo: for every number x there exists a numeral d such that x is d. It is necessary to make this precise; as someone once said, it depends on what you mean by “is”. We cannot express it as a formula of arithmetic because “there exists” in “there exists a numeral d” is a metamathematical existence assertion, not an arithmetical formula beginning with ∃.

Let A be a formula of P with just one free variable x such that ⊢P∃xA. By the least number principle (which is a form of induction), there is a least number x satisfying A. One might, thinking that every number is a numeral, assert that there exists a numeral d such that ⊢PAx(d).

[Here Ax(d) is A with the free variable x replaced by the numeral d.]

But, as I learned from Simon Kochen, this does not work. The rank of a formula is the number of occurrences of ∃ in it. Let B be the formula asserting that there is no arithmetized proof of a contradiction all of whose formulas are of rank at most x. Then each Bx(d) can be proved in P by introducing a truth definition for formulas of rank at most d. But if P is consistent then ∀xB is not a theorem of P, by Gödel’s second theorem. Now let A be B⇒∀xB. Then ∃xA is a theorem of P since it is equivalent to the tautology ∀xB⇒∀xB, but (if P is consistent) there is no numeral d such that ⊢PAx(d).

The finitary credo can be formulated precisely using the concept of the standard model of arithmetic: for every element ξ of N there exists a numeral d such that it can be proved that d is equal to the name of ξ; but this brings us back to set theory. The finitary credo has an infinitary foundation.

The use of induction goes far beyond the application to numerals. It is used to create new kinds of numbers (exponential, superexponential, and so forth) in the belief that they already exist in a completed infinity. If there were a completed in finity N consisting of all numbers, then the axioms of P would be true assertions about numbers and P would be consistent.

It is not a priori obvious that P can express combinatorics, but this is well known thanks to Gödel’s great paper on incompleteness. As a consequence, exponentiation ↑ and superexponentiation ⇑ can be defined in P so that we have

... (see link)

The problem is not simply that some primitive recursions are too long. The problem is structural: there is a sharp division between two classes of primitive recursions. This results from work of Bellantoni and Cook; see also Bellantoni’s thesis. They indicate that their work was strongly inuenced by previous work of Leivant, who subsequently gave a more elegant form to the characterization, and it is appropriate to call the result the BCL theorem.

(contd)

ReplyDeleteWhile a number is being constructed by recursion, it is only potential, and when the recursion is complete, it is actual. What Bellantoni and Cook, and Leivant, do is restrict recursions so that they occur only on actual numbers. Then the theorem is that the class of functions computable in this way is precisely the class of polynomial-time functions. This is an astonishing result, since the characterization is qualitative and conceptually motivated, saying nothing whatever about polynomials, Bellantoni, Cook, and Leivant have revealed a profound difference between polynomial-time recursions and all other recursions. The recursions constructed by the BCL schema enjoy a different ontological status from recursions in general. In the former, recursions are performed only on objects that have already been constructed. In the latter, for example in a superexponential recursion, one counts chickens before they are hatched (and the chicks that they produce as well), all in the fond hope that this will eventually take place in the completed infinity by and by.

Not only is induction as a general axiom schema lacking any justification other than an appeal to N as a completed infinity, but its application to specific variable-free primitive-recursive terms lacks a cogent justification. We shall exhibit a superexponential recursion and prove that it does not terminate, thus disproving Church’s Thesis from below and demonstrating that finitism is untenable.'

I think Tao's syntax/semantics dualism helped him elucidate the error (re. permitting unbounded complexity verifiers) very well and it will be very interesting to see how Nelson responds.

This comment has been removed by a blog administrator.

ReplyDeleteThis comment has been removed by a blog administrator.

ReplyDeleteThis comment has been removed by a blog administrator.

ReplyDelete