We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment (...) of GLP Λ. (shrink)

For any ordinal $\Lambda$, we can define a polymodal logic $\mathsf{GLP}_\Lambda$, with a modality $[\xi]$ for each $\xi < \Lambda$. These represent provability predicates of increasing strength. Although $\mathsf{GLP}_\Lambda$ has no Kripke models, Ignatiev showed that indeed one can construct a Kripke model of the variable-free fragment with natural number modalities, denoted $\mathsf{GLP}^0_\omega$. Later, Icard defined a topological model for $\mathsf{GLP}^0_\omega$ which is very closely related to Ignatiev's. In this paper we show how to extend these constructions for arbitrary $\Lambda$. (...) More generally, for each $\Theta,\Lambda$ we build a Kripke model $\mathfrak I^\Theta_\Lambda$ and a topological model $\mathfrak T^\Theta_\Lambda$, and show that $\mathsf{GLP}^0_\Lambda$ is sound for both of these structures, as well as complete, provided $\Theta$ is large enough. (shrink)

Ordinal functions may be iterated transfinitely in a natural way by taking pointwise limits at limit stages. However, this has disadvantages, especially when working in the class of normal functions, as pointwise limits do not preserve normality. To this end we present an alternative method to assign to each normal function f a family of normal functions Hyp[f]=〈fξ〉ξ∈OnHyp[f]=〈fξ〉ξ∈On, called its hyperation, in such a way that f0=idf0=id, f1=ff1=f and fα+β=fα∘fβfα+β=fα∘fβ for all α, β.Hyperations are a refinement of the Veblen hierarchy (...) of f. Moreover, if f is normal and has a well-behaved left-inverse g called a left adjoint, then g can be assigned a cohyperationcoH[g]=〈gξ〉ξ∈OncoH[g]=〈gξ〉ξ∈On, which is a family of initial functions such that gξgξ is a left adjoint to fξfξ for all ξ. (shrink)

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)

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)

The provability logic of a theory T captures the structural behavior of formalized provability in T as provable in T itself. Like provability, one can formalize the notion of relative interpretability giving rise to interpretability logics. Where provability logics are the same for all moderately sound theories of some minimal strength, interpretability logics do show variations.The logic IL is defined as the collection of modal principles that are provable in any moderately sound theory of some minimal strength. In this article (...) we raise the previously known lower bound of IL by exhibiting two series of principles which are shown to be provable in any such theory. Moreover, we compute the collection of frame conditions for both series. (shrink)

Turing progressions have been often used to measure the proof-theoretic strength of mathematical theories: iterate adding consistency of some weak base theory until you “hit” the target theory. Turing progressions based on n-consistency give rise to a \ proof-theoretic ordinal \ also denoted \. As such, to each theory U we can assign the sequence of corresponding \ ordinals \. We call this sequence a Turing-Taylor expansion or spectrum of a theory. In this paper, we relate Turing-Taylor expansions of sub-theories (...) of Peano Arithmetic to Ignatiev’s universal model for the closed fragment of the polymodal provability logic \. In particular, we observe that each point in the Ignatiev model can be seen as Turing-Taylor expansions of formal mathematical theories. Moreover, each sub-theory of Peano Arithmetic that allows for a Turing-Taylor expansion will define a unique point in Ignatiev’s model. (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.

Vardanyan’s Theorems [36, 37] state that $\mathsf {QPL}(\mathsf {PA})$ —the quantified provability logic of Peano Arithmetic—is $\Pi ^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge [38] generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf (...) {QRC_1}$ was previously introduced by the authors [1] as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf {QRC_1}$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf {QRC_1}$ is the strictly positive fragment of $\mathsf {QGL}$ and a fragment of $\mathsf {QPL}(\mathsf {PA})$. (shrink)

By Solovay’s celebrated completeness result [31] on formal provability we know that the provability logic ${\textbf {GL}}$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable axiomatisation. Japaridze generalised this result in [22] by considering a polymodal version ${\mathsf {GLP}}$ of ${\textbf {GL}}$ with modalities $[n]$ for each natural number n referring to ever increasing notions of provability. Modern treatments of ${\mathsf {GLP}}$ tend to interpret the $[n]$ provability notion as “provable in (...) a base theory T together with all true $\Pi ^0_n$ formulas as oracles.” In this paper we generalise this interpretation into the transfinite. In order to do so, a main difficulty to overcome is to generalise the syntactical characterisations of the oracle formulas of complexity $\Pi ^0_n$ to the hyper-arithmetical hierarchy. The paper exploits the fact that provability is $\Sigma ^0_1$ complete and that similar results hold for stronger provability notions. As such, the oracle sentences to define provability at level $\alpha $ will recursively be taken to be consistency statements at lower levels: provability through provability whence the name of the paper. The paper proves soundness and completeness for the proposed interpretation for a wide class of theories, namely for any theory that can formalise the recursion described above and that has some further very natural properties. Some remarks are provided on how the recursion can be formalised into second order arithmetic and on lowering the proof-theoretical strength of these systems of second order arithmetic. (shrink)

Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”.For a set of formulas Γ, define predicative oracle reflection for T over Γ ) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then$$\forall \,\lambda (...) < {\rm{\Lambda }}\,.$$In particular, define predicative oracle consistency ) as Pred–O–RFN{0=1}.Our main result is as follows. Let ATR0 be the second-order theory of Arithmetical Transfinite Recursion, ${\rm{RCA}}_0^{\rm{*}}$ be Weakened Recursive Comprehension and ACA be Arithmetical Comprehension with Full Induction. Then,$${\rm{ATR}}_0 \equiv {\rm{RCA}}_0^{\rm{*}} + {\rm{Pred - O - Cons\ }}\left \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - Cons\ }}\left \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - RFN}}\,_{{\bf{\Pi }}_2^1 } \left.$$We may even replace ${\rm{RCA}}_0^{\rm{*}}$ by the weaker ECA0, the second-order analogue of Elementary Arithmetic.Thus we characterize ATR0, a theory often considered to embody Predicative Reductionism, in terms of strong reflection and consistency principles. (shrink)

The provability logic of a theory $T$ is the set of modal formulas, which under any arithmetical realization are provable in $T$. We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $\Gamma$. We make an analogous modification for interpretability logics. We first study provability logics with restricted realizations and show that for various natural candidates of $T$ and restriction set $\Gamma$, the result is the logic of linear frames. However, for the theory Primitive (...) Recursive Arithmetic (PRA), we define a fragment that gives rise to a more interesting provability logic by capitalizing on the well-studied relationship between PRA and I$\Sigma_1$. We then study interpretability logics, obtaining upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely related to linear frames. The technique is also applied to yield the nontrivial result that IL(PRA) $\subset$ ILM. (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)

The paper presents an exploration of conceptual issues that have arisen in the course of investigating speed-up and slowdown phenomena in small Turing machines, in particular results of a test that may spur experimental approaches to the notion of computational irreducibility. The test involves a systematic attempt to outrun the computation of a large number of small Turing machines (3 and 4 state, 2 symbol) by means of integer sequence prediction using a specialized function for that purpose. The experiment prompts (...) an investigation into rates of convergence of decision procedures and the decidability of sets in addition to a discussion of the (un)predictability of deterministic computing systems in practice. We think this investigation constitutes a novel approach to the discussion of an epistemological question in the context of a computer simulation, and thus represents an interesting exploration at the boundary between philosophical concerns and computational experiments. (shrink)

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 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)

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.

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)

Turing progressions arise by iteratedly adding consistency statements to a base theory. Different notions of consistency give rise to different Turing progressions. In this paper we present a logic that generates exactly all relations that hold between these different Turing progressions given a particular set of natural consistency notions. Thus, the presented logic is proven to be arithmetically sound and complete for a natural interpretation, named the formalized Turing progressions interpretation.

In this paper we will state and prove some comparative theorems concerning PRA and IΣ1. We shall provide a characterization of IΣ1 in terms of PRA and iterations of a class of functions. In particular, we prove that for this class of functions the difference between IΣ1 and PRA is exactly that, where PRA is closed under iterations of these functions, IΣ1 is moreover provably closed under iteration. We will formulate a sufficient condition for a model of PRA to be (...) a model of IΣ1. This condition is used to give a model-theoretic proof of Parsons’ theorem, that is, IΣ1 is Π2-conservative over PRA. We shall also give a purely syntactical proof of Parsons’ theorem. Finally, we show that IΣ1 proves the consistency of PRA on a definable IΣ1-cut. This implies that proofs in IΣ1 can have non-elementary speed up over proofs in PRA. (shrink)

La pratique de la loi assure la vie. Ce principe est martelé tout au long de la Bible hébraïque. Son expression la plus concise se trouve en Lv 18,5 : «Vous observerez mes lois et mes ordonnances : l'homme qui les mettra en pratique vivra par elles ». Cet axiome n'est jamais remis en question, même si un ou deux passages en limitent l'application. La littérature intertestamentaire continue à investir ce thème et le Nouveau Testament le reprend à sa manière. (...) L'enseignement de Jésus s'efforce d'articuler le motif de la loi de vie avec celui de la grâce s'adressant à tous les hommes. Il ne met pas en doute le principe même selon lequel la pratique de la loi mène à la vie. La loi et la grâce se présentent comme des principes complémentaires. (shrink)

L’unité des disciplines théologiques n’est pas toujours facile à percevoir. L’étude des textes bibliques, d’une part, et la réflexion sys­tématique, d’autre part, suivent chacune leur logique et leurs méthodes, pour ne rien dire des disciplines historiques et pratiques ! Afin de répondre à la demande toujours grandissante d’une approche interdisciplinaire, les soussignés, tous deux enseignants à la Faculté de théologie protestante de l’Université Marc Bloch, l’un bibliste, l’autre éthicien, a..

A fast consistency prover is a consistent polytime axiomatized theory that has short proofs of the finite consistency statements of any other polytime axiomatized theory. Krajíček and Pudlák have proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that NP = coNP implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the notion of (...) an unlikely fast consistency prover and prove that its existence is equivalent to NP = coNP. Next it is proved that fast consistency provers do not exist if one considers RE axiomatized theories rather than theories with an axiom set that is recognizable in polynomial time. (shrink)