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 Primitive-recursive syntax and certified proof checking and the strengthened representation constructed in Primitive-recursive functions are representable in Q. 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.