
Properties of Selector Proofs
A serial property is a suitably enumerated sequence $\{F_n\}$ of formulas and is called selector provable in PA if there is a PA-recursive function $s(x)$ such that PA $\vdash \forall x (s(x){:}_{\text{PA}} \ulcorner F_x\urcorner)$ where $x{:}_{\text{PA}} y$ is a suitable proof predicate. These notions were introduced by Artemov in his analysis of consistency and the formalisation of metamathematics. These matters aside, the notion is intimately connected with that of relative consistency.
Th…