With a finite limit on proof length, the Godel sentence I mentioned might be longer than the limit—and so not fall within the set of proofs under consideration.
However, the point of mentioning the “Undefinability of Truth Theorem” was to illustrate how there might be truths that would be provably correct—under a more sophisticated set of axioms—but which are not captured by the axiom system being used. That can still be true if the limit on proof length is finite.
Incidentally, your rhetoric about me is getting out of control. Please calm down!
With a finite limit on proof length, the Godel sentence I mentioned might be longer than the limit—and so not fall within the set of proofs under consideration.
However, the point of mentioning the “Undefinability of Truth Theorem” was to illustrate how there might be truths that would be provably correct—under a more sophisticated set of axioms—but which are not captured by the axiom system being used. That can still be true if the limit on proof length is finite.
Incidentally, your rhetoric about me is getting out of control. Please calm down!