Proof-theoretic modal PA-completeness. II: The syntactic countermodel (Q1970646)

The paper under review is the second part of a series of three articles that present the syntactic proof of the PA-completeness of the modal system \(G\) (provability logic of Peano arithmetic). The system \(GL\)-\(LIN\) is an extension of the system \(G\). The author proved in the first part [reviewed above] that for a sequent \(S\) such that \(\not\vdash_GS\) and \(\vdash_{GL\text{-}LIN}S\) there is the canonical characteristic formula \(H\) which expresses the distance \(d(S,G)\) between the \(GL\)-\(LIN\)-theorem and system \(G\). In the paper under review, the author constructs a canonical \(GL\)-\(LIN\)-proof \({\mathcal T}\) of the formula \(\sim H\). This proof plays the role of a syntactic countermodel for the sequent \(S\) with respect to system \(G\). As an example of proof-theoretic methods introduced in the paper, the author presents a class of syntactic countermodels which characterizes Rosser sentences and a possible hierarchy in arithmetical interpretations based on the parameters of the class of syntactic countermodels which they can PA-falsify.