A smart child of Peano’s

Abstract

We calculate the provability logic of a special form of the Fefer- man provability predicate together with the usual provability predicate of Peano Arithmetic. In other words, we construct a bimodal system with the intended interpretation of the expression ☐φ being as usual the formalizastion of φ is provable in PA” and the new modal operator Δ standing, when applied to φ, for “there exists an x s.t. IΣx is consistent and proves φ”. The new system is called LF. We construct a Kripke semantics for LF and prove the arithmetical completeness theorem for this system. A small number of other issues concerning the Feferman predicate, such as uniqueness of godel- sentences for Δ, is also considered. © 1994 Duke University Press.