Provability Logics with Quantifiers on Proofs

Rostislav Yavorsky

The language qLP of the provability logic with quantifiers on proofs contains propositional letters, proof variables, boolean connectives, quantifiers over the proof variables and binary proof operator x : F (“x is a proof of the formula F ”) introduced by S.N.Artemov in [1].

This language naturally extends the language of the logic of proofs considered in [1]. The operational properties of provability studied in [2] could be expressed in this language by the corresponding quantified sentences:

\begin{matrix}∀x∀y∃z(x : (A → B) → (y : A → z : B)), \\ ∀x∃y(x : A → y : (x : A)), etc. \end{matrix}

Also, this language may be considered as an extension of the propositional modal language, since the modal provability operator □A could be expressed by the formula ∃x(x : A).

An arithmetical interpretation ∗ assigns arithmetical sentences to propositional variables, commutes with boolean connectives and quantifiers and (x : A)^{∗} = P rf(x, ⌈A^{∗}⌉). (We suppose that the set of proof variables coincides with the set of individual variables in arithmetic.)

Given an arithmetical theory T and a class of proof predicates K we define the logic qLP_{K}(T) as the set of all formulas in the language qLP, which are provable in T under every arithmetical interpretation ∗ based on proof predicates from K.

We present recent results concerning the decidability and arithmetical complexity of the corresponding logics for different T and K. It turned out that for many natural classes K the logic qLP_{K}(P A) is Π_{2}^{0}- hard. For the case of the Gödel proof predicate decidable fragments were found.

[1] S. Artemov, Logic of Proofs. APAL, 67 (1994), pp. 29–59.

[2] S. Artemov, Explicit provability: the intended semantics for intuitionistic and modal logic. Techn. Rep. 98–10. MSI, Cornell University, 1998.

Address: Steklov Mathematical Institute, Moscow, Gubkina, 8, 117966, RUSSIA

E-mail: rey@mi.ras.ru