arXiv subjects
Publications and source records attributed to Joost J. Joosten.
In is paper we present a labelled tableau proof system that serves a wide class of interpretability logics. The system is proved sound and complete for any interpretability logic characterised by a frame condition given by a set of universal strict first order Horn sentences. As such, the current paper adds to a better proof-theoretical understanding of interpretability logics.
This paper deals with three tools to compare proof-theoretic strength of formal arithmetical theories: interpretability, $Π^0_1$-conservativity and proving restricted consistency. It is well known that under certain conditions these three notions are equivalent and this equivalence is often referred to as the Orey-Hájek characterization of interpretability. In this paper we look with detail at the Orey-Hájek characterization and study what conditions are needed and in what meta-theory the characterizations can be formalized.
Turing progressions have been often used to measure the proof-theoretic strength of mathematical theories. Turing progressions based on $n$-provability give rise to a $Π_{n+1}$ proof-theoretic ordinal. As such, to each theory $U$ we can assign the sequence of corresponding $Π_{n+1}$ ordinals $\langle |U|_n\rangle_{n>0}$. We call this sequence a \emph{Turing-Taylor expansion} 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 ${\mathbf{GLP}}_ω$. In particular, in this first draft 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 expression will define a unique point in Ignatiev's model.
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(All) is defined as the collection of modal principles that are provable in any moderately sound theory of some minimal strength. In this paper we raise the previously known lower bound of IL(All) 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.
Fixing some computably enumerable theory $T$, the Friedman-Goldfarb-Harrington (FGH) theorem says that over elementary arithmetic, each $Σ_1$ formula is equivalent to some formula of the form $\Box_T φ$ provided that $T$ is consistent. In this paper we give various generalizations of the FGH theorem. In particular, for $n>1$ we relate $Σ_{n}$ formulas to provability statements $[n]_T^{\sf True}φ$ which are a formalization of "provable in $T$ together with all true $Σ_{n+1}$ sentences". As a corollary we conclude that each $[n]_T^{\sf True}$ is $Σ_{n+1}$-complete. This observation yields us to consider a recursively defined hierarchy of provability predicates $[n+1]^\Box_T$ which look a lot like $[n+1]_T^{\sf True}$ except that where $[n+1]_T^{\sf True}$ calls upon the oracle of all true $Σ_{n+2}$ sentences, the $[n+1]^\Box_T$ recursively calls upon the oracle of all true sentences of the form $\langle n \rangle_T^\Boxϕ$. As such we obtain a `syntax-light' characterization of $Σ_{n+1}$ definability whence of Turing jumps which is readily extended beyond the finite. Moreover, we observe that the corresponding provability predicates $[n+1]_T^\Box$ are well behaved in that together they provide a sound interpretation of the polymodal provability logic ${\sf GLP}_ω$.
Peano Arithmetic is known to be provably equivalent to reflection over Elementary Arithmetic. We prove a characterization of Predicative Analysis in the guise of ATR0 in terms of stronger reflection principles.
The principle of Generalized Natural Selection (GNS) states that in nature, computational processes of high computational sophistication are more likely to maintain/abide than processes of lower computational sophistication provided that sufficiently many resources are around to sustain the processes. In this paper we give a concrete set-up how to test GNS in a weak sense. In particular, we work in the setting of Cellular Automata and see how GNS can manifest itself in this setting.
This paper studies the transfinite propositional provability logics $\glp_Λ$ and their corresponding algebras. These logics have for each ordinal $ξ< Λ$ a modality $\la α\ra$. We will focus on the closed fragment of $\glp_Λ$ (i.e., where no propositional variables occur) and \emph{worms} therein. Worms are iterated consistency expressions of the form $\la ξ_n\ra \ldots \la ξ_1 \ra \top$. Beklemishev has defined well-orderings $<_ξ$ on worms whose modalities are all at least $ξ$ and presented a calculus to compute the respective order-types. In the current paper we present a generalization of the original $<_ξ$ orderings and provide a calculus for the corresponding generalized order-types $o_ξ$. Our calculus is based on so-called {\em hyperations} which are transfinite iterations of normal functions. Finally, we give two different characterizations of those sequences of ordinals which are of the form $\la {\formerOmega}_ξ(A) \ra_{ξ\in \ord}$ for some worm $A$. One of these characterizations is in terms of a second kind of transfinite iteration called {\em cohyperation.}
We study transfinite extensions of Japaridze's provability logic GLP and the well-founded relations that naturally occur within them. Every ordinal induces a partial order over the class of "words," which are iterated consistency statements expressible within GLP. Well-ordered restrictions of these partial orders have been studied previously; in this paper we consider the unrestricted partial orders, which are no longer linear but remain well-founded. These unrestricted partial orders bear important repercussions on modal semantics for GLP and on Turing progressions.
In this paper we consider transfinite provability logics where for each ordinal in some recursive well-order we have a corresponding modal provability operator. The modality [xi] will be interpreted as "provable in ACA_0 together with at most xi nested applications of the omega rule". We show how to formalize this in in second order number theory. Next we prove both soundness and completeness under this interpretation. We conclude by showing how one can lower the base theory ACA_0 to theories below RCA_0.
Wolfram's Principle of Computational Equivalence (PCE) implies that universal complexity abounds in nature. This paper comprises three sections. In the first section we consider the question why there are so many universal phenomena around. So, in a sense, we week a driving force behind the PCE if any. We postulate a principle GNS that we call the Generalized Natural Selection Principle that together with the Church-Turing Thesis is seen to be equivalent to a weak version of PCE. In the second section we ask the question why we do not observe any phenomena that are complex but not-universal. We choose a cognitive setting to embark on this question and make some analogies with formal logic. In the third and final section we report on a case study where we see rich structures arise everywhere.
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(Λ).
In this paper we introduce hyperations and cohyperations, which are forms of transfinite iteration of ordinal functions. Hyperations are iterations of normal functions. Unlike iteration by pointwise convergence, hyperation preserves normality. The hyperation of a normal function f is a sequence of normal functions so that f^0= id, f^1 = f and for all ordinals α, βwe have that f^(α+ β) = f^αf^β. These conditions do not determine f^αuniquely; in addition, we require that the functions be minimal in an appropriate sense. We study hyperations systematically and show that they are a natural refinement of Veblen progressions. Next, we define cohyperations, very similar to hyperations except that they are left-additive: given α, β, f^(α+ β)= f^βf^α. Cohyperations iterate initial functions which are functions that map initial segments to initial segments. We systematically study cohyperations and see how they can be employed to define left inverses to hyperations. Hyperations provide an alternative presentation of Veblen progressions and can be useful where a more fine-grained analysis of such sequences is called for. They are very amenable to algebraic manipulation and hence are convenient to work with. Cohyperations, meanwhile, give a novel way to describe slowly increasing functions as often appear, for example, in proof theory.
For any ordinal Λ, we can define a polymodal logic GLP(Λ), with a modality [ξ] for each ξ<Λ. These represent provability predicates of increasing strength. Although GLP(Λ) has no Kripke models, Ignatiev showed that indeed one can construct a Kripke model of the variable-free fragment with natural number modalities. Later, Icard defined a topological model for the same fragment which is very closely related to Ignatiev's. In this paper we show how to extend these constructions for arbitrary Λ. More generally, for each Θ,Λwe build a Kripke model I(Θ,Λ) and a topological model T(Θ,Λ), and show that the closed fragment of GLP(Λ) is sound for both of these structures, as well as complete, provided Θis large enough.
Consider three players Alice, Bob and Cath who hold a, b and c cards, respectively, from a deck of d=a+b+c cards. The cards are all different and players only know their own cards. Suppose Alice and Bob wish to communicate their cards to each other without Cath learning whether Alice or Bob holds a specific card. Considering the cards as consecutive natural numbers 0,1,..., we investigate general conditions for when Alice or Bob can safely announce the sum of the cards they hold modulo an appropriately chosen integer. We demonstrate that this holds whenever a,b>2 and c=1. Because Cath holds a single card, this also implies that Alice and Bob will learn the card deal from the other player's announcement.
There are several forms of irreducibility in computing systems, ranging from undecidability to intractability to nonlinearity. This paper is an exploration of the conceptual issues that have arisen in the course of investigating speed-up and slowdown phenomena in small Turing machines. We present the 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 (all 3 and 4 state, 2 symbol) by means of integer sequence prediction using a specialized function finder program. This massive 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.
The aim of this paper is to undertake an experimental investigation of the trade-offs between program-size and time computational complexity. The investigation includes an exhaustive exploration and systematic study of the functions computed by the set of all 2-color Turing machines with 2, 3 and 4 states--denoted by (n,2) with n the number of states--with particular attention to the runtimes and space usages when the machines have access to larger resources (more states). We report that the average runtime of Turing machines computing a function almost surely increases as a function of the number of states, indicating that machines not terminating (almost) immediately tend to occupy all the resources at hand. We calculated all time complexity classes to which the algorithms computing the functions found in both (2,2) and (3,2) belong to, and made a comparison among these classes. For a selection of functions the comparison was extended to (4,2). Our study revealed various structures in the micro-cosmos of small Turing machines. Most notably we observed "phase-transitions" in the halting-probability distribution that we explain. Moreover, it is observed that short initial segments fully define a function computed by a Turing machine.
We start by an introduction to the basic concepts of computability theory and the introduction of the concept of Turing machine and computation universality. Then se turn to the exploration of trade-offs between different measures of complexity, particularly algorithmic (program-size) and computational (time) complexity as a mean to explain these measure in a novel manner. The investigation proceeds by an exhaustive exploration and systematic study of the functions computed by a large set of small Turing machines with 2 and 3 states with particular attention to runtimes, space-usages and patterns corresponding to the computed functions when the machines have access to larger resources (more states). We report that the average runtime of Turing machines computing a function increases as a function of the number of states, indicating that non-trivial machines tend to occupy all the resources at hand. General slow-down was witnessed and some incidental cases of (linear) speed-up were found. Throughout our study various interesting structures were encountered. We unveil a study of structures in the micro-cosmos of small Turing machines.