-2
$\begingroup$

I want to coin a notion of "strong provability", to be defined as:

$S$ is strongly provable in $T$ if and only if there is a Gödel code of its proof in $T$ that is strictly smaller than any Gödel code of a proof of its negation in $T$

Formally:

$ S \text { is strongly provable in } T \iff \\ \exists x: \operatorname {Proof}_T(x, \ulcorner S \urcorner ) \land \forall y (\operatorname {Proof}_T (y, \operatorname {neg}(\ulcorner S \urcorner)) \implies x < y ) $

Now let $T \vdash S$ be the usual metatheoretic statement of $S$ being syntactically proved from $T$

Then is it provable that:

$(T\vdash S) \iff S \text { is strongly provable in } T$

The forward direction is clear, but the opposite is what irks me? Can we have a sentence whose smallest code of its proof (not the metatheoretic) is a non-standard natural, and every proof of its negations is strictly lager than it? I mean in this case it'll be indeterminate syntactically speaking, and the statements would be false, yet is this possible, can we have a theory that spells that and be consistent?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
12
  • $\begingroup$ Your last paragraph contradicts the sentence just before it. This means that the biconditional is not true in both directions. However, if we assume that T is consistent, then just the forward direction is true, the other direction is falsified by the models of PA in your last paragraph. I think, if we assume that T is $\omega$-consistent, then we get both directions true. $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 15, 2023 at 21:02
  • $\begingroup$ The statement just before is a statement in the metatheory, that if a statement is strongly provable, then in particular, it is provable. This is obvious, since part of what it means to be strongly provable is to be provable, but furthermore in a certain way. The last paragraph, in contrast, is about the internal notions of provability of the Rosser sentence, and in those models I mention, in fact everything is provable---the only question is whether $\rho$ or $\neg\rho$ has the smaller proof. And the independence of $\rho$ means it can happen either way. $\endgroup$
    – Joel David Hamkins
    Commented Jul 15, 2023 at 21:30
  • $\begingroup$ No! I was speaking about the biconditional, on the left is the syntactic (metatheoretic) provability, while on the right is the notion of strong provability which is a theoretic statement, what I mean is that the right to left direction of the biconditional doesn't hold, because the models of PA you spoke about in your last paragraph shows that you can have $\rho$ being strongly provable (in a theoretic sense) yet not syntactically (metatheoretically) provable. $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 15, 2023 at 21:42
  • $\begingroup$ Strong provability is also a metatheoretic statement, which is the same as interpreting the theoretic statement in the standard model. That is how I am reading your biconditional. What is true in some nonstandard models has nothing to do with the biconditional, which doesn't refer to any nonstandard models. $\endgroup$
    – Joel David Hamkins
    Commented Jul 15, 2023 at 21:53
  • $\begingroup$ Well strong provability as defined here is not a metatheoretic statement, it becomes equivalent to the metatheoretic syntactical notion of provability in the standard model yes, but not in all models. In the models you spoke about it appears that one can state strong provability of a sentence (like $\rho$ or like $\neg \rho$) yet without being able to prove it syntactically. I read the biconditional externally as the existence of a standard natural coding a proof of the sentence in T (on the left) and on the right we have strong provability allowing non-standards, so R to L direction fails $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 16, 2023 at 10:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .