Skip to main content
deleted 336 characters in body
Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k

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.

A more interesting example might be: let $P(n)$ assert that the $\Sigma_n$ fragment of PA is consistent. Each standard instance of this $P(n)$ is provable in PA, but one must use stronger and stronger axioms in these proofs, and in this sense, the complexity is growing. But the universal $\forall n\, P(n)$ is not provable in PA.

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.

A more interesting example might be: let $P(n)$ assert that the $\Sigma_n$ fragment of PA is consistent. Each standard instance of this $P(n)$ is provable in PA, but one must use stronger and stronger axioms in these proofs, and in this sense, the complexity is growing. But the universal $\forall n\, P(n)$ is not provable in PA.

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.

added 336 characters in body
Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k

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.

A more interesting example might be: let $P(n)$ assert that the $\Sigma_n$ fragment of PA is consistent. Each standard instance of this $P(n)$ is provable in PA, but one must use stronger and stronger axioms in these proofs, and in this sense, the complexity is growing. But the universal $\forall n\, P(n)$ is not provable in PA.

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.

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.

A more interesting example might be: let $P(n)$ assert that the $\Sigma_n$ fragment of PA is consistent. Each standard instance of this $P(n)$ is provable in PA, but one must use stronger and stronger axioms in these proofs, and in this sense, the complexity is growing. But the universal $\forall n\, P(n)$ is not provable in PA.

added 2 characters in body
Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k

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)$$\forall x\, P(x)$ is independent.

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.

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.

added 18 characters in body
Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k
Loading
Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k
Loading