15 citations · 26 across the 27 of their papers we have counts for
29 papers
Feferman's completeness theorem
Fedor Pakhomov, Michael Rathjen, Dino Rossegger
Feferman proved in 1962 that any arithmetical theorem is a consequence of a suitable transfinite iteration of full uniform reflection of . This result is commonly know…
Kreisel-Lévy-type theorems for Kripke-Platek and other set theories
Shuangshuang Shu, Michael Rathjen
We prove that, over Kripke-Platek set theory with infinity (KP), transfinite induction along the ordinal is equivalent to the schema asserting the soundness of KP, where…
Constructing the Constructible Universe Constructively
Richard Matthews, Michael Rathjen
We study the properties of the constructible universe, L, over intuitionistic theories. We give an extended set of fundamental operations which is sufficient to generate the univer…
Admissible extensions of subtheories of second order arithmetic
Gerhard Jäger, Michael Rathjen
In this paper we study admissible extensions of several theories T of reverse mathematics. The idea is that in such an extension the structure M = (N,S,\in) of the natural numbers…
Well ordering principles for iterated -comprehension
Anton Freund, Michael Rathjen
We introduce ordinal collapsing principles that are inspired by proof theory but have a set theoretic flavor. These principles are shown to be equivalent to iterated -compre…
No speedup for geometric theories
Michael Rathjen
Geometric theories based on classical logic are conservative over their intuitionistic counterparts for geometric implications. The latter result (sometimes referred to as Barr's t…
Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
Maria Emilia Maietti, Samuele Maschio, Michael Rathjen
In this work we consider an extension MFcind of the Minimalist Foundation MF for predicative constructive mathematics with the addition of inductive and coinductive definitions suf…
Extensional realizability for intuitionistic set theory
Emanuele Frittaion, Michael Rathjen
In generic realizability for set theories, realizers treat unbounded quantifiers generically. To this form of realizability, we add another layer of extensionality by requiring tha…
Ackermann and Goodstein go functorial
Juan P. Aguilera, Anton Freund, Michael Rathjen +1
We present variants of Goodstein's theorem that are equivalent to arithmetical comprehension and to arithmetical transfinite recursion, respectively, over a weak base theory. These…
Well-Ordering Principles in Proof Theory and Reverse Mathematics
Michael Rathjen
Several theorems about the equivalence of familiar theories of reverse mathematics with certain well-ordering principles have been proved by recursion-theoretic and combinatorial m…
Minimal bad sequences are necessary for a uniform Kruskal theorem
Anton Freund, Michael Rathjen, Andreas Weiermann
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…
The independence of premise rule in intuitionistic set theories
Takako Nemoto, Michael Rathjen
Independence of premise principles play an important role in characterizing the modified realizability and the Dialectica interpretations. In this paper we show that a great many i…
Upper bounds on the graph minor theorem
Martin Krombholz, Michael Rathjen
Lower bounds on the proof-theoretic strength of the graph minor theorem were found over 30 years ago by Friedman, Robertson and Seymour 1987, but upper bounds have always been elus…
A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice
Maria Emilia Maietti, Samuele Maschio, Michael Rathjen
We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mtt, extended with inductively generated formal topologies, Church's t…
Derivatives of normal functions in reverse mathematics
Anton Freund, Michael Rathjen
Consider a normal function on the ordinals (i. e. a function that is strictly increasing and continuous at limit stages). By enumerating the fixed points of we obtain a…
Lifschitz Realizability as a Topological Construction
Michael Rathjen, Andrew Swan
We develop a number of variants of Lifschitz realizability for CZF by building topological models internally in certain realizability models. We use this to show some interesting m…
Power Kripke-Platek set theory and the axiom of choice
Michael Rathjen
Whilst Power Kripke-Platek set theory, KPP, shares many properties with ordinary Kripke-Platek set theory, KP, in several ways it behaves quite differently from KP. This is perhaps…
Classifying the provably total set functions of KP and KP(P)
Jacob Cook, Michael Rathjen
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 (…
Proof Theory of Constructive Systems: Inductive Types and Univalence
Michael Rathjen
In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Ma…
Remarks on Barr's theorem: Proofs in geometric theories
Michael Rathjen
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…
Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
Jacob Cook, Michael Rathjen
Until the 1970s, proof theoretic investigations were mainly concerned with theories of inductive definitions, subsystems of analysis and finite type systems. With the pioneering wo…
Realizability Models Separating Various Fan Theorems
Robert S. Lubarsky, Michael Rathjen
We develop a realizability model in which the realizers are the reals not just Turing computable in a fixed real but rather the reals in a countable ideal of Turing degrees. This i…
On the Constructive Dedekind Reals
Robert Lubarsky, Michael Rathjen
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 De…
Ordinal notation systems corresponding to Friedman's linearized well-partial-orders with gap-condition
Michael Rathjen, Jeroen Van der Meeren, Andreas Weiermann
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-call…