The interpretability logic of a mathematical theory describes the structural behavior of interpretations over that theory. Different theories have different logics. This paper revolves around the question what logic describes the behavior that is present in all theories with a minimum amount of arithmetic; the intersection over all such theories so to say. We denote this target logic by IL.In this paper we present a new principle R in IL. We show that R does not follow from the logic ILP0W* (...) that contains all previously known principles. This is done by providing a modal incompleteness proof of ILP0W*: showing that R follows semantically but not syntactically from ILP0W*. Apart from giving the incompleteness proof by elementary methods, we also sketch how to work with so-called Generalized Veltman Semantics as to establish incompleteness. To this extent, a new version of this Generalized Veltman Semantics is defined and studied. Moreover, for the important principles the frame correspondences are calculated.After the modal results it is shown that the new principle R is indeed valid in any arithmetically theory. The proof employs some elementary results on definable cuts in arithmetical theories. (shrink)

Solovay's 1976 completeness result for modal provability logic employs the recursion theorem in its proof. It is shown that the uses of the recursion theorem can in this proof replaced by the diagonalization lemma for arithmetic and that, in effect, the proof neatly fits the framework of another, enriched, system of modal logic so that any arithmetical system for which this logic is sound is strong enough to carry out the proof, in particular $\text{I}\Delta _{0}+\text{EXP}$ . The method is adapted (...) to obtain a similar completeness result for the Rosser logic. (shrink)

In this paper, we study IL(), the interpretability logic of . As is neither an essentially reflexive theory nor finitely axiomatizable, the two known arithmetical completeness results do not apply to : IL() is not or . IL() does, of course, contain all the principles known to be part of IL, the interpretability logic of the principles common to all reasonable arithmetical theories. In this paper, we take two arithmetical properties of and see what their consequences in the modal logic (...) IL() are. These properties are reflected in the so-called Beklemishev Principle , and Zambella’s Principle , neither of which is a part of IL. Both principles and their interrelation are submitted to a modal study. In particular, we prove a frame condition for . Moreover, we prove that follows from a restricted form of . Finally, we give an overview of the known relationships of IL() to important other interpretability principles. (shrink)

Each closed (i.e. variable free) formula of interpretability logic is equivalent in ILF to a closed formula of the provability logic G, thus to a Boolean combination of formulas of the form n.

PA is Peano arithmetic. The formula $\operatorname{Interp}_\mathrm{PA}(\alpha, \beta)$ is a formalization of the assertion that the theory PA + α interprets the theory PA + β (the variables α and β are intended to range over codes of sentences of PA). We extend Solovay's modal analysis of the formalized provability predicate of PA, Pr PA (x), to the case of the formalized interpretability relation $\operatorname{Interp}_\mathrm{PA}(x, y)$ . The relevant modal logic, in addition to the usual provability operator `□', has a (...) binary operator ` $\triangleright$ ' to be interpreted as the formalized interpretability relation. We give an axiomatization and a decision procedure for the class of those modal formulas that express valid interpretability principles (for every assignment of the atomic modal formulas to sentences of PA). Our results continue to hold if we replace the base theory PA with Zermelo-Fraenkel set theory, but not with Gödel-Bernays set theory. This sensitivity to the base theory shows that the language is quite expressive. Our proof uses in an essential way earlier work done by A. Visser, D. de Jongh, and F. Veltman on this problem. (shrink)

Within the technical frame supplied by the algebraic variety of diagonalizable algebras, defined by R. Magari in [2], we prove the following: Let T be any first-order theory with a predicate Pr satisfying the canonical derivability conditions, including Löb's property. Then any formula in T built up from the propositional variables $q,p_{1},...,p_{n}$ , using logical connectives and the predicate Pr, has the same "fixed-points" relative to q (that is, formulas $\psi (p_{1},...,p_{n})$ for which for all $p_{1},...,p_{n}\vdash _{T}\phi (\psi (p_{1},...,p_{n}),p_{1},...,p_{n})\leftrightarrow \psi (...) (p_{1},...,p_{n})$ ) of a formula $\phi ^{\ast}$ of the same kind, obtained from φ in an effective way. Moreover, such $\phi ^{\ast}$ is provably equivalent to the formula obtained from φ substituting with $\phi ^{\ast}$ itself all the occurrences of q which are under Pr. In the particular case where q is always under Pr in φ, $\phi ^{\ast}$ is the unique (up to provable equivalence) "fixed-point" of φ. Since this result is proved only assuming Pr to be canonical, it can be deduced that Löb's property is, in a sense, equivalent to Gödel's diagonalization lemma. All the results are proved more generally in the intuitionistic case. (shrink)

It is shown that the propositional modal logic IRM (interpretability logic with Montagna's principle and with witness comparisons in the style of Guaspari's and Solovay's logicR) is sound and complete as the logic ofII 1-conservativity over each∑ 1-sound axiomatized theory containingI∑ 1. The exact statement of the result uses the notion of standard proof predicate. This paper is an immediate continuation of our paper [HM]. Knowledge of [HM] is presupposed. We define a modal logic, called IRM, which includes both ILM (...) andR (the logic of [GS]) and prove an arithmetical completeness theorem in the style of [GS], thus showing that IRM is the logic ofII 1-conservativity with witness comparisons. The reader is recommended to have Smoryński's book [Sm] at his/her disposal. (shrink)

This paper studies a propositional logic which is obtained by interpreting implication as formal provability. It is also the logic of finite irreflexive Kripke Models.A Kripke Model completeness theorem is given and several completeness theorems for interpretations into Provability Logic and Peano Arithmetic.

This paper is a presentation of astatus quæstionis, to wit of the problemof the interpretability logic of all reasonablearithmetical theories.We present both the arithmetical side and themodal side of the question.Dedicated to Dick de Jongh on the occasion of his 60th birthday.

Let PLω be the provability logic of IΔ0 + ω1. We prove some containments of the form L ⊆ PLω < Th(C) where L is the provability logic of PA and Th(C) is a suitable class of Kripke frames.

Solovay's 1976 completeness result for modal provability logic employs the recursion theorem in its proof. It is shown that the uses of the recursion theorem can in this proof be replaced by the diagonalization lemma for arithmetic and that, in effect, the proof neatly fits the framework of another, enriched, system of modal logic (the so-called Rosser logic of Gauspari-Solovay, 1979) so that any arithmetical system for which this logic is sound is strong enough to carry out the proof, in (...) particular I0+EXP. The method is adapted to obtain a similar completeness result for the Rosser logic. (shrink)

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. (shrink)

A well-known polymodal provability logic inlMMLBox due to Japaridze is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic. This system plays an important role in some recent applications of provability algebras in proof theory. However, an obstacle in the study of inlMMLBox is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for inlMMLBox . First, we isolate a certain subsystem inlMMLBox (...) of inlMMLBox that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for inlMMLBox are defined as the limits of chains of finite expansions of models for inlMMLBox . The techniques involves unions of n -elementary chains and inverse limits of Kripke models. All the results are obtained by purely modal-logical methods formalizable in elementary arithmetic. (shrink)

We show that the modal prepositional logicILM (interpretability logic with Montagna's principle), which has been shown sound and complete as the interpretability logic of Peano arithmetic PA (by Berarducci and Savrukov), is sound and complete as the logic ofπ 1-conservativity over eachbE 1-sound axiomatized theory containingI⌆ 1 (PA with induction restricted tobE 1-formulas). Furthermore, we extend this result to a systemILMR obtained fromILM by adding witness comparisons in the style of Guaspari's and Solovay's logicR (this will be done in a (...) separate continuation of the present paper). (shrink)

We characterize the bimodal provability logics for certain natural (classes of) pairs of recursively enumerable theories, mostly related to fragments of arithmetic. For example, we shall give axiomatizations, decision procedures, and introduce natural Kripke semantics for the provability logics of (IΔ 0 + EXP, PRA); (PRA, IΣ 1 ); (IΣ m , IΣ n ) for $1 \leq m etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants.

In this paper we carry out a comparative study of $\mathrm{I}\Sigma_1$ and PRA. We will in a sense fully determine what these theories have to say about each other in terms of provability and interpretability. Our study will result in two arithmetically complete modal logics with simple universal models.

In this paper we carry out a comparative study of and PRA. We will in a sense fully determine what these theories have to say about each other in terms of provability and interpretability. Our study will result in two arithmetically complete modal logics with simple universal models.

We study the arithmetical schema asserting that every eventually decreasing elementary recursive function has a limit. Some other related principles are also formulated. We establish their relationship with restricted parameter-free induction schemata. We also prove that the same principle, formulated as an inference rule, provides an axiomatization of the Σ2-consequences of IΣ1.Using these results we show that ILM is the logic of Π1-conservativity of any reasonable extension of parameter-free Π1-induction schema. This result, however, cannot be much improved: by adapting a (...) theorem of D. Zambella and G. Mints we show that the logic of Π1-conservativity of primitive recursive arithmetic properly extends ILM.In the third part of the paper we give an ordinal classification of -consequences of the standard fragments of Peano arithmetic in terms of reflection principles. This is interesting in view of the general program of ordinal analysis of theories, which in the most standard cases classifies Π-classes of sentences. (shrink)