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.
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.