Löb's Theorem for proofs of constant size

Question

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?

Answer 1

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.

Answer 2

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.