# Löb's Theorem for proofs of constant size

Löb's Theorem roughly states that for any formal system $T$ with Peano Arithmetic and all formulas $P$

If $T$ proves (if $T$ proves $P$ then $P$) then $T$ proves $P$

What happens if we change the inner condition slightly, so that it is assumed the proof is of a certain size, let's say $1$? Consider the following claim:

If $T$ proves (if $T$ proves $P$ in one step then $P$) then $T$ proves $P$

Proving something in one step is equivalent to having it as an axiom. We can also take the contrapositive of the whole thing, yielding

Suppose $T$ doesn't prove $P$. Then $T$ doesn't prove (if $P$ is an axiom of $T$ then $P$)

If that still holds, then it seems as though $T$ is unable to prove the fact that its axioms are true. This actually seems reasonable if we remember that "$P$ is an axiom of $T$" is actually saying something about the string $P$ the "inner" $T$ sees, which the "outer" $T$ doesn't know how to relate to its own (supposed) axiom $P$.

Is the modified claim still a theorem, and, if so, is my analysis in the previous paragraph correct?

• Why would it still hold, though? It's ostensibly a stronger statement. – spaceisdarkgreen May 5 '18 at 2:34
• Counterexample: $T$ is Peano arithmetic, $P$ is $0\ne0.$ Peano arithmetic is consistent, but Peano arithmetic proves that no contradiction can be derived in $P$ in less than a million steps. – bof May 5 '18 at 2:51
• @bof And for any $n,$ if indeed there's no such contradiction, PA can prove there's no contraction in less than $n$ steps. (Though I suppose it could do the same if there were such a contradiction.. hmm.) – spaceisdarkgreen May 5 '18 at 4:17

We can cut out some chaff here and define a predicate $A_T(x)$ analogous to $\operatorname{Prov}_T(x)$ that expresses when $x$ is (the Godel number of) an axiom of T. Since T is PA here, the axioms are a recursive set, so we can choose $A_T(x)$ to be a $\Delta_0$ formula.

If $\phi$ is an axiom, then of course it is provable, so PA proves $A(\ulcorner\phi\urcorner)\to \phi.$ If $\phi$ is not an axiom then $A(\ulcorner\phi\urcorner)$ is a false $\Delta_0$ statement and thus its negation is provable in PA, so again PA proves $A(\ulcorner\phi\urcorner)\to \phi.$ So we have $T\vdash A(\ulcorner\phi\urcorner)\to \phi$ for all sentences $\phi.$

And yet we know that there is a sentence such that $T\not\vdash \phi$ (assuming that PA is consistent of course). So your stronger version of Lob's theorem is false.

Similarly, for any $n,$ the set of sentences for which there is a PA proof of length less than $n$ is recursive. So your statement is false for an arbitrary finite number of steps, not just one.

• I see. So $PA$ doesn't need to see a connection between $A(\ulcorner\phi\urcorner)$ and $\phi$. All it needs is to prove the latter or the negation of the former. I'm not sure if I should ask this as a separate question, but here goes: suppose a theory $T$ containing $PA$ cannot prove $\neg A_T(\ulcorner\phi\urcorner)$ and cannot prove $\phi$. Would it still be able to prove $A_T(\ulcorner\phi\urcorner)\rightarrow\phi$? – Detached Laconian May 5 '18 at 22:55
• @TuringMachine Yes, for any given sentence, PA can prove $A_{PA}(\ulcorner\phi\urcorner) \to \phi$ but it cannot express, let alone prove this statement quantified over all sentences (if that's what you mean by "see the connection"). Your question is an odd hypothetical and I'm not sure where you're going with it. If T is a recursively axiomatized extension of PA, then the same above reasoning applies to it, so there is no such situation. Maybe it's confusion stemming from your first remark: it is jarring how wide a gulf there can be between "for all _ T proves _" and "T proves for all _, _." – spaceisdarkgreen May 6 '18 at 3:41
• @TuringMachine Ahh I think I catch the connection between your first point and your question now. It's a familiar complaint at the connective $\to$. $A\to B$ is only really compelling to PA if it doesn't already know $\lnot A$ or $B,$ even if it might be technically true here. Unfortunately, PA is not in this situation for a given instance of the scheme (i.e. the statement for a given sentence $\phi$). A universally quantified version of the scheme would be more compelling, but PA doesn't even know there's something to quantify over (see my last comment). So my answer is pretty much the same. – spaceisdarkgreen May 6 '18 at 4:36
• What about a theory $T$ that's not recursively axiomatized? I know this is a very weird kind of theory, but, for the sake of the "connection" issue, I think it'd be nice to know that $T$ wouldn't necessarily be able to prove $A_T(\ulcorner \phi \urcorner) \rightarrow \phi$, so that, in a sense, the theory $T$ doesn't "understand" its axioms are true. – Detached Laconian May 7 '18 at 4:58
• @TuringMachine I don't know. One obstacle here is that when we stop assuming RA, it's not just that the property of being an axiom may no longer be representable, but we lose the right to assume it's expressible as well (and Tarski's theorem will attest to this). – spaceisdarkgreen May 7 '18 at 5:35

spaceisdarkgreen's answer is good, but the way I like to think about Löb's theorem is that it says that (in any sufficiently strong system $T$) that to prove $\phi$, it is admissible to assume $\mbox{Pr}(\ulcorner \phi \urcorner)$ (where $\mbox{Pr}$ is the provability predicate for $T$). Clearly assuming $\phi$ is provable in one step is not admissible, since (if $T$ is consistent) there are unprovable formulas that are not axioms, so your strengthened form of Löb's theorem is false.

• That's an interesting way to think about it! I'm not sure I understand the part about one-step proofs, though. You say "there are unprovable formulas that are not axioms", but there are also unprovable formulas that are not provable. I don't see what has changed here. – Detached Laconian May 5 '18 at 23:04
• If $\phi$ is neither an axiom nor provable and we assume it is provable in one step, then we are assuming it is an axiom and hence we have a contradiction, from which we can infer anything, in particular we can infer that $\phi$ is provable. So it is not admissible to assume that the formula we are trying to prove is provable in one step. – Rob Arthan May 6 '18 at 10:00
• I see. The important distinction, though, is that $PA$ can prove $\phi$ isn't an axiom when $\phi$ isn't an axiom. On the other hand, $PA$ can't necessarily prove $\phi$ isn't provable when $\phi$ isn't provable. – Detached Laconian May 7 '18 at 4:49