Arithmetical provability predicate (${\mathrm{Pr}}_T(v)$)

For an effectively axiomatized arithmetic theory, a arithmetical provability predicate expresses that a formal proof of the sentence with a specified code exists. If axioms are only enumerated, proof certificates also record finite stages at which their axioms appear. The resulting predicate is arithmetically expressible.

A logical formula weakly defines a total numerical function in a first-order theory when, at every standard input tuple, it proves the graph instance with the correct standard output and refutes graph instances with every incorrect standard output. This is numeralwise representation of the graph; it does not yet assert uniqueness against nonstandard outputs inside a first-order model.

Strong definability of a numerical function adds internal uniqueness of the output at every standard input tuple. Together with a proved correct instance, this says the first-order theory proves that the output logical formula is equivalent to logical equality with the correct numeral, for arbitrary potential outputs.

An arithmetical proof relation represents the effective relation that a natural number encodes a formal proof of the logical formula with a specified Gödel number. With the usual coding apparatus its proof-checking relation is bounded. Existential quantification over the formal proof code gives the ordinary arithmetical provability predicate.

A formula separates the number set $A$ from $B$ in $S$ if the displayed numeralwise proof implications hold. No decision is required outside $A\cup B$. In a consistent theory the sets must be disjoint. A diagonal sentence asserting the negation of its membership in a separator of provable from refutable codes is undecidable by the two direct contradiction cases.

A two-variable formula enumerates a set $A$ in a theory $S$ when membership supplies a standard numeral stage whose instance is provable, while nonmembership makes every standard-stage instance refutable. The notion contains these proof obligations, not merely a syntactic complexity restriction on the formula. With bounded completeness, a bounded formula whose existential closure defines a computably enumerable set provides such an enumerator.^[ref]

A Rosser provability predicate adds a bounded proof-order test to an arithmetical provability predicate: a proof of the sentence must occur before every proof of its negation. For a consistent theory it has the same standard extension as ordinary provability. Internally its behavior can differ: arithmetic proves $\neg R_T(┌\perp ┐)$ by splitting proof codes before and after a fixed proof of $\neg \perp$. This does not establish the usual consistency statement for ordinary provability.

The internal derivability conditions of a Rosser provability predicate depend on the proof numbering, even when the ordinary provability predicate is unchanged up to provable equivalence. Joining proofs of $A$ and $A\to B$ can increase their codes beyond the two bounds in the Rosser hypotheses, leaving the absence of earlier proofs of $\neg B$ unestablished. Internal modus ponens rule therefore needs a separate argument for the chosen numbering. Proof predicates can be constructed with different combinations of closure and introspection properties. ^[ref]. ^[ref].

If a first-order theory proves both $A$ and $\neg A$, the external truth of its Rosser provability predicate for $A$ depends on which side has the earlier formal proof code. A reserved least code for a formal proof of $\neg A$ makes the Rosser assertion false. Reserving the least code for a formal proof of $A$ makes it true. These are legitimate effective renumberings of the same formal proofs. Inconsistent first-order theories therefore require an explicit proof-order convention.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. If $T+X$ proves ${\mathrm{Pr}}_T(┌Y┐)\to Y$ for every sentence $Y$, then $T⊢\neg X$. Take the single instance $Y=\neg X$ and discharge the assumption: $T⊢X\to (\square \neg X\to \neg X)$. This propositionally implies $T⊢\square \neg X\to \neg X$, and Löb's theorem gives $T⊢\neg X$. A diagonal proof is also possible using the Gödel sentence of the extension and formalized proof transfer, without appealing to Löb's theorem.

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. Choose $D$ with $T⊢D\leftrightarrow (\square D\to A)$. Necessitating the forward implication and using distribution and positive introspection gives $T⊢\square D\to \square A$. If $T⊢\square A\to A$, then $T⊢\square D\to A$, so the reverse fixed-point implication gives $T⊢D$. Necessitation gives $T⊢\square D$, and the preceding implications give $T⊢A$. No consistency assumption is needed for this implication between provability assertions.

For standard provability satisfying positive introspection, suppose $T⊢{\square }^{j}A\to A$ for some positive integer $j$. Positive introspection gives $T⊢\square A\to {\square }^{j}A$, hence $T⊢\square A\to A$. Löb's theorem yields $T⊢A$. The same argument applies with an already iterated first-order sentence in place of $A$.

In the Löb's theorem proof, $T⊢\square D\to \square A$ is obtained before any reflection assumption. Put $H=(\square A\to A)$. Propositional reasoning and the diagonal equation give $T⊢H\to D$. Necessitation and distribution yield $T⊢\square H\to \square D$, hence the displayed implication. This is the arithmetic interpretation of the Löb axiom in Gödel-Löb logic, and avoids necessitating a temporary assumption.

For an arithmetical provability predicate write $\square A={\mathrm{Pr}}_T(┌A┐)$. The conditions are: if $T⊢A$ then $T⊢\square A$; $T⊢\square (A\to B)\to (\square A\to \square B)$; and $T⊢\square A\to \square \square A$. The first is an external rule, while the latter two are internal theorems. They formalize proof verification, closure under modus ponens rule and positive introspection. None licenses reflection from a proved sentence $\square A$ to $A$.