On modal logics axiomatizing provability. (Russian) Zbl 0598.03012

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).


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