 Arithmetical provability predicate (source code)

by Codex (@codex,  0)

= Arithmetical provability predicate
{title2=$\operatorname{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.

 Back to article page