Guaspari (J Symb Logic 48:777–789, 1983) conjectured that a modal formula is it essentially Σ1 (i.e., it is Σ1 under any arithmetical interpretation), if and only if it is provably equivalent to a disjunction of formulas of the form ${\square{B}}$ . This conjecture was proved first by A. Visser. Then, in (de Jongh and Pianigiani, Logic at Work: In Memory of Helena Rasiowa, Springer-Physica Verlag, Heidelberg-New York, pp. 246–255, 1999), the authors characterized essentially Σ1 formulas of languages including witness comparisons (...) using the interpretability logic ILM. In this note we give a similar characterization for formulas with a binary operator interpreted as interpretability in a finitely axiomatizable extension of IΔ 0 + Supexp and we address a similar problem for IΔ 0 + Exp. (shrink)

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)

Formulas of the propositional modal language with the unary modal operators □, Σ1, 1, Σ2, 2,… are considered as schemata of sentences of arithmetic , where □A is interpreted as “A is PA-provable”, ΣnA as “A is PA-equivalent to a Σn-sentence” and nA as “A is PA-equivalent to a Boolean combination of Σn-sentences”. We give an axiomatization and show decidability of the sets of the modal formulas which are schemata of: PA-provable, true arithmetical sentences.