I’m not convinced that FairBot cooperates with itself. If we call the statement that FairBot self-cooperates S, then it is not the case that we know that (There exists a proof of S) → S [which would imply S by Lob’s Theorem]. Instead, what we know is (There exists a proof of S of length at most Ackermann(20)) → S. I’m not convinced that this is enough to conclude S. In fact, I am somewhat doubtful that S is true.
In particular, I can also prove (There exists a proof of (not S) of length at most Ackermann(20)) → (not S). This is by case analysis:
If S is false: By simulating FairBot, I can prove not S, and thus the statement
If S is true: Since the axioms are consistent, there is no proof of (not S). Thus, by enumerating all proofs of length at most Ackermann(20), I can prove that there is no proof of (not S) of at most this length, thus proving the above statement.
Then again, it is likely that any proof of this implication would need to be longer than Ackermann(20)...
On the other hand, you do need more than Lob’s Theorem to prove that FairBot self-cooperates. Anybody know enough logic to resolve this issue?
Ah, never mind I see it. You just need to modify the proof of Lob’s Theorem. Instead of using
L = (there exists a proof of L) → S
you instead use
L = (there exists a proof of L of length at most Ackermann(10)) → S
and the rest of the proof of Lob’s Theorem still works.
Yeah, that’s the main idea. Note that to state the bounded version of Lob’s theorem, you actually have to use two separate limits: “if having a bounded-size proof of statement S would imply the truth of S, and that fact itself has a short enough proof, then S is provable”. The proof is similar to the regular Lob’s theorem, but each step has to keep track of length limits, and these bookkeeping details eventually determine how high the limits have to be in the first place for the theorem to be true.
I’m not convinced that FairBot cooperates with itself. If we call the statement that FairBot self-cooperates S, then it is not the case that we know that (There exists a proof of S) → S [which would imply S by Lob’s Theorem]. Instead, what we know is (There exists a proof of S of length at most Ackermann(20)) → S. I’m not convinced that this is enough to conclude S. In fact, I am somewhat doubtful that S is true.
In particular, I can also prove (There exists a proof of (not S) of length at most Ackermann(20)) → (not S). This is by case analysis:
If S is false: By simulating FairBot, I can prove not S, and thus the statement
If S is true: Since the axioms are consistent, there is no proof of (not S). Thus, by enumerating all proofs of length at most Ackermann(20), I can prove that there is no proof of (not S) of at most this length, thus proving the above statement. Then again, it is likely that any proof of this implication would need to be longer than Ackermann(20)...
On the other hand, you do need more than Lob’s Theorem to prove that FairBot self-cooperates. Anybody know enough logic to resolve this issue?
Ah, never mind I see it. You just need to modify the proof of Lob’s Theorem. Instead of using L = (there exists a proof of L) → S you instead use L = (there exists a proof of L of length at most Ackermann(10)) → S and the rest of the proof of Lob’s Theorem still works.
Yeah, that’s the main idea. Note that to state the bounded version of Lob’s theorem, you actually have to use two separate limits: “if having a bounded-size proof of statement S would imply the truth of S, and that fact itself has a short enough proof, then S is provable”. The proof is similar to the regular Lob’s theorem, but each step has to keep track of length limits, and these bookkeeping details eventually determine how high the limits have to be in the first place for the theorem to be true.