Artemov, S. N. On modal logics axiomatizing provability. (Russian) Zbl 0598.03012 Izv. Akad. Nauk SSSR, Ser. Mat. 49, No. 6, 1123-1154 (1985). Like in the paper of R. M. Solovay in Isr. J. Math. 25, 287-304 (1976; Zbl 0352.02019) an interpretation * is an assignment of arithmetic sentences to propositional modal formulas such that * preserves logical connectives and \((\square Q)^*\) is \(\Pr (\ulcorner Q^*\urcorner)\) where Pr(\(\cdot)\) is a standard arithmetical formula of provability in PA. The modal representation g(T) of a theory T is the set of propositional formulas Q such that \(T\vdash Q^*\) for all *. So g(T) is the collection of all universal laws of formal provability Pr(\(\cdot)\) which can be deduced by means of theory T. The logics of provability are the values of g(\(\cdot)\); and let LP be the class of all logics of provability. The cardinality of LP is \(2^{\aleph_ 0}\) [the author, Semiotika Inf. 14, 115-133 (1980; Zbl 0463.03006)]. The least logic of provability is \(GL=K+\square (\square p\to p)\to \square p\) [R. M. Solovay, op. cit.]. The paper studies LP and the class L of all extensions of GL. An infinite set of new logics of provability is found. The classification of L is developed on the basis of the notion of trace of a modal formula which is the set of all possible heights of Kripke countermodels for the formula. According to this classification the majority of logics in L are not logics of provability. The decidability of \(GL_{\omega}=GL+\{\neg \square^ n\perp |\) \(n\in \omega \}\) and some other logics of provability is shown. The problem of the entire description of LP is reduced to the problem of description of all logics of provability from the interval between GL and S (Solovay’s logic of all true laws of provability). Cited in 4 ReviewsCited in 5 Documents MSC: 03B45 Modal logic (including the logic of norms) 03F07 Structure of proofs 03F30 First-order arithmetic and fragments 03F50 Metamathematics of constructive systems 03B25 Decidability of theories and sets of sentences Keywords:Kripke models; formal provability; logics of provability; extensions of GL; Solovay’s logic of all true laws of provability Citations:Zbl 0352.02019; Zbl 0463.03006 PDFBibTeX XMLCite \textit{S. N. Artemov}, Izv. Akad. Nauk SSSR, Ser. Mat. 49, No. 6, 1123--1154 (1985; Zbl 0598.03012)