-
33Inaccessibility in constructive set theory and type theoryAnnals of Pure and Applied Logic 94 (1-3): 181-200. 1998.This paper is the first in a series whose objective is to study notions of large sets in the context of formal theories of constructivity. The two theories considered are Aczel's constructive set theory and Martin-Löf's intuitionistic theory of types. This paper treats Mahlo's π-numbers which give rise classically to the enumerations of inaccessibles of all transfinite orders. We extend the axioms of CZF and show that the resulting theory, when augmented by the tertium non-datur, is equivalent t…Read more
-
32Recent 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
-
30Ordinal notation systems corresponding to Friedman’s linearized well-partial-orders with gap-conditionArchive 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
-
28Proof theory of reflectionAnnals 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
-
28On the regular extension axiom and its variantsMathematical Logic Quarterly 49 (5): 511. 2003.The regular extension axiom, REA, was first considered by Peter Aczel in the context of Constructive Zermelo-Fraenkel Set Theory as an axiom that ensures the existence of many inductively defined sets. REA has several natural variants. In this note we gather together metamathematical results about these variants from the point of view of both classical and constructive set theory
-
28Ordinal analysis and the infinite ramsey theoremIn S. Barry Cooper (ed.), How the World Computes, . pp. 1--10. 2012.
-
27Characterizing the interpretation of set theory in Martin-Löf type theoryAnnals 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
-
27The disjunction and related properties for constructive Zermelo-Fraenkel set theoryJournal of Symbolic Logic 70 (4): 1233-1254. 2005.This paper proves that the disjunction property, the numerical existence property, Church’s rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory, CZF, and also for the theory CZF augmented by the Regular Extension Axiom.As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth.
-
27Preservation of choice principles under realizabilityLogic 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
-
23Constructing the constructible universe constructivelyAnnals of Pure and Applied Logic 175 (3): 103392. 2024.
-
23Richard Sommer. Transfinite induction within Peano arithmetic. Annals of pure and applied logic, vol. 76 , pp. 231–289Journal of Symbolic Logic 61 (4): 1388. 1996.
-
23Recent 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
-
22Constructive Zermelo–Fraenkel set theory and the limited principle of omniscienceAnnals 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
-
21Relativized ordinal analysis: The case of Power Kripke–Platek set theoryAnnals 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
-
21How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinalsMathematical Logic Quarterly 39 (1): 47-54. 1993.In ordinal analysis of impredicative theories so-called collapsing functions are of central importance. Unfortunately, the definition procedure of these functions makes essential use of uncountable cardinals whereas the notation system that they call into being corresponds to a recursive ordinal. It has long been claimed that, instead, one should manage to develop such functions directly on the basis of admissible ordinals. This paper is meant to show how this can be done. Interpreting the colla…Read more
-
21Indefiniteness in semi-intuitionistic set theories: On a conjecture of FefermanJournal of Symbolic Logic 81 (2): 742-754. 2016.The paper proves a conjecture of Solomon Feferman concerning the indefiniteness of the continuum hypothesis relative to a semi-intuitionistic set theory.
-
20An order-theoretic characterization of the Howard–Bachmann-hierarchyArchive 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
-
20Proof-theoretic investigations on Kruskal's theoremAnnals 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
-
20Well-partial-orderings and the big Veblen numberArchive for Mathematical Logic 54 (1-2): 193-230. 2015.In this article we characterize a countable ordinal known as the big Veblen number in terms of natural well-partially ordered tree-like structures. To this end, we consider generalized trees where the immediate subtrees are grouped in pairs with address-like objects. Motivated by natural ordering properties, extracted from the standard notations for the big Veblen number, we investigate different choices for embeddability relations on the generalized trees. We observe that for addresses using on…Read more
-
17Replacement versus collection and related topics in constructive Zermelo–Fraenkel set theoryAnnals 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
-
17The natural numbers in constructive set theoryMathematical Logic Quarterly 54 (1): 83-97. 2008.Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories
-
16Reverse mathematics and well-ordering principlesIn S. B. Cooper & Andrea Sorbi (eds.), Computability in Context: Computation and Logic in the Real World, World Scientific. 2011.
-
14Derivatives of normal functions in reverse mathematicsAnnals of Pure and Applied Logic 172 (2): 102890. 2021.
-
131997 european summer meeting of the association for symbolic logicBulletin of Symbolic Logic 4 (1): 55-117. 1998.
-
13Choice and independence of premise rules in intuitionistic set theoryAnnals of Pure and Applied Logic 174 (9): 103314. 2023.
-
12The Recursively Mahlo Property in Second Order ArithmeticMathematical Logic Quarterly 42 (1): 59-66. 1996.The paper characterizes the second order arithmetic theorems of a set theory that features a recursively Mahlo universe; thereby complementing prior proof-theoretic investigations on this notion. It is shown that the property of being recursively Mahlo corresponds to a certain kind of β-model reflection in second order arithmetic. Further, this leads to a characterization of the reals recursively computable in the superjump functional
-
11Gentzen's Centenary: The Quest for Consistency (edited book)Springer. 2015.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
-
10On the proof-theoretic strength of monotone induction in explicit mathematicsAnnals 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
-
10A note on the Σ1 spectrum of a theoryArchive for Mathematical Logic 41 (1): 33-34. 2002.Let T be a suitable system of classical set theory. We will show, that the Σ1 spectrum of T, i.e. the set of ordinals having good Σ1 definition in T is an initial segment of the ordinals.
-
9Remarks on Barr’s Theorem: Proofs in Geometric TheoriesIn Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter. pp. 347-374. 2016.
-
University of LeedsRegular Faculty
Leeds, West Yorkshire, United Kingdom of Great Britain and Northern Ireland
Areas of Interest
19th Century Philosophy |
20th Century Philosophy |