Arithmetical proof relation (source code)

= Arithmetical proof relation
{title2=$\operatorname{Proof}_T(u,v)$}

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>.