On arithmetical completeness of the logic of proofs (Q1625591): Difference between revisions

\textit{S. N. Artemov} introduced the logic of proofs \(\mathsf{LP}\) [Bull. Symb. Log. 7, No. 1, 1--36 (2001; Zbl 0980.03059)]. The logic of proofs \(\mathsf{LP}\) includes several modal-like operators that allow formulas of the form \(t:X\) (intuitively meaning that term \(t\) is a proof for formula \(X\)). The logic \(\mathsf{LP}\) without the axiom necessitation rule is denoted by \(\mathsf{LP}_0.\) Artemov [loc. cit.] proved the arithmetical completeness theorem of \(\mathsf{LP}_0\). A stronger version of Artemov's arithmetical completeness of the \(\mathsf{LP}_0\) is proved in the paper under review. Moreover, the authors prove a version of the uniform arithmetical completeness theorem of \(\mathsf{LP}_0,\) i.e.\ there exist a \(\Sigma_1\) proof predicate \(\mathsf{Prf}(x,y)\) and an arithmetical interpretation \(\ast\) based on \(\mathsf{Prf}\) such that for any \(\mathsf{LP}\)-formula \(F\), \(\mathsf{LP}_0\vdash F\) if and only if \(PA\vdash F^\ast\).