On strong provability predicates and the associated modal logics

Abstract

Abstract PA is Peano Arithmetic. Pr( x ) is the usual Σ 1 ,-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ 1 . An example: Q is ω -provable if PA + ¬ Q is ω -inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω -provability and obtained its arithmetical completeness. In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig interpolation lemma. We also consider other examples of the strong provability predicates and their applications.