| Publication | Date of Publication | Type |
|---|
Wellfoundedness proof with the maximal distinguished set Archive for Mathematical Logic | 2023-04-27 | Paper |
| Well-foundedness proof for $\Pi^{1}_{1}$-reflection | 2023-04-07 | Paper |
| Lectures on Ordinal Analysis | 2023-04-01 | Paper |
| Provably well-founded strict partial orders | 2023-03-24 | Paper |
Wellfoundedness proof with the maximal distinguished set (available as arXiv preprint) | 2022-11-15 | Paper |
| An ordinal analysis of $\Pi_{1}$-Collection | 2021-12-18 | Paper |
Cut-Elimination for SBL The Legacy of Kurt Schütte | 2021-12-03 | Paper |
GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN–PÉTER FUNCTION The Bulletin of Symbolic Logic | 2021-09-17 | Paper |
A simplified ordinal analysis of first-order reflection Journal of Symbolic Logic | 2021-03-19 | Paper |
Ordinal Analysis with an Introduction to Proof Theory Logic in Asia: Studia Logica Library | 2020-09-04 | Paper |
| A constructive proof of a theorem by Ferreira-Zantema | 2020-08-17 | Paper |
| Refinement of proof-theoretic analysis of the lpo due to Buchholz | 2020-08-17 | Paper |
Predicatively unprovable termination of the Ackermannian Goodstein process Proceedings of the American Mathematical Society | 2020-06-11 | Paper |
Proof-theoretic strengths of the well-ordering principles Archive for Mathematical Logic | 2020-04-01 | Paper |
| Two remarks on proof theory of first-order arithmetic | 2020-03-29 | Paper |
| Mahlo classes for first-order reflections | 2019-10-15 | Paper |
Iterating the recursively Mahlo operations (available as arXiv preprint) | 2019-04-23 | Paper |
| Grzegorczyk sequence | 2018-11-25 | Paper |
Proof-theoretic strengths of weak theories for positive inductive definitions Journal of Symbolic Logic | 2018-10-26 | Paper |
Cut-elimination for \(\omega_{1}\) Annals of Pure and Applied Logic | 2018-10-18 | Paper |
Derivatives of normal functions and \(\omega \)-models Archive for Mathematical Logic | 2018-08-16 | Paper |
| Hydra games for recursively Mahlo operations | 2018-08-14 | Paper |
Cut-elimination for $\omega_{1}$ (available as arXiv preprint) | 2018-01-27 | Paper |
Proof Theory for Theories of Ordinals III: $$\Pi _{N}$$ -Reflection Gentzen's Centenary | 2017-09-27 | Paper |
| Cut-eliminability in second order logic calculi | 2017-01-04 | Paper |
Cut-elimination for SBL (available as arXiv preprint) | 2016-06-13 | Paper |
A new function algebra of EXPTIME functions by safe nested recursion ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Intuitionistic fixed point theories over set theories Archive for Mathematical Logic | 2015-09-01 | Paper |
| $omega_{1}$ under $Pi_{1}$-Collection | 2015-08-06 | Paper |
| Hydras for $\omega_{1}$ | 2015-08-06 | Paper |
| Well-foundedness proof for first-order reflection | 2015-06-17 | Paper |
Predicatively computable functions on sets Archive for Mathematical Logic | 2015-04-14 | Paper |
| Axiomatizing some small classes of set functions | 2015-03-27 | Paper |
CONSERVATIONS OF FIRST-ORDER REFLECTIONS Journal of Symbolic Logic | 2014-12-05 | Paper |
Lifting proof theory to the countable ordinals: Zermelo-Fraenkel set theory The Journal of Symbolic Logic | 2014-09-30 | Paper |
| Lifting proof theory to the countable ordinals II: second-order indescribable cardinals | 2014-09-04 | Paper |
| A polynomial time complete disjunction property in intuitionistic propositional logic | 2013-12-11 | Paper |
| Proof search in multi-succedent sequent calculi for intuitionistic logic under the Schuette's schema | 2013-12-04 | Paper |
A sneak preview of proof theory of ordinals Annals of the Japan Association for Philosophy of Science | 2013-11-18 | Paper |
Proof theory of weak compactness Journal of Mathematical Logic | 2013-10-17 | Paper |
Provably \(\Delta ^0_2\) and weakly descending chains Proceedings of the 11th Asian Logic Conference | 2013-06-03 | Paper |
Quick cut-elimination for strictly positive cuts Annals of Pure and Applied Logic | 2011-09-22 | Paper |
Wellfoundedness proofs by means of non-monotonic inductive definitions. II: First order operators Annals of Pure and Applied Logic | 2011-09-12 | Paper |
Intuitionistic fixed point theories over Heyting arithmetic (available as arXiv preprint) | 2011-05-31 | Paper |
Nested PLS Archive for Mathematical Logic | 2011-05-11 | Paper |
Exact bounds on epsilon processes Archive for Mathematical Logic | 2011-05-11 | Paper |
| scientific article; zbMATH DE number 5788436 (Why is no real title available?) | 2010-09-20 | Paper |
Polynomal-size Frege proofs of Bollobás' theorem on the trace of sets Proceedings of the Japan Academy. Series A | 2009-01-13 | Paper |
Non-elementary speed-ups in logic calculi Mathematical Logic Quarterly | 2008-12-10 | Paper |
Epsilon substitution method for -FIX Journal of Symbolic Logic | 2007-01-19 | Paper |
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science Lecture Notes in Computer Science | 2006-11-14 | Paper |
Epsilon substitution method for \([\Pi^0_1,\Pi^0_1]\)-FIX Archive for Mathematical Logic | 2005-12-14 | Paper |
Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX Annals of Pure and Applied Logic | 2005-09-22 | Paper |
Wellfoundedness proofs by means of non-monotonic inductive definitions I: Π<sub>2</sub><sup>0</sup>-operators Journal of Symbolic Logic | 2005-08-29 | Paper |
Proof theory for theories of ordinals. II: \(\Pi_{3}\)-reflection Annals of Pure and Applied Logic | 2004-11-22 | Paper |
Epsilon substitution method for theories of jump hierarchies Archive for Mathematical Logic | 2003-09-16 | Paper |
Proof theory for theories of ordinals. I: Recursively Mahlo ordinals Annals of Pure and Applied Logic | 2003-08-13 | Paper |
Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\) Annals of Pure and Applied Logic | 2003-07-30 | Paper |
On the slowly well orderedness of \(\varepsilon_0\) Mathematical Logic Quarterly (MLQ) | 2002-05-05 | Paper |
Ordinal diagrams for Π<sub>3</sub>-reflection Journal of Symbolic Logic | 2002-02-17 | Paper |
Ordinal diagrams for recursively Mahlo universes Archive for Mathematical Logic | 2002-01-09 | Paper |
A bounded arithmetic AID for Frege systems Annals of Pure and Applied Logic | 2001-05-02 | Paper |
Extended normal form theorems for logical proofs from axioms Theoretical Computer Science | 2000-08-23 | Paper |
Some results on cut-elimination, provable well-orderings, induction and reflection Annals of Pure and Applied Logic | 2000-05-17 | Paper |
| scientific article; zbMATH DE number 1390268 (Why is no real title available?) | 2000-01-17 | Paper |
Introducing the hardline in proof theory (available as arXiv preprint) | 1999-11-08 | Paper |
| scientific article; zbMATH DE number 1305938 (Why is no real title available?) | 1999-11-08 | Paper |
| scientific article; zbMATH DE number 1305939 (Why is no real title available?) | 1999-08-22 | Paper |
Variations on a theme by Weiermann Journal of Symbolic Logic | 1999-08-19 | Paper |
Consistency proof via pointwise induction Archive for Mathematical Logic | 1998-08-10 | Paper |
A slow growing analogue to Buchholz' proof Annals of Pure and Applied Logic | 1992-06-28 | Paper |
Derivability conditions on Rosser's provability predicates Notre Dame Journal of Formal Logic | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4128806 (Why is no real title available?) | 1988-01-01 | Paper |
A consistency proof of a system including Feferman's \(ID_{\xi}\) by Takeuti's reduction method Tsukuba Journal of Mathematics | 1987-01-01 | Paper |
A subsystem of classical analysis proper to Takeuti's reduction method for \(\Pi ^ 1_ 1\)-analysis Tsukuba Journal of Mathematics | 1985-01-01 | Paper |
An accessibility proof of ordinal diagrams in intuitionistic theories for iterated inductive definitions Tsukuba Journal of Mathematics | 1984-01-01 | Paper |
An ordinal analysis of a single stable ordinal (available as arXiv preprint) | N/A | Paper |
An ordinal analysis of $\Pi_{N}$-Collection (available as arXiv preprint) | N/A | Paper |