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:
if we have a formal system S, and “if S proves A, then B” and “if S proves B, then A” are theorems of S, then S indeed proves both A and B.
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).
And of course, “if ‘M(FB)=C’ is provable in PA+3, then FB(M)=C” is provable in PA+3, since again PA+3 can prove that PA through PA+2 won’t have found proofs of contrary conclusions before it gets around to trying to find cooperation in PA+3.
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?)
I think to be rigorous you need to consider proof lengths explicitly (like cousin_it did with his proofs).
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.)
Can you explain how PA+3 can prove that PA through PA+2 won’t have found proofs of contrary conclusions?
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.
As Benja said, I’m imagining that my agents have O(1) calls to a hierarchy of halting agents. But when I write it up, I’ll also write up the version with bounded proof limits (where exponentially greater limits correspond to higher oracles), the bounded Löb’s Theorem, etc. I’m not too worried, because (as Paul Christiano put it) there are no interesting differences between what you can do in each case; it’s simply easier to track things with oracle hierarchies.
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?
Hmm. This is a real problem, and I’m thinking about it today.
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.
As Benja said, I’m imagining that my agents have O(1) calls to a hierarchy of halting agents. But when I write it up, I’ll also write up the version with bounded proof limits (where exponentially greater limits correspond to higher oracles), the bounded Löb’s Theorem, etc. I’m not too worried, because (as Paul Christiano put it) there are no interesting differences between what you can do in each case; it’s simply easier to track things with oracle hierarchies.
Hmm. This is a real problem, and I’m thinking about it today.
ETA: Oh, good, Benja’s solution works.