-
11Carnegie Mellon University, Pittsburgh, PA May 19–23, 2004Bulletin of Symbolic Logic 11 (1). 2005.
-
13Intuitionistic sets and numbers: small set theory and Heyting arithmeticArchive for Mathematical Logic. forthcoming.It has long been known that (classical) Peano arithmetic is, in some strong sense, “equivalent” to the variant of (classical) Zermelo–Fraenkel set theory (including choice) in which the axiom of infinity is replaced by its negation. The intended model of the latter is the set of hereditarily finite sets. The connection between the theories is so tight that they may be taken as notational variants of each other. Our purpose here is to develop and establish a constructive version of this. We prese…Read more
-
17Handbook of Constructive Mathematics (edited book)Cambridge University Press. 2023.Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s my…Read more
-
8Admissible extensions of subtheories of second order arithmeticAnnals of Pure and Applied Logic 175 (7): 103425. 2024.
-
27Constructing the constructible universe constructivelyAnnals of Pure and Applied Logic 175 (3): 103392. 2024.
-
13Choice and independence of premise rules in intuitionistic set theoryAnnals of Pure and Applied Logic 174 (9): 103314. 2023.
-
5Investigations of Subsystems of Second Order Arithmetic and Set Theory in Strength between Π11 -CA and Δ12 -CA + BI: Part I (review)In Ralf Schindler (ed.), Ways of Proof Theory, De Gruyter. pp. 363-440. 2010.
-
4Formal Baire Space in Constructive Set TheoryIn Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation, De Gruyter. pp. 123-136. 2012.
-
18Ordinal notations based on a weakly Mahlo cardinalArchive for Mathematical Logic 29 (4): 249-263. 1990.
-
41997 european summer meeting of the association for symbolic logicBulletin of Symbolic Logic 4 (1): 55-117. 1998.
-
31A proof-theoretic characterization of the primitive recursive set functionsJournal 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
-
9On the proof-theoretic strength of monotone induction in explicit mathematicsAnnals of Pure and Applied Logic 85 (1): 1-46. 1997.
-
7On 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
-
12Inaccessible set axioms may have little consistency strengthAnnals 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
-
8Lifschitz realizability as a topological constructionJournal 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.
-
19Derivatives of normal functions in reverse mathematicsAnnals of Pure and Applied Logic 172 (2): 102890. 2021.
-
On Relating Theories: Proof-Theoretical ReductionIn Stefania Centrone, Sara Negri, Deniz Sarikaya & Peter M. Schuster (eds.), Mathesis Universalis, Computability and Proof, Springer Verlag. 2019.
-
24Richard Sommer. Transfinite induction within Peano arithmetic. Annals of pure and applied logic, vol. 76 , pp. 231–289Journal of Symbolic Logic 61 (4): 1388. 1996.
-
12Gentzen'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
-
29Preservation 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
-
Proof Theory of Constructive Systems: Inductive Types and UnivalenceIn Gerhard Jäger & Wilfried Sieg (eds.), Feferman on Foundations: Logic, Mathematics, Philosophy, Springer. 2017.
-
15Kripke-Platek Set Theory and the Anti-Foundation AxiomMathematical 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
-
25An 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
-
34Ordinal 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
-
4Explicit Mathematics with the Monotone Fixed Point Principle. II: ModelsJournal 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
-
12Remarks 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.
-
19Reverse mathematics and well-ordering principlesIn S. B. Cooper & Andrea Sorbi (eds.), Computability in Context: Computation and Logic in the Real World, World Scientific. 2011.
-
24Recent 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
-
14Constructive 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
-
15Proof 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
-
University of LeedsRegular Faculty
Leeds, West Yorkshire, United Kingdom of Great Britain and Northern Ireland
Areas of Interest
19th Century Philosophy |
20th Century Philosophy |