School of Mathematics

Search site

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

Personal web page

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 TheoryADVANCES 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 analysisComputation and Logic in the Real World, Proceedings, 632-637 2007

Lubarsky RS; Rathjen M On the constructive Dedekind reals: Extended abstractLOGICAL 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 algebrasLECT NOTES COMPUT SC, 68-78 2006
View abstract

Rathjen M Choice principles in constructive and classical set theoriesLogic 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 surveyREFLECTIONS 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