A proof theory for the logic of provability in true arithmetic (Q2193977)

The provability logic \(\mathsf{GL}\) (Gödel-Löb) is a simple modal description of provability. The axioms of system \(\mathsf{GL}\) are all tautologies, \(\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B),\) \(\Box (\Box A\rightarrow A)\rightarrow \Box A.\) The inference rules of \(\mathsf{GL}\) are modus ponens and necessitation \(A/ \Box A\). The provability logic \(\mathsf{GL}\) describes completely provability in Peano arithmetic [\textit{R. M. Solovay}, Isr. J. Math. 25, 287--304 (1976; Zbl 0352.02019)]. In that paper, Solovay also provided an axiomatic system \(\mathsf{GLS}\) and proved that provability of a modal formula in \(\mathsf{GLS}\) coincides with truth of its arithmetical interpretations in the standard model of Peano arithmetic. There are a several papers that study proof theory for \(\mathsf{GL}.\) Sequent calculus for the provability logic \(\mathsf{GL}\) is introduced by \textit{G. Sambin} and \textit{S. Valentini} [Stud. Log. 39, 245--256 (1980; Zbl 0457.03016); J. Philos. Log. 11, 311--342 (1982; Zbl 0523.03014)]. A syntactic proof of the cut-elimination theorem for sequent calculus for \(\mathsf{GL}\) was given by \textit{S. Valentini} [J. Philos. Log. 12, 471--476 (1983; Zbl 0535.03031)]. In the paper under review, a sequent calculus for \(\mathsf{GLS}\) is developed. The cut-elimination theorem is proved. Some standard consequences as interpolation and definability theorems are proved, too. As another consequence of cut-elimination, the equivalence of \(\mathsf{GL}\) and \(\mathsf{GLS}\) with respect to a special form of formulas which is called Gödel sentences, using a purely proof-theoretical method is proved.