Provability logics with quantifiers on proofs Original Research Article

We study here extensions of the Artemovʹs logic of proofs in the language with quantifiers on proof variables. Since the provability operator □A could be expressed in this language by the formula ∃u[u]A, the corresponding logic naturally extends the well-known modal provability logic GL. Besides, the presence of quantifiers on proofs allows us to study some properties of provability not covered by the propositional logics. In this paper we study the arithmetical complexity of the provability logic with quantifiers on proofs View the MathML source for a given arithmetical theory T and a class View the MathML source of proof predicates. In the last section we define Kripke style semantics for the logics corresponding to the standard Gödel proof predicate and its multiple conclusion version.