Abstract

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 for a given arithmetical theory T and a class 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