can’t you prove that proves(outputs(2), n) implies the negation of proves(outputs(1), n)
To prove that, the proof system would need to know its own consistency, because an inconsistent proof system could prove both of these statements and indeed any statement at all. But a proof system cannot know its own consistency without actually being inconsistent (Goedel’s second theorem).
Technically true. You could always just evaluate the two statements and there you have your proof, with length exponential in n. I very much doubt the proof could be made shorter than n though, because the statement is equivalent to “you can’t find a contradiction in these axioms using less than n steps”, the difficulty of which should grow way faster than linearly in n.
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”.
To prove that, the proof system would need to know its own consistency, because an inconsistent proof system could prove both of these statements and indeed any statement at all. But a proof system cannot know its own consistency without actually being inconsistent (Goedel’s second theorem).
For a finite set of proofs, that a given statement is not provable by a proof from that set, is provable, possibly by a proof from that set.
Technically true. You could always just evaluate the two statements and there you have your proof, with length exponential in n. I very much doubt the proof could be made shorter than n though, because the statement is equivalent to “you can’t find a contradiction in these axioms using less than n steps”, the difficulty of which should grow way faster than linearly in n.
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”.
Aha—very cunning.