Provability logics with quantifiers on proofs (Q5957922)

The system GL (Gödel-Löb) is a modal propositional logic. It is the provability logic of Peano arithmetic. The axioms of system GL are all tautologies, \(\square (A\rightarrow B)\rightarrow (\square A\rightarrow \square B),\) \(\square (\square A\rightarrow A)\rightarrow \square A.\) The inference rules of GL are modus ponens and necessitation \(A/ \square A.\) Provability logic is a modal description of the provability predicate. \textit{S. Artëmov} [Ann. Pure Appl. Logic 67, 29-59 (1994; Zbl 0796.03029)] defined the logic of proofs and proved completeness theorems with respect to the arithmetical interpretation. There are two different ways of introducing quantifiers into the language of the logic of proofs. The first way is to extend the set of atomic formulas by predicate symbols and introduce individual variables and quantifiers on them. In the paper under review the author consider another kind of first-order extensions of the logic of proofs. He allows quantifiers on proof variables. The language of the provability logic with quantifiers on proofs (or \(q \mathcal L \mathcal P\)) contains propositional constants, propositional variables, proof constants, proof variables, Boolean connectives, quantifiers on proof variables and the proof operator of the type [\textsl{term}]\textsl{formula}. Here \textsl{term} is either a proof constant or a proof variable. The intended semantics for a formula \([t] F\) is ``\(t\) is a proof of \(F\)''. The provability operator \(\square A\) could be expressed in this language by the formula \(\exists u [u]A,\) the corresponding logic naturally extends the system GL. Quantifiers on proofs allows us to study some properties of provability not covered by the propositional logic (e.g., we can express the separability property of the multi-conclusion version of Gödel's proof predicate and infiniteness of the set of proofs for a given provable formula). In the paper under review the author studies the arithmetical complexity of the provability logic with quantifiers on proofs \(q {\mathcal LP}_{\mathcal K}(T)\) for a given arithmetical theory \(T\) containing Peano arithmetic and a class \(\mathcal K\) of proof predicates. It is shown that the logic \(q {\mathcal LP}_{\mathcal K}(T)\) is not effectively axiomatizable for different classes \(\mathcal K\) of proof predicates. The author defines Kripke-style semantics for the logic corresponding to the standard Gödel proof predicate and its multi-conclusion version.