I'm not terribly worried about an actual inconsistency in PA. So much goes wrong if that's the case that AI issues might actually be small (no really. It could be that bad.)
That is an understandable reaction. But since encountering Nelson's ideas a while ago, I've found myself thinking less and less that it would be that bad at all. There is no very strong evidence that completed infinities need to be grappled with at a physical or real-world level. The main "finitary" thing you lose without PA is superexponentiation. But that shows up surprisingly rarely, in the universe and in math. (Or maybe not so surprisingly!)
Interestingly, superexponentiation shows up very often on less wrong. Maybe that's a good answer to XiXiDu's question. If Nelson is right, then people should stop using 3^^^3 in their thought experiments.
If Nelson is right, then people should stop using 3^^^3 in their thought experiments.
...I don't understand how this can be. 3^^3 is just (3^(3^3))= 3^27 = 7625597484987 And 3^^^3 is just (3^(3^(3^(... 7625597484987 times ...))))
Superexponentiation is just made of exponentiation many times. And exponentiation is made of multiplication, and multiplication is made of addition.
How can superexponentiation be made invalid without making invalid even normal addition?
We've discussed Edward Nelson's beliefs and work before. Now, he claims to have a proof of a contradiction in Peano Arithmetic; which if correct is not that specific to PA but imports itself into much weaker systems. I'm skeptical of the proof but haven't had the time to look at it in detail. There seem to be two possible weakpoints in his approach. His approach is to construct a system Q_0^* which looks almost but not quite a fragment of PA and then show that PA both proves this system's consistency and proves its inconsistency.
First, he may be mis-applying the Hilbert-Ackermann theorem-when it applies is highly technical and can be subtle. I don't know enough to comment on that in detail. The second issue is that in trying to show that he can use finitary methods to show there's a contradiction in Q_0^* he may have proven something closer to Q_0^* being omega-inconsistent. Right now, I'm extremely skeptical of this result.
If anyone is going to find an actual contradiction in PA or ZFC it would probably be Nelson. There some clearly interesting material here such as using a formalization of the surprise examiation/unexpected hanging to get a new proof of of Godel's Second Incompleteness Theorem. The exact conditions which this version of Godel's theorem applies may be different from the conditions under which the standard theorem can be proven.