Second incompleteness for standard provability

The standard certified provability predicate: For a fixed effective theory T, let ${\mathrm{Prf}}_T(p,a)$ be the chosen numeralwise arithmetic representation of certified proof checking, with proof code first. Use lem-primitive-recursive-syntax-and-proof-checking and the strengthened representation constructed in thm-primitive-recursive-numeralwise-representability. Retain also the finite PA proof of equivalence to its syntactic ${\mathrm{\Sigma }}_1$ computation form. Thus “Sigma1” for this chosen predicate may mean PA-Sigma1; it does not assert Q equivalence.

Put ${\mathrm{Prov}}_T(a):=\mathrm{\exists }p{\mathrm{Prf}}_T(p,a)$ and $\mathrm{Con}(T):=\mathrm{\neg }{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)$, where $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$ is in the appropriate signature and corner brackets denote the numeral of a code. External consistency means that there is no actual finite T-refutation; the displayed Con is an arithmetic formula.

For theories extending Q, $0=1$ may replace the fixed contradiction: Q proves $0\mathrm{\ne }S0$, so from $0=S0$ explosion gives $\mathrm{\perp }$; conversely reflexivity refutes $\mathrm{\perp }$ and explosion gives $0=S0$. Appending these fixed finite proof blocks gives primitive-recursive transformations between refutation certificates, verified in PA. We use the fixed $\mathrm{\perp }$ throughout. Correctness only on standard numerals is insufficient to replace this predicate in a derivability or second-incompleteness theorem.

Löb theorem: Let T extend Q, or have the effective interpreted Q copy needed for diagonalization, and let its chosen provability predicate satisfy D1–D3. If $T⊢{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)\to \varphi$, then $T⊢\varphi$. Consistency is not a hypothesis.

Derivability conditions for the chosen proof predicate: For the standard certified predicate of an effective T extending PA, the following hold for sentences $\varphi ,\psi$: D1, if $T⊢\varphi$ then $T⊢{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)$; D2, T proves ${\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi \to \psi <mi\; mathvariant="normal">⌝</mi>)\to ({\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\psi <mi\; mathvariant="normal">⌝</mi>))$; D3, T proves ${\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)<mi\; mathvariant="normal">⌝</mi>)$. The interpreted version requires an effective PA copy and verification there of the arithmetic proof constructors and axiom-proof translations used below.