Provability logics with quantifiers on proofs
by
Rostislav Yavorsky
Steklov Mathematical Institute, Moscow, Russia

Propositional logics of explicit provability were introduced and studied by S.N.Artemov in his papers of 1994-1999. All these logics are shown to be decidable and complete with respect to their intended semantics. The aim of our work is to estimate the complexity of the extensions of these logics in the language qLP with quantifiers on the proof variables.

The language qLP contains propositional letters and constants, proof variables, boolean connectives, quantifiers on the proof variables and the bynary operator x:F for the relation ``x is a proof of a formula F''.

An arithmetical interpretation * is defined in the standard way. It assigns arithmetical sentences to propositional variables, commutes with the boolean connectives and quantifiers and (x:F)^* = Prf (x, F^* ) for the fixed proof predicate Prf. Given an arithmetical theory T and a class of proof predicates K we define the logic qLP_K(T) as a set of all qLP-formulas that are provable in T under every arithmetical interpretation based on proof predicates from K.

Theorem. Let T be \omega-consistent extension of Peano Arithmetic. Then for the both classes of all proof predicates and of all functional proof predicates the closed (letterless) fragment of qLP_K(T) is \Pi₂ in T hard.

Date received: March 1, 1999

Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-13.