As I understand it, because T proves in n symbols that “T can’t prove a falsehood in f(n) symbols”, taking the specification of R (program length) we could do a formal verification proof that R will not find any proofs, as R only finds a proof if T can prove a falsehood within g(n)<exp(g(n)<<f(n) symbols. So I’m guessing that the slightly-more-than-n-symbols-long is on the order of:
n + Length(proof in T that R won’t print with the starting true statement that “T can’t prove a falsehood in f(n) symbols”)
This would vary some with the length of R and with the choice of T.
As I understand it, because T proves in n symbols that “T can’t prove a falsehood in f(n) symbols”, taking the specification of R (program length) we could do a formal verification proof that R will not find any proofs, as R only finds a proof if T can prove a falsehood within g(n)<exp(g(n)<<f(n) symbols. So I’m guessing that the slightly-more-than-n-symbols-long is on the order of:
n + Length(proof in T that R won’t print with the starting true statement that “T can’t prove a falsehood in f(n) symbols”)
This would vary some with the length of R and with the choice of T.