•  19
    Constructing the constructible universe constructively
    Annals of Pure and Applied Logic 175 (3): 103392. 2024.
  •  10
    Choice and independence of premise rules in intuitionistic set theory
    with Emanuele Frittaion and Takako Nemoto
    Annals of Pure and Applied Logic 174 (9): 103314. 2023.
  •  1
    Formal Baire Space in Constructive Set Theory
    with Giovanni Curi
    In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation, De Gruyter. pp. 123-136. 2012.
  •  100
    Ordinal notations based on a weakly Mahlo cardinal
    Archive for Mathematical Logic 29 (4): 249-263. 1990.
  •  10
    1997 european summer meeting of the association for symbolic logic
    with R. Shore, J. Steel, and A. Wilkie
    Bulletin of Symbolic Logic 4 (1): 55-117. 1998.
  •  213
    A proof-theoretic characterization of the primitive recursive set functions
    Journal of Symbolic Logic 57 (3): 954-969. 1992.
    Let KP- be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V:= universe of sets) be a ▵0-definable set function, i.e. there is a ▵0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and $V \models \forall x \exists!y\varphi (x, y)$ . In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection of those functions which are Σ1…Read more
  •  7
    On the proof-theoretic strength of monotone induction in explicit mathematics
    with Thomas Glaß and Andreas Schlüter
    Annals of Pure and Applied Logic 85 (1): 1-46. 1997.
    We characterize the proof-theoretic strength of systems of explicit mathematics with a general principle asserting the existence of least fixed points for monotone inductive definitions, in terms of certain systems of analysis and set theory. In the case of analysis, these are systems which contain the Σ12-axiom of choice and Π12-comprehension for formulas without set parameters. In the case of set theory, these are systems containing the Kripke-Platek axioms for a recursively inaccessible unive…Read more
  •  44
    Inaccessible set axioms may have little consistency strength
    Annals of Pure and Applied Logic 115 (1-3): 33-70. 2002.
    The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In ZFC inaccessible sets are of the form Vκ where κ is a strongly inaccessible cardinal and Vκ denotes the κth level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the co…Read more
  •  4
    Lifschitz realizability as a topological construction
    with Andrew W. Swan
    Journal of Symbolic Logic 85 (4): 1342-1375. 2020.
    We develop a number of variants of Lifschitz realizability for $\mathbf {CZF}$ by building topological models internally in certain realizability models. We use this to show some interesting metamathematical results about constructive set theory with variants of the lesser limited principle of omniscience including consistency with unique Church’s thesis, consistency with some Brouwerian principles and variants of the numerical existence property.
  •  11
    Derivatives of normal functions in reverse mathematics
    with Anton Freund
    Annals of Pure and Applied Logic 172 (2): 102890. 2021.
  • On Relating Theories: Proof-Theoretical Reduction
    with Michael Toppel
    In Stefania Centrone, Sara Negri, Deniz Sarikaya & Peter M. Schuster (eds.), Mathesis Universalis, Computability and Proof, Springer Verlag. 2019.
  •  8
    Gerhard Gentzen has been described as logic’s lost genius, whom Gödel called a better logician than himself. This work comprises articles by leading proof theorists, attesting to Gentzen’s enduring legacy to mathematical logic and beyond. The contributions range from philosophical reflections and re-evaluations of Gentzen’s original consistency proofs to the most recent developments in proof theory. Gentzen founded modern proof theory. His sequent calculus and natural deduction system beautifull…Read more
  •  19
    Preservation of choice principles under realizability
    with Eman Dihoum
    Logic Journal of the IGPL 27 (5): 746-765. 2019.
    Especially nice models of intuitionistic set theories are realizability models $V$, where $\mathcal A$ is an applicative structure or partial combinatory algebra. This paper is concerned with the preservation of various choice principles in $V$ if assumed in the underlying universe $V$, adopting Constructive Zermelo–Fraenkel as background theory for all of these investigations. Examples of choice principles are the axiom schemes of countable choice, dependent choice, relativized dependent choice…Read more
  •  87
    Kripke-Platek Set Theory and the Anti-Foundation Axiom
    Mathematical Logic Quarterly 47 (4): 435-440. 2001.
    The paper investigates the strength of the Anti-Foundation Axiom, AFA, on the basis of Kripke-Platek set theory without Foundation. It is shown that the addition of AFA considerably increases the proof theoretic strength
  •  15
    An order-theoretic characterization of the Howard–Bachmann-hierarchy
    with Jeroen Van der Meeren and Andreas Weiermann
    Archive for Mathematical Logic 56 (1-2): 79-118. 2017.
    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 Π11\documentclass[12pt]{minimal} \usep…Read more
  •  19
    Ordinal notation systems corresponding to Friedman’s linearized well-partial-orders with gap-condition
    with Jeroen Van der Meeren and Andreas Weiermann
    Archive for Mathematical Logic 56 (5-6): 607-638. 2017.
    In this article we investigate whether the following conjecture is true or not: does 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 n 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 t…Read more
  •  4
    Explicit Mathematics with the Monotone Fixed Point Principle. II: Models
    Journal of Symbolic Logic 64 (2): 517-550. 1999.
    This paper continues investigations of the monotone fixed point principle in the context of Feferman's explicit mathematics begun in [14]. Explicit mathematics is a versatile formal framework for representing Bishop-style constructive mathematics and generalized recursion theory. The object of investigation here is the theory of explicit mathematics augmented by the monotone fixed point principle, which asserts that any monotone operation on classifications possesses a least fixed point. To be m…Read more
  •  10
    Reverse mathematics and well-ordering principles
    with Andreas Weiermann
    In S. B. Cooper & Andrea Sorbi (eds.), Computability in Context: Computation and Logic in the Real World, World Scientific. 2011.
  •  18
    Recent Advances in Ordinal Analysis: Π 1 2 — CA and Related Systems (review)
    Bulletin of Symbolic Logic 1 (4): 468-485. 1995.
    §1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of-analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to-formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated-comprehension, e.g.,-comprehension. The details will be laid out in [28].Ordinal-t…Read more
  •  17
    Constructive Zermelo–Fraenkel set theory and the limited principle of omniscience
    Annals of Pure and Applied Logic 165 (2): 563-572. 2014.
    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 st…Read more
  •  18
    Proof theory of reflection
    Annals of Pure and Applied Logic 68 (2): 181-224. 1994.
    The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. R…Read more
  •  18
    Relativized ordinal analysis: The case of Power Kripke–Platek set theory
    Annals of Pure and Applied Logic 165 (1): 316-339. 2014.
    The paper relativizes the method of ordinal analysis developed for Kripke–Platek set theory to theories which have the power set axiom. We show that it is possible to use this technique to extract information about Power Kripke–Platek set theory, KP.As an application it is shown that whenever KP+AC proves a ΠP2 statement then it holds true in the segment Vτ of the von Neumann hierarchy, where τ stands for the Bachmann–Howard ordinal
  •  12
    Replacement versus collection and related topics in constructive Zermelo–Fraenkel set theory
    Annals of Pure and Applied Logic 136 (1-2): 156-174. 2005.
    While it is known that intuitionistic ZF set theory formulated with Replacement, IZFR, does not prove Collection, it is a longstanding open problem whether IZFR and intuitionistic set theory ZF formulated with Collection, IZF, have the same proof-theoretic strength. It has been conjectured that IZF proves the consistency of IZFR. This paper addresses similar questions but in respect of constructive Zermelo–Fraenkel set theory, CZF. It is shown that in the latter context the proof-theoretic stren…Read more
  •  13
    Proof-theoretic investigations on Kruskal's theorem
    with Andreas Weiermann
    Annals of Pure and Applied Logic 60 (1): 49-88. 1993.
    In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction
  •  26
    Characterizing the interpretation of set theory in Martin-Löf type theory
    with Sergei Tupailo
    Annals of Pure and Applied Logic 141 (3): 442-471. 2006.
    Constructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized b…Read more
  •  42
    Reverse mathematics and well-ordering principles: A pilot study
    with Bahareh Afshari
    Annals of Pure and Applied Logic 160 (3): 231-237. 2009.
    The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, we prove in …Read more