Regarding Tarski’s theorem—you seem to be misinterpreting me. I am not saying that checking a proof with respect to an axiom system is necessarily difficult. I am saying that truth is not contained by any finite axiom system. So, there will be true statements that are unprovable within the system—but can still be proven in a larger system. Some of those unprovable truths will be of the form that I mentioned.
If that’s what you mean, then you seem to be even more confused than I realized. If you are just talking about the original context then the set of proofs that are below some fixed length cannot be a statement that is true and unproveable. The proof itself self-verifies. If the statement in question is true, there must exist a proof of the statement that is of the desired bounded size. This follows from consistency and the fact that there are only a finite collection of such proofs.
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!
If that’s what you mean, then you seem to be even more confused than I realized. If you are just talking about the original context then the set of proofs that are below some fixed length cannot be a statement that is true and unproveable. The proof itself self-verifies. If the statement in question is true, there must exist a proof of the statement that is of the desired bounded size. This follows from consistency and the fact that there are only a finite collection of such proofs.
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!