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)

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.

We investigate the theory IΔ 0 + Ω 1 and strengthen [Bu86. Theorem 8.6] to the following: if NP ≠ co-NP. then Σ-completeness for witness comparison formulas is not provable in bounded arithmetic. i.e. $I\delta_0 + \Omega_1 + \nvdash \forall b \forall c (\exists a(\operatorname{Prf}(a.c) \wedge \forall = \leq a \neg \operatorname{Prf} (z.b))\\ \rightarrow \operatorname{Prov} (\ulcorner \exists a(\operatorname{Prf}(a. \bar{c}) \wedge \forall z \leq a \neg \operatorname{Prf}(z.\bar{b})) \urcorner)).$ Next we study a "small reflection principle" in bounded arithmetic. We prove that for (...) all sentences φ $I\Delta_0 + \Omega_1 \vdash \forall x \operatorname{Prov}(\ulcorner \forall y \leq \bar{x} (\operatorname{Prf} (y. \overline{\ulcorner \varphi \urcorner}) \rightarrow \varphi)\urcorner).$ The proof hinges on the use of definable cuts and partial satisfaction predicates akin to those introduced by Pudlak in [Pu86]. Finally, we give some applications of the small reflection principle, showing that the principle can sometimes be invoked in order to circumvent the use of provable Σ-completeness for witness comparison formulas. (shrink)

One of the main goals of scientific research is to provide a description of the empirical data which is as accurate and comprehensive as possible, while relying on as few and simple assumptions as possible. In this paper, I propose a definition of the notion of few and simple assumptions that is not affected by known problems. This leads to the introduction of a simple model of scientific progress that is based only on empirical accuracy and conciseness. An essential point (...) in this task is the understanding of the role played by measurability in the formulation of a scientific theory. This is the key to prevent artificially concise formulations. The model is confronted here with many possible objections and with challenging cases of real progress. Although I cannot exclude that the model might have some limitations, it includes all the cases of genuine progress examined here, and no spurious one. In this model, I stress the role of the state of the art, which is the collection of all the theories that are the only legitimate source of scientific predictions. Progress is a global upgrade of the state of the art. (shrink)

In this paper we study the interpretations of a weak arithmetic, like Buss’s theory $\mathsf{S}^{1}_{2}$, in a given theory $U$. We call these interpretations the arithmetics of $U$. We develop the basics of the structure of the arithmetics of $U$. We study the provability logic of $U$ from the standpoint of the framework of the arithmetics of $U$. Finally, we provide a deeper study of the arithmetics of a finitely axiomatized sequential theory.

This paper attempts to address the question what logical strength theories of truth have by considering such questions as: If you take a theory T and add a theory of truth to it, how strong is the resulting theory, as compared to T? It turns out that, in a wide range of cases, we can get some nice answers to this question, but only if we work in a framework that is somewhat different from those usually employed in discussions of (...) axiomatic theories of truth. These results are then used to address a range of philosophical questions connected with truth, such as what Tarski meant by "essential richness" and the so-called conservativeness argument against deflationism. -/- This draft dates from about 2009, with some significant updates having been made around 2011. Around then, however, I decided that the paper was becoming unmanageable and that I was trying to do too many things in it. I have therefore exploded the paper into several pieces, which will be published separately. These include "Disquotationalism and the Compositional Principles", "The Logical Strength of Compositional Principles", "Consistency and the Theory of Truth", and "What Is Essential Richness?" You should probably read those instead, since this draft remains a bit of a mess. Terminology and notation are inconsistent, and some of the proofs aren't quite right. So, caveat lector. I make it public only because it has been cited in a few places now. (shrink)

This paper is concerned with the logical structure of arithmetical theories. We survey results concerning logics and admissible rules of constructive arithmetical theories. We prove a new theorem: the admissible propositional rules of Heyting Arithmetic are the same as the admissible propositional rules of Intuitionistic Propositional Logic. We provide some further insights concerning predicate logical admissible rules for arithmetical theories.

For “natural enough” systems of ordinal notation we show that α times iterated local reflection schema over a sufficiently strong arithmetic T proves the same Π 1 0 -sentences as ω α times iterated consistency. A corollary is that the two hierarchies catch up modulo relative interpretability exactly at ε-numbers. We also derive the following more general “mixed” formulas estimating the consistency strength of iterated local reflection: for all ordinals α ⩾ 1 and all β, β ≡ Π 1 0 (...) T ω α · , α ≡ Π 1 0 T β + ω α . Here T α stands for α times iterated local reflection over T , T β stands for β times iterated consistency, and ≡ Π 1 0 denotes mutual Π 1 0 -conservativity. In an appendix to this paper we develop our notion of “natural enough” system of ordinal notation and show that such systems do exist for every recursive ordinal. (shrink)

The notion of a critical successor [5] in relational semantics has been central to most classic modal completeness proofs in interpretability logics. In this paper we shall work with a more general notion, that of an assuring successor. This will enable more concisely formulated completeness proofs, both with respect to ordinary and generalised Veltman semantics. Due to their interesting theoretical properties, we will devote some space to the study of a particular kind of assuring labels, the so‐called full labels and (...) maximal labels. After a general treatment of assuringness, we shall apply it to obtain a completeness result for the modal logic w.r.t. generalised semantics for a restricted class of frames. (shrink)

In this paper, we characterize the strength of the predicative Frege hierarchy, , introduced by John Burgess in his book [J. Burgess, Fixing frege, in: Princeton Monographs in Philosophy, Princeton University Press, Princeton, 2005]. We show that and are mutually interpretable. It follows that is mutually interpretable with Q. This fact was proved earlier by Mihai Ganea in [M. Ganea, Burgess’ PV is Robinson’s Q, The Journal of Symbolic Logic 72 619–624] using a different proof. Another consequence of the our (...) main result is that is mutually interpretable with Kalmar Arithmetic . The fact that interprets EA was proved earlier by Burgess. We provide a different proof. Each of the theories is finitely axiomatizable. Our main result implies that the whole hierarchy taken together, , is not finitely axiomatizable. What is more: no theory that is mutually locally interpretable with is finitely axiomatizable. (shrink)

A theory T is trustworthy iff, whenever a theory U is interpretable in T, then it is faithfully interpretable. In this paper we give a characterization of trustworthiness. We provide a simple proof of Friedman’s Theorem that finitely axiomatized, sequential, consistent theories are trustworthy. We provide an example of a theory whose schematic predicate logic is complete Π20.

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)

One way to study and understand the notion of truth is to examine principles that we are willing to associate with truth, often because they conform to a pre-theoretical or to a semi-formal characterization of this concept. In comparing different collections of such principles, one requires formally precise notions of inter-theoretic reduction that are also adequate to compare these conceptual aspects. In this work I study possible ways to make precise the relation of conceptual equivalence between notions of truth associated (...) with collections of principles of truth. In doing so, I will consider refinements and strengthenings of the notion of relative truth-definability proposed by Fujimoto (2010): in particular I employ suitable variants of notions of equivalence of theories considered in Visser (2006) and Friedman & Visser (2014) to show that there are better candidates than mutual truth-definability for the role of sufficient condition for conceptual equivalence between the semantic notions associated with the theories. In the concluding part of the paper, I extend the techniques introduced in the first and show that there is a precise sense in which ramified truth (either disquotational or compositional) does not correspond to iterations of comprehension. (shrink)

In the paper we investigate typed axiomatizations of the truth predicate in which the axioms of truth come with a built-in, minimal and self-sufficient machinery to talk about syntactic aspects of an arbitrary base theory. Expanding previous works of the author and building on recent works of Albert Visser and Richard Heck, we give a precise characterization of these systems by investigating the strict relationships occurring between them, arithmetized model constructions in weak arithmetical systems and suitable set existence axioms. The (...) framework considered will give rise to some methodological remarks on the construction of truth theories and provide us with a privileged point of view to analyze the notion of truth arising from compositional principles in a typed setting. (shrink)

A generalized Veltman semantics developed by de Jongh is used to investigate correspondences between several extensions of intepretability logic . In this paper we present some new results on independences.

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.

It can be argued that only the equational theories of some sub-elementary function algebras are finitistic or intuitive according to a certain interpretation of Hilbert's conception of intuition. The purpose of this paper is to investigate the relation of those restricted forms of equational reasoning to classical quantifier logic in arithmetic. The conclusion reached is that Edward Nelson's ‘predicative arithmetic’ program, which makes essential use of classical quantifier logic, cannot be justified finitistically and thus requires a different philosophical foundation, possibly (...) as a restricted form of logicism. (shrink)

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted inbut also what cannot be so (...) interpreted. We explain some of these results and rely on them to discuss Nelson's position. (shrink)

We investigate the bimodal logics sound and complete under the interpretation of modal operators as the provability predicates in certain natural pairs of arithmetical theories . Carlson characterized the provability logic for essentially reflexive extensions of theories, i.e. for pairs similar to . Here we study pairs of theories such that the gap between and is not so wide. In view of some general results concerning the problem of classification of the bimodal provability logics we are particularly interested in such (...) pairs that is axiomatized over by ∏1-sentences only, and, for each n 1, proves the n-times iterated consistency of . A complete axiomatization, along with the appropriate Kripke semantics and decision procedures, is found for the two principal cases: finitely axiomatizable extensions of this sort, like e.g. ), ), etc., and reflexive extensions, like ¦n 1\s}), etc. We show that the first logic, ICP, is the minimal and the second one, RP, is the maximal within the class of the provability logics for such pairs of theories. We also show that there are some provability logics lying strictly between these two. As an application of the results of this paper, in the last section the polymodal provability logics for natural recursive progressions of theories based on iteration of consistency are characterized. We construct a system of ordinal notation , which gives exactly one notation to each constructive ordinal, such that the logic corresponding to any progression along coincides with that along natural Kalmar elementary well-orderings. (shrink)

By a result of Paris and Friedman, the collection axiom schema for $\Sigma_{n+1}$ formulas, $B\Sigma_{n+1}$ , is $\Pi_{n+2}$ conservative over $I\Sigma_n$ . We give a new proof-theoretic proof of this theorem, which is based on a reduction of $B\Sigma_n$ to a version of collection rule and a subsequent analysis of this rule via Herbrand's theorem. A generalization of this method allows us to improve known results on reflection principles for $B\Sigma_n$ and to answer some technical questions left open by Sieg (...) [23] and Hájek [9]. We also give a new proof of independence of $B\Sigma_{n+1}$ over $I\Sigma_n$ by a direct recursion-theoretic argument and answer an open problem formulated by Gaifman and Dimitracopoulos [8]. (shrink)