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.
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.