Skip to main content
added 411 characters in body
Source Link
Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k

This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.

Specifically, Rosser proposes to consider the sentence $\rho$ asserting that for every proof of $\rho$ in PA, there is a smaller proof of $\neg\rho$. In your terminology, $\rho$ asserts its own non-strong-provability. Such a sentence can be constructed by the fixed-point lemma. The conclusion is that if PA is consistent, then $\rho$ is independent of PA. It cannot be provable, since then it would have a proof of some specific length, and PA would prove that some smaller number would be a proof of $\neg\rho$, but by consistency none of those numbers can actually code a proof. And it cannot be refutable, since then $\neg\rho$ would have a proof of some specific length, and so PA would have to prove that one of the smaller numbers is a proof of $\rho$, which again can't happen by consistency.

The forward direction of your biconditional, which you say is "clear", is false if $T$ is inconsistent, since $T$ will prove every $S$, but it will not strongly prove every $S$. Meanwhile, the converse direction is true, since if a statement is strongly provable, it is provable.

Meanwhile, regarding the issues in your final paragraph, it may be interesting to consider the case of the Rosser sentence. In some models of PA, there is a proof of $\rho$ that is smaller than any proof of $\neg\rho$; and in other models of PA, there is a proof of $\neg\rho$ that is smaller than any proof of $\rho$. In both cases, those proofs are nonstandard, since $\rho$ is actually independent of PA.

This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.

Specifically, Rosser proposes to consider the sentence $\rho$ asserting that for every proof of $\rho$ in PA, there is a smaller proof of $\neg\rho$. In your terminology, $\rho$ asserts its own non-strong-provability. Such a sentence can be constructed by the fixed-point lemma. The conclusion is that if PA is consistent, then $\rho$ is independent of PA. It cannot be provable, since then it would have a proof of some specific length, and PA would prove that some smaller number would be a proof of $\neg\rho$, but by consistency none of those numbers can actually code a proof. And it cannot be refutable, since then $\neg\rho$ would have a proof of some specific length, and so PA would have to prove that one of the smaller numbers is a proof of $\rho$, which again can't happen by consistency.

The forward direction of your biconditional, which you say is "clear", is false if $T$ is inconsistent, since $T$ will prove every $S$, but it will not strongly prove every $S$. Meanwhile, the converse direction is true, since if a statement is strongly provable, it is provable.

This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.

Specifically, Rosser proposes to consider the sentence $\rho$ asserting that for every proof of $\rho$ in PA, there is a smaller proof of $\neg\rho$. In your terminology, $\rho$ asserts its own non-strong-provability. Such a sentence can be constructed by the fixed-point lemma. The conclusion is that if PA is consistent, then $\rho$ is independent of PA. It cannot be provable, since then it would have a proof of some specific length, and PA would prove that some smaller number would be a proof of $\neg\rho$, but by consistency none of those numbers can actually code a proof. And it cannot be refutable, since then $\neg\rho$ would have a proof of some specific length, and so PA would have to prove that one of the smaller numbers is a proof of $\rho$, which again can't happen by consistency.

The forward direction of your biconditional, which you say is "clear", is false if $T$ is inconsistent, since $T$ will prove every $S$, but it will not strongly prove every $S$. Meanwhile, the converse direction is true, since if a statement is strongly provable, it is provable.

Meanwhile, regarding the issues in your final paragraph, it may be interesting to consider the case of the Rosser sentence. In some models of PA, there is a proof of $\rho$ that is smaller than any proof of $\neg\rho$; and in other models of PA, there is a proof of $\neg\rho$ that is smaller than any proof of $\rho$. In both cases, those proofs are nonstandard, since $\rho$ is actually independent of PA.

added 741 characters in body
Source Link
Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k

This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.

Specifically, Rosser proposes to consider the sentence $\rho$ asserting that for every proof of $\rho$ in PA, there is a smaller proof of $\neg\rho$. In your terminology, $\rho$ asserts its own non-strong-provability. Such a sentence can be constructed by the fixed-point lemma. The conclusion is that if PA is consistent, then $\rho$ is independent of PA. It cannot be provable, since then it would have a proof of some specific length, and PA would prove that some smaller number would be a proof of $\neg\rho$, but by consistency none of those numbers can actually code a proof. And it cannot be refutable, since then $\neg\rho$ would have a proof of some specific length, and so PA would have to prove that one of the smaller numbers is a proof of $\rho$, which again can't happen by consistency.

The forward direction of your biconditional, which you say is "clear", is false if $T$ is inconsistent, since $T$ will prove every $S$, but it will not strongly prove every $S$. Meanwhile, the converse direction is true, since if a statement is strongly provable, it is provable.

This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.

The forward direction of your biconditional, which you say is "clear", is false if $T$ is inconsistent, since $T$ will prove every $S$, but it will not strongly prove every $S$. Meanwhile, the converse direction is true, since if a statement is strongly provable, it is provable.

This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.

Specifically, Rosser proposes to consider the sentence $\rho$ asserting that for every proof of $\rho$ in PA, there is a smaller proof of $\neg\rho$. In your terminology, $\rho$ asserts its own non-strong-provability. Such a sentence can be constructed by the fixed-point lemma. The conclusion is that if PA is consistent, then $\rho$ is independent of PA. It cannot be provable, since then it would have a proof of some specific length, and PA would prove that some smaller number would be a proof of $\neg\rho$, but by consistency none of those numbers can actually code a proof. And it cannot be refutable, since then $\neg\rho$ would have a proof of some specific length, and so PA would have to prove that one of the smaller numbers is a proof of $\rho$, which again can't happen by consistency.

The forward direction of your biconditional, which you say is "clear", is false if $T$ is inconsistent, since $T$ will prove every $S$, but it will not strongly prove every $S$. Meanwhile, the converse direction is true, since if a statement is strongly provable, it is provable.

Source Link
Joel David Hamkins
  • 236.3k
  • 44
  • 777
  • 1.4k

This idea in play here is due to Rosser and is the main idea behind the Gödel-Rosser theorem.

The forward direction of your biconditional, which you say is "clear", is false if $T$ is inconsistent, since $T$ will prove every $S$, but it will not strongly prove every $S$. Meanwhile, the converse direction is true, since if a statement is strongly provable, it is provable.