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