This paper is the second in a series of three papers. All three papers deal with interpretability logics and related matters. In the first paper a construction method was exposed to obtain models of these logics. Using this method, we obtained some completeness results, some already known, and some new. In this paper, we will set the construction method to work to obtain more results. First, the modal completeness of the logic ILM is proved using the construction method. This is (...) not a new result, but by using our new proof we can obtain new results. Among these new results are some admissible rules for ILM and GL. Moreover, the new proof will be used to classify all the essentially Δ1 and also all the essentially Σ1 formulas of ILM. Closely related to essentially Σ1 sentences are the so-called self provers. A self-prover is a formula φ which implies its own provability, that is φ → □φ. Each formula φ will generate a self prover φ ^ □φ. We will use the construction method to characterize those sentences of GL that generate a self prover that is trivial in the sense that it is Σ1. (shrink)

This paper is the first in a series of three related papers on modal methods in interpretability logics and applications. In this first paper the fundaments are laid for later results. These fundaments consist of a thorough treatment of a construction method to obtain modal models. This construction method is used to reprove some known results in the area of interpretability like the modal completeness of the logic IL. Next, the method is applied to obtain new results: the modal completeness (...) of the logic ILMo, and modal completeness of ILW*. (shrink)

In this paper we will be concerned with the interpretability logic of PA and in particular with the fact that this logic, which is denoted by ILM, does not have the interpolation property. An example for this fact seems to emerge from the fact that ILM cannot express Σ₁-ness. This suggests a way to extend the expressive power of interpretability logic, namely, by an additional operator for Σ₁-ness, which might give us a logic with the interpolation property. We will formulate (...) this extension, give an axiomatization which is modally complete and arithmetically complete (although for proofs of these theorems we refer to an earlier paper), and investigate interpolation. We show that this logic still does not have the interpolation property. (shrink)