= 27d567bc2d48d9f40e9ccc20ea370b15)
Benja comments on Decision Theories, Part 3.75: Hang On, I Think This Works After All - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (45)
When you say "PA+i" you must mean a finite fragment of PA+i (e.g., PA+i with a limit on proof length), otherwise I don't see how FairBot ever gets to execute the second "if" statement. But the Löbian cycle:
isn't a theorem when S is a finite fragment of a formal system, because for example S may "barely" prove "if S proves A, then B" and "if S proves B, then A", and run out of proof length to prove A and B from them. I think to be rigorous you need to consider proof lengths explicitly (like cousin_it did with his proofs).
I'm not seeing how this goes through. Can you explain how PA+3 can prove that PA through PA+2 won't have found proofs of contrary conclusions? (If they did, that would imply that PA+3 is inconsistent, but PA+3 can't assume that PA+3 is consistent. How else can PA+3 prove this?)
This is clearly not what orthonormal meant, but I think if you interpret the "provable in PA+i" function as a call to a halting oracle, all the parts that raise questions about proof lengths just go through. (I also had the impression that each step in the post should break down to a formal proof whose length is O(l), where l is the length of the expression specifying how many proofs are searched; if so, everything should work out for a large enough proof limit. I think this was orthonormal's intent. However, I haven't checked this in detail.)
Let me try something, without a high degree of confidence--
The following reasoning is in PA+3, using the halting oracle interpretation so that I do not need to worry about proof lengths. We assume that 'M(FB)=C' is provable in PA+3 and that FB(M) != C, and try to derive a contradiction.
It follows directly that FB(M)=D; given our assumption, this means that PA+2 proves 'M(FB)=D'. Since we're in PA+3, it follows that M(FB)=D. But we also know that if 'FB(M)=C' is provable in PA+3, then M(FB)=C (as stated in the proof of Lemma 8, right before the contentious argument). Thus, if M(FB)=D, then PA+3 does not prove 'FB(M)=C'. This means that PA+3 is consistent. But we also know (given our assumptions) that PA+3 proves both 'M(FB)=C' and 'M(FB)=D' (the latter because PA+3 proves everything that PA+2 proves); contradiction.
It took me a while to sit down and work through it, but the proof works! Thanks for patching the pothole I didn't see.