BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Michael Rathjen

Michael Rathjen appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
math.LOLogic in Computer Sciencemath.CO

Catalog footprint

What is connected

12works
3topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

12 published item(s)

preprint2020arXiv

Minimal bad sequences are necessary for a uniform Kruskal theorem

The minimal bad sequence argument due to Nash-Williams is a powerful tool in combinatorics with important implications for theoretical computer science. In particular, it yields a very elegant proof of Kruskal's theorem. At the same time, it is known that Kruskal's theorem does not require the full strength of the minimal bad sequence argument. This claim can be made precise in the framework of reverse mathematics, where the existence of minimal bad sequences is equivalent to a principle known as $Π^1_1$-comprehension, which is much stronger than Kruskal's theorem. In the present paper we give a uniform version of Kruskal's theorem by relativizing it to certain transformations of well partial orders. We show that $Π^1_1$-comprehension is equivalent to our uniform Kruskal theorem (over $\mathbf{RCA}_0$ together with the chain-antichain principle). This means that any proof of the uniform Kruskal theorem must entail the existence of minimal bad sequences. As a by-product of our investigation, we obtain uniform proofs of several Kruskal-type independence results.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Classifying the provably total set functions of KP and KP(P)

This article is concerned with classifying the provably total set-functions of Kripke-Platek set theory, KP, and Power Kripke-Platek set theory, KP(P), as well as proving several (partial) conservativity results. The main technical tool used in this paper is a relativisation technique where ordinal analysis is carried out relative to an arbitrary but fixed set x. A classic result from ordinal analysis is the characterisation of the provably recursive functions of Peano Arithmetic, PA, by means of the fast growing hierarchy [10]. Whilst it is possible to formulate the natural numbers within KP, the theory speaks primarily about sets. For this reason it is desirable to obtain a characterisation of its provably total set functions. We will show that KP proves the totality of a set function precisely when it falls within a hierarchy of set functions based upon a relativised constructible hierarchy stretching up in length to any ordinal below the Bachmann-Howard ordinal. As a consequence of this result we obtain that IKP + forall x,y (x in y or x not in y) is conservative over KP for forall-exists-formulae, where IKP stands for intuitionistic Kripke-Platek set theory. In a similar vein, utilising [56], it is shown that KP(P) proves the totality of a set function precisely when it falls within a hierarchy of set functions based upon a relativised von Neumann hierarchy of the same length. The relativisation technique applied to KP(P) with the global axiom of choice, AC-global, also yields a parameterised extension of a result in [58], showing that KP(P) + AC-global is conservative over KP(P) + AC and CZF + AC for Pi_2 in powerset statements. Here AC stands for the ordinary axiom of choice and CZF refers to constructive Zermelo-Fraenkel set theory.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory

Until the 1970s, proof theoretic investigations were mainly concerned with theories of inductive definitions, subsystems of analysis and finite type systems. With the pioneering work of Gerhard Jaeger in the late 1970s and early 1980s, the focus switched to set theories, furnishing ordinal-theoretic proof theory with a uniform and elegant framework. More recently it was shown that these tools can even sometimes be adapted to the context of strong axioms such as the powerset axiom, where one does not attain complete cut elimination but can nevertheless extract witnessing information and characterize the strength of the theory in terms of provable heights of the cumulative hierarchy. Here this technology is applied to intuitionistic Kripke-Platek set theories IKP(P) and IKP(E), where the operation of powerset and exponentiation, respectively, is allowed as a primitive in the separation and collection schemata. In particular, IKP(P) proves the powerset axiom whereas IKP(E) proves the exponentiation axiom. The latter expresses that given any sets A and B, the collection of all functions from A to B is a set, too. While IKP(P) can be dealt with in a similar vein as its classical cousin, the treatment of IKP(E) posed considerable obstacles. One of them was that in the infinitary system the levels of terms become a moving target as they cannot be assigned a fixed level in the formal cumulative hierarchy solely based on their syntactic structure. As adumbrated in an earlier paper, the results of this paper are an important tool in showing that several intuitionistic set theories with the collection axiom possess the existence property, i.e., if they prove an existential theorem then a witness can be provably described in the theory, one example being intuitionistic Zermelo-Fraenkel set theory with bounded separation.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Remarks on Barr's theorem: Proofs in geometric theories

A theorem, usually attributed to Barr, yields that (A) geometric implications deduced in classical L_{\inftyω} logic from geometric theories also have intuitionistic proofs. Barr's theorem is of a topos-theoretic nature and its proof is non-constructive. In the literature one also finds mysterious comments about the capacity of this theorem to remove the axiom of choice from derivations. This article investigates the proof-theoretic side of Barr's theorem and also aims to shed some light on the axiom of choice part. More concretely, a constructive proof of the Hauptsatz for L_{\inftyω} is given and is put to use to arrive at a simple proof of (A) that is formalizable in constructive set theory and Martin-Loef type theory.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

An order-theoretic characterization of the Howard-Bachmann-hierarchy

In this article we provide an intrinsic characterization of the famous Howard-Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees with respect to a homeomorphic embeddability relation. We use our calculations to draw some conclusions about some corresponding subsystems of second order arithmetic. All these subsystems deal with versions of light-face $Π^1_1$-comprehension

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

On the Constructive Dedekind Reals

In order to build the collection of Cauchy reals as a set in constructive set theory, the only Power Set-like principle needed is Exponentiation. In contrast, the proof that the Dedekind reals form a set has seemed to require more than that. The main purpose here is to show that Exponentiation alone does not suffice for the latter, by furnishing a Kripke model of constructive set theory, CZF with Subset Collection replaced by Exponentiation, in which the Cauchy reals form a set while the Dedekind reals constitute a proper class.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Ordinal notation systems corresponding to Friedman's linearized well-partial-orders with gap-condition

In this article we investigate whether the addition-free theta functions form a canonical notation system for the linear versions of Friedman's well-partial-orders with the so-called gap-condition over a finite set of labels. Rather surprisingly, we can show this is the case for two labels, but not for more than two labels. To this end, we determine the order type of the notation systems for addition-free theta functions in terms of ordinals less than $\varepsilon_0$. We further show that the maximal order type of the Friedman ordering can be obtained by a certain ordinal notation system which is based on specific binary theta functions.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Goodstein revisited

Inspired by Gentzen's 1936 consistency proof, Goodstein found a close fit between descending sequences of ordinals epsilon_0 and sequences of integers, now known as Goodstein sequences. This article revisits Goodstein's 1944 paper. In light of new historical details found in a correspondence between Bernays and Goodstein, we address the question of how close Goodstein came to proving an independence result for PA. We also present an elementary proof of the fact that already the termination of all special Goodstein sequences, i.e. those induced by the shift function, is not provable in PA. This was first proved by Kirby and Paris in 1982, using techniques from the model theory of arithmetic. The proof presented here arguably only uses tools that would have been available in the 1940's or 1950's. Thus we ponder the question whether striking independence results could have been proved much earlier? In the same vein we also wonder whether the search for strictly mathematical examples of an incompleteness in PA really attained its "holy grail" status before the late 1970's. Almost no direct moral is ever given; rather, the paper strives to lay out evidence for the reader to consider and have the reader form their own conclusions. However, in relation to independence results, we think that both Goodstein and Gentzen are deserving of more credit.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience

In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo-Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF +RDC+ LPO has indeed the same strength as CZF, where RDC stands for relativized dependent choice. In particular, these theories prove the same Pi-?0-2 theorems of arithmetic.

0 citations0 reviewsNo code linkedOpen access