I think the proof would be about g(n) symbols long, which is basically linear in n. Since R finds a proof shorter than g(n), exhibiting that proof yields a slightly longer proof that R stops early (because R either finds the exhibited proof, or stops even earlier). Then it’s easy to deduce that T+¬S is inconsistent, which can be converted into a proof of S from T.
I like (apart from the use of T and S to denote very different things). EDIT: and R!
One question: any idea how long it would take T to prove S under this reasoning?
I think the proof would be about g(n) symbols long, which is basically linear in n. Since R finds a proof shorter than g(n), exhibiting that proof yields a slightly longer proof that R stops early (because R either finds the exhibited proof, or stops even earlier). Then it’s easy to deduce that T+¬S is inconsistent, which can be converted into a proof of S from T.