Bi-Modal Logics and Their Arithmetic Interpretations

Abstract

If we have a metamathematical predicate other than provability, yet strong enough (if “strong” is the right word) to satisfy the axioms of PRL, then some of our preceding modal analysis carries over from Pr(·) to the predicate in question. It could happen that the analogue to Solovay’s First Completeness Theorem holds, i.e. that PRL is the logic of the given predicate, or it could happen that additional axioms are required and one must find these and prove completeness. This last is important if we wish to obtain applications like those we made of Solovay’s Second Completeness Theorem in Chapter 3, section 2, above. Even without this, however, we have some applications— particularly, the explicit definability and uniqueness of the fixed points.