The predicate modal logic of provability (Q800346)

QGL is the obvious predicate extension of the propositional modal logic GL which is PA-complete, that is complete for the interpretation of necessity as provability in the first order arithmetic PA. It is proved that several good properties of GL do not extend to QGL. It is not PA-complete, the counterexample being of the form \(\diamond\underline T\to\diamond \diamond t,\) where \(t\) is the constant truth, and \(\bar{T}\) is the only axiom of a consistent theory \(T\) such that PA proves \(Con(T)\to Con(PA+Con(PA)).\) To demonstrate the unprovability of the above formula in QGL, a Kripke countermodel is constructed and the completeness of QGL with respect to a suitable class of Kripke models (with transitive and reversely well-founded accessibility relation) is used. On the other hand, the formula \(\neg (\exists u\diamond P(u)\wedge\forall v\exists w\square (P(v)\to\square P(w)))\) is valid in all transitive and reversely well-founded frames, but unprovable in QGL, so QGL is not complete with respect to any class of frames. Propositional provability logics of all \(\Sigma_ 1\) sound r.e. extensions of PA coincide with GL. The formula \(\diamond\underline T\to\diamond \diamond t,\) where \(T\) is a finitely axiomatizable subtheory of ZF strong enough to construct the model of PA (so that PA proves \(Con(T)\to Con(PA+Con(PA))),\) is PA-valid but not ZF-valid. The fixed point theorem fails for QGL: there is no sentence \(B\) such that \(B\leftrightarrow\forall u\exists v\square (B\to P(u,v))\). Familiar proof for GL cannot be extended, since the substitution rule \(D\to (B\leftrightarrow C)/\square D\to (A(B)\leftrightarrow A(C)),\) when substituted occurrences are modalized, fails if some free variables of \(D\) are bound in \(A\). If the latter obstacle is removed, the proof goes through, which proves the uniqueness of fixed points in QGL and in PA. Several problems are formulated.