# School of Mathematics

## Prof Michael Rathjen

Professor of Pure Mathematics

Pure Mathematics

### Contact details

Room: Satellite 10.29

Tel: +44 (0)113 3435109

Email: M.Rathjen @ leeds.ac.uk

## Research interests

1) PROOF THEORY: Cut elimination for infinitary proof systems; ordinal analysis of classical and intuitionistic theories; witness extraction from proofs. In Proof Theory, from the work of Gentzen in the 1930's up to the present time, a central theme is the assignment of `proof theoretic ordinals' to theories, measuring their `consistency strength' and `computational power', and providing a scale against which those theories may be compared and classified.

2) INTUITIONISM and CONSTRUCTIVE MATHEMATICS: frameworks for constructivism (constructive set theory, explicit mathematics, Martin-Löf type theory); realizability and forcing techniques

3) SET THEORY (mostly non-classical): proof theory and ordinal analysis of set theories; admissible set theory; constructive and intuitionistic set theory; set theory with anti-foundation axiom; "large cardinals" axioms in constructive and intuitionistic set theories.

4) REVERSE MATHEMATICS and COMBINATORIAL PRINCIPLES: Kruskal's Theorem, Graph Minor Theorem, ...

5) PHILOSOPHY of MATHEMATICS

### Useful links

## Current postgraduate students

Anton Freund (2014)

Cesare Gallozzi (2014)

Martin Krombholz (2014)

Alec Thomson (2012)

Jakob Vidmar (2014)

## Publications

**Rathjen M, Van der Meeren J, Weiermann A** Ordinal notation systems corresponding to Friedman’s linearized well-partial-orders with gap-condition *Archive for Mathematical Logic*, **56**, 607-638, 2017

DOI:10.1007/s00153-017-0559-2

View abstract

**Van der Meeren J, Rathjen M, Weiermann A** An order-theoretic characterization of the Howard–Bachmann-hierarchy *Archive for Mathematical Logic*, **56**, 79-118, 2017

DOI:10.1007/s00153-016-0515-6

View abstract

**Cook J, Rathjen M** Classifying the provably total set functions of KP and KP(P) *IfCoLog Journal of Logics and their Applications*, **3**, 681-753, 2016

View abstract

**Rathjen M** Indefiniteness in semi-intuitionistic set theories: On a conjecture of feferman *Journal of Symbolic Logic*, **81**, 742-754, 2016

DOI:10.1017/jsl.2015.55

View abstract

**Cook J, Rathjen M** Ordinal Analysis of Intuionistic power and exponentiation Kripke Platek set theory In *Advances in Proof Theory*, **28**, 79-172, 2016

DOI:10.1007/978-3-319-29198-7_4

View abstract

**Rathjen M ** Remarks on Barr's Theorem: Proofs in Geometric Theories. 6, 347-374 2016

**Cook J; Rathjen M ** *Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory*ADVANCES IN PROOF THEORY, 79-172 2016

DOI:10.1007/978-3-319-29198-7_4

**Rathjen M** Goodstein's theorem revisited In *Gentzen's Centenary: The Quest for Consistency*, 229-242, 2015

DOI:10.1007/978-3-319-10103-3_9

View abstract

**Van der Meeren J, Rathjen M, Weiermann A** Well-partial-orderings and the big Veblen number *Archive for Mathematical Logic*, **54**, 193-230, 2015

DOI:10.1007/s00153-014-0408-5

View abstract

**Kahle R; Rathjen M ** Gentzen’s centenary: The quest for consistency. 1-561 2015

DOI:10.1007/978-3-319-10103-3

View abstract

**Van Der Meeren J, Rathjen M, Weiermann A** Well-partial-orderings and the big Veblen number *Archive for Mathematical Logic*, 2014

DOI:10.1007/s00153-014-0408-5

View abstract

**Rathjen M** Omega-models and well-ordering proofs In *Foundational Adventures*, 179-212, 2014

**Rathjen M** Relativized ordinal analysis: The case of Power Kripke-Platek set theory *Annals of Pure and Applied Logic*, **165**, 316-339, 2014

DOI:10.1016/j.apal.2013.07.016

View abstract

**Rathjen M** Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience *Annals of Pure and Applied Logic*, **165**, 563-572, 2013

DOI:10.1016/j.apal.2013.08.001

View abstract

**Lubarsky RS, Rathjen M** Realizability models separating various Fan theorems *Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, **7921 LNCS**, 306-315, 2013

DOI:10.1007/978-3-642-39053-1_35

View abstract

**Friedman S-D, Rathjen M, Weiermann A** Slow consistency *Annals of Pure and Applied Logic*, **164**, 382-393, 2013

DOI:10.1016/j.apal.2012.11.009

View abstract

**Rathjen M** Michael Rathjen looks at - TURING'S 'ORACLE' IN PROOF THEORY *ALAN TURING: HIS WORK AND IMPACT*, 198-202, 2013

**Rathjen M** From the weak to the strong existence property *Annals of Pure and Applied Logic*, **163**, 1400-1418, 2012

DOI:10.1016/j.apal.2012.01.012

View abstract

**Chen R-M, Rathjen M** Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory *Archive for Mathematical Logic*, **51**, 789-818, 2012

DOI:10.1007/s00153-012-0299-2

View abstract

**Rathjen M, Leigh GE** The Friedman-Sheard programme in intuitionistic
logic *The Journal of Symbolic Logic*, **77**, 777-806, 2012

DOI:10.2178/jsl/1344862162

View abstract

**Afshari B, Rathjen M** Ordinal analysis and the infinite Ramsey theorem *Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, **7318 LNCS**, 1-10, 2012

DOI:10.1007/978-3-642-30870-3_1

View abstract

**Rathjen M** Constructive zermelo-fraenkel set theory, power set, and the calculus of constructions In *Epistemology versus ontology: Essays on the philosophy and foundations of mathematics in honour of Per Martin-Löf*, **27**, 313-349, 2012

DOI:10.1007/978-94-007-4435-6

View abstract

**Rathjen M, Chen RM** Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory *Archive for Mathematical Logic*, 2012

DOI:10.1007/s00153-012-0299-2

**Curi G, Rathjen M** Baire space in CZF In *Logic, construction, computation*, 123-135, 2012

**Rathjen M, Weiermann A** Reverse mathematics and well-ordering principles In *Computability in Context*, 351-370, 2011

View abstract

**Leigh GE, Rathjen M** An ordinal analysis for theories of self-referential truth *ARCH MATH LOGIC*, **49**, 213-247, 2010

DOI:10.1007/s00153-009-0170-2

**Afshari B, Rathjen M** A note on the theory of positive induction, ID1* *ARCH MATH LOGIC*, **49**, 275-281, 2010

DOI:10.1007/s00153-009-0168-9

**Rathjen M** Metamathematical properties of intuitionistic set theories with choice principles In *New Computational Paradigms:
Changing Conceptions of What is Computable*, 287-312, 2010

DOI:10.1007/978-0-387-68546-5_13

View abstract

**Rathjen M** Investigations of subsystems of second order arithmetic and set theory in strength between Pi-1-1-CA and delta-1-2-CA+BI: part I In *Ways of proof theory*, 363-440, 2010

View abstract

**Afshari B, Rathjen M** Reverse mathematics and well-ordering principles: A pilot study *ANNALS OF PURE AND APPLIED LOGIC*, **160**, 231-237, 2009

DOI:10.1016/j.apal.2009.01.001

**Rathjen M** The constructive Hilbert program and the limits of Martin-Löf type theory In *Logicism, intuitionism, and formalism*, **341**, 397-433, 2008

View abstract

**Rathjen M, Lubarsky RS** On the constructive Dedekind reals *Logic and Analysis*, **1**, 131-152, 2008

DOI:10.1007/s11813-007-0005-6

View abstract

**Rathjen M** The natural numbers in constructive set theory *MATHEMATICAL LOGIC QUARTERLY*, **54**, 83-97, 2008

DOI:10.1002/malq.200710036

**Rathjen M ** *Theories and ordinals: ordinal analysis*Computation and Logic in the Real World, Proceedings, 632-637 2007

**Lubarsky RS; Rathjen M ** *On the constructive Dedekind reals: Extended abstract*LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 349-+ 2007

DOI:10.1007/978-3-540-72734-7_25

**Rathjen M** The art of ordinal analysis *International Congress of Mathematicians, ICM 2006*, **2**, 45-69, 2006

View abstract

**Rathjen M** Theories and ordinals in proof theory *SYNTHESE*, **148**, 719-743, 2006

DOI:10.1007/s11229-004-6297-0

**Rathjen M** A note on bar induction in constructive set theory *MATH LOGIC QUART*, **52**, 253-258, 2006

DOI:10.1002/malq.200510030

**Rathjen M ** *Models of intuitionistic set theories over partial combinatory algebras*LECT NOTES COMPUT SC, 68-78 2006

View abstract

**Rathjen M ** *Choice principles in constructive and classical set theories*Logic Colloquium '02, 299-326 2006

**Rathjen M** The constructive Hilbert program and the limits of Martin-Lof type theory *SYNTHESE*, **147**, 81-120, 2005

DOI:10.1007/s11229-004-6208-4

**Rathjen M** Constructive set theory and Brouwerian principles *Journal of Universal Computer Science*, **11**, 2008-2033, 2005

DOI:10.3217/jucs-011-12-2008

View abstract

**Rathjen M** The anti-foundation axiom in constructive set theories In *Games, Logic and Constructive Sets*, 87-108, 2003

**Rathjen M, Lubarsky YE** On the regular extension axiom and its variants *Mathematical Logic Quarterly*, **49**, 511-518, 2003

View abstract

**Rathjen M** Realizing Mahlo set theory in type theory *ARCH MATH LOGIC*, **42**, 89-101, 2003

DOI:10.1007/s00153-002-0159-6

**Crosilla L, Rathjen M** Inaccessible set axioms may have little consistency strength *Annals of Pure and Applied Logic*, **115**, 33-70, 2002

DOI:10.1016/S0168-0072(01)00083-5

View abstract

**Rathjen M** Explicit mathematics with monotone inductive definitions: A Survey In *Reflections on The Foundation of Mathematics: Essays in honor of Soloman Feferman*, 335-352, 2002

**Rathjen M, Ollerfeld MM** A note on the Sigma (1) spectrum of a theory *Archive for Mathematical Logic*, **41**, 33-34, 2002

DOI:10.1007/s001530200001

**Mollerfeld M, Rathjen M** A note on the Sigma(1) spectrum of a theory *ARCH MATH LOGIC*, **41**, 33-34, 2002

DOI:10.1007/s001530100103

**Rathjen M ** *Explicit mathematics with monotone inductive definitions: A survey*REFLECTIONS ON THE FOUNDATIONS OF MATHEMATICS, 329-346 2002

**Rathjen M** Kripke-Platek set theory and the Anti-Foundation Axiom *MATH LOGIC QUART*, **47**, 435-440, 2001

**Rathjen M** The strength of Martin-L\"of type theory with a superuniverse Part II *Archive for Mathematical Logic*, **40**, 207-233, 2001

DOI:10.1007/s001530000051

**Rathjen M** The strength of Martin-lof type theory with a superuniverse part II *Archive for Mathematical Logic*, 2001

**Rathjen M** Explicit mathematics with the monotone fixed point principle *Journal of Symbolic Logic*, **63**, 509-542, 1998

**Lubarsky RS, Rathjen M** On the constructive dedekind reals: Extended abstract *Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, **4514 LNCS**, 349-362,

DOI:10.1007/s11813-007-0005-6

**Rathjen M** Proof Theory of Constructive Systems: Inductive Types and Univalence In *Feferman on Foundations: Logic, Mathematics, Philosophy*

View abstract

© Copyright Leeds 2011