Return to Revisions

Consider the assertion $P(x)$ that asserts "$x$ is not the Gödel code of a proof of a contradiction in PA". If PA is consistent, then we can prove $P(n)$ for any particular natural number $n$, since no such $n$ codes a proof. I don't know what is your measure of proof complexity, but the proof of $P(n)$ in every case is mundane: it is because the sequence coded by $n$ violates one of the syntactic requirements of being a proof. Namely, one of the sequents is not an axiom, or does not follow by modus ponens from the earlier sequents, or the conclusion is not a contradiction, and so on. In particular, the formulas appearing in the proofs of $P(n)$ have bounded complexity (although these proofs do get longer, since one must check more cases to cover the earlier sequents). But meanwhile, the assertion $\forall x P(X)$ is independent.