Good catch! Yes, my argument only shows that there’s no short easy proof. You can always just evaluate the two statements and there you have your proof. But that has length exponential in nmax. I’d be amazed if “1=2 is unprovable with length < nmax” were provable with length < nmax, which is pretty much the same statement. This is a very very strong statement. It can also be reformulated as “you cannot find a contradiction in the theory using less than nmax steps”.
Good catch! Yes, my argument only shows that there’s no short easy proof. You can always just evaluate the two statements and there you have your proof. But that has length exponential in nmax. I’d be amazed if “1=2 is unprovable with length < nmax” were provable with length < nmax, which is pretty much the same statement. This is a very very strong statement. It can also be reformulated as “you cannot find a contradiction in the theory using less than nmax steps”.