Proof-theoretic modal PA-completeness. I: A system-sequent metric (Q1970598)

The modal logic \(G\) is axiomatized (over classical propositional logic) by the rule \(A/\square A\) and the axioms \(\square(A\to B)\to (\square A\to \square B)\) and \(\square(\square A\to A)\to \square A\) (Löb's scheme). This logic has been found by \textit{R. M. Solovay} [Isr. J. Math. 25, 287-304 (1976; Zbl 0352.02019)] to formalize the provable propositional properties of the provability predicate for PA (Peano arithmetic). R. M. Solovay gave a semantic proof of the PA-completeness of \(G\). A sequential calculus for \(G\) is obtained by adding the rule \(X\), \(\square X\), \(\square A\vdash A/\square X\vdash\square A\) to the usual sequential calculus for classical propositional logic. The author states the following PA-completeness problem for a modal system \(L\): to find a suitable and if possible minimal class of interpretations \(\{\varphi\}\) so that for any sequent \(S\) in \(L\): \(\vdash_{\text{PA}} S^\varphi\) for each \(\varphi\) implies \(\vdash_L S\), where \(\varphi\) is an application \(\varphi:\{\text{formuas of }L\}\to\{\text{formulas of PA}\}\) which maintains propositional connectives and \(\varphi(\square A)= \text{Pr}_{\text{PA}}(\varphi(A))\). The paper under review is the first part of a series of three articles [Part II is reviewed below] that present the syntactic proof of the PA-completeness of the modal system \(G\). Some proof-theoretic objects are introduced, which also have an independent interest, and this fact has caused the subdivision into three parts. If a sequent \(S\) is not a \(G\)-theorem, the author proves that there is a canonical characteristic formula \(H\) of \(S\) which expresses the non-\(G\)-provability of \(S\), and he defines the notion of a syntactic metric \(d(S, G)\) as the complexity of a formula \(\sim H\). Furthermore, the tree-function \(F\) associated to a proof-tree \({\mathcal P}\) and the arithmetical \({\mathcal P}\)-interpretation of a modal sequent \(S\) are defined.