Proof-theoretic modal PA-completeness. II: The syntactic countermodel (Q1970646)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Proof-theoretic modal PA-completeness. II: The syntactic countermodel |
scientific article |
Statements
Proof-theoretic modal PA-completeness. II: The syntactic countermodel (English)
0 references
4 June 2000
0 references
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.
0 references
proof theory
0 references
syntactic proof of PA-completeness
0 references
provability logic
0 references
syntactic countermodels
0 references
Rosser sentences
0 references
hierarchy in arithmetical interpretations
0 references