-
232A 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
-
206Explicit 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 (Feferman's notion of set) possesses a…Read more
-
184Explicit mathematics with the monotone fixed point principleJournal of Symbolic Logic 63 (2): 509-542. 1998.The context for this paper is Feferman's theory of explicit mathematics, a formal framework serving many purposes. It is suitable for representing Bishop-style constructive mathematics as well as generalized recursion, including direct expression of structural concepts which admit self-application. 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 (Feferman's notion …Read more
-
122Lifschitz realizability for intuitionistic Zermelo–Fraenkel set theoryArchive for Mathematical Logic 51 (7-8): 789-818. 2012.A variant of realizability for Heyting arithmetic which validates Church’s thesis with uniqueness condition, but not the general form of Church’s thesis, was introduced by Lifschitz (Proc Am Math Soc 73:101–106, 1979). A Lifschitz counterpart to Kleene’s realizability for functions (in Baire space) was developed by van Oosten (J Symb Log 55:805–821, 1990). In that paper he also extended Lifschitz’ realizability to second order arithmetic. The objective here is to extend it to full intuitionistic…Read more
-
120An ordinal analysis for theories of self-referential truthArchive for Mathematical Logic 49 (2): 213-247. 2010.The first attempt at a systematic approach to axiomatic theories of truth was undertaken by Friedman and Sheard (Ann Pure Appl Log 33:1–21, 1987). There twelve principles consisting of axioms, axiom schemata and rules of inference, each embodying a reasonable property of truth were isolated for study. Working with a base theory of truth conservative over PA, Friedman and Sheard raised the following questions. Which subsets of the Optional Axioms are consistent over the base theory? What are the …Read more
-
106Ordinal notations based on a weakly Mahlo cardinalArchive for Mathematical Logic 29 (4): 249-263. 1990.
-
92Kripke-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
-
88An ordinal analysis of parameter free Π12-comprehensionArchive for Mathematical Logic 44 (3): 263-362. 2005.Abstract.This paper is the second in a series of three culminating in an ordinal analysis of Π12-comprehension. Its objective is to present an ordinal analysis for the subsystem of second order arithmetic with Δ12-comprehension, bar induction and Π12-comprehension for formulae without set parameters. Couched in terms of Kripke-Platek set theory, KP, the latter system corresponds to KPi augmented by the assertion that there exists a stable ordinal, where KPi is KP with an additional axiom stating…Read more
-
87Proof-theoretic analysis of KPMArchive for Mathematical Logic 30 (5-6): 377-403. 1991.KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained…Read more
-
74From the weak to the strong existence propertyAnnals of Pure and Applied Logic 163 (10): 1400-1418. 2012.
-
73An ordinal analysis of stabilityArchive for Mathematical Logic 44 (1): 1-62. 2005.Abstract.This paper is the first in a series of three which culminates in an ordinal analysis of Π12-comprehension. On the set-theoretic side Π12-comprehension corresponds to Kripke-Platek set theory, KP, plus Σ1-separation. The strength of the latter theory is encapsulated in the fact that it proves the existence of ordinals π such that, for all β>π, π is β-stable, i.e. Lπ is a Σ1-elementary substructure of Lβ. The objective of this paper is to give an ordinal analysis of a scenario of not too …Read more
-
71The Friedman—Sheard programme in intuitionistic logicJournal of Symbolic Logic 77 (3): 777-806. 2012.This paper compares the roles classical and intuitionistic logic play in restricting the free use of truth principles in arithmetic. We consider fifteen of the most commonly used axiomatic principles of truth and classify every subset of them as either consistent or inconsistent over a weak purely intuitionistic theory of truth
-
71The Constructive Hilbert Program and the Limits of Martin-Löf Type TheorySynthese 147 (1): 81-120. 2005.
-
66On the constructive Dedekind realsLogic and Analysis 1 (2): 131-152. 2008.In order to build the collection of Cauchy reals as a set in constructive set theory, the only power set-like principle needed is exponentiation. In contrast, the proof that the Dedekind reals form a set has seemed to require more than that. The main purpose here is to show that exponentiation alone does not suffice for the latter, by furnishing a Kripke model of constructive set theory, Constructive Zermelo–Fraenkel set theory with subset collection replaced by exponentiation, in which the Cauc…Read more
-
64Theories and Ordinals in Proof TheorySynthese 148 (3): 719-743. 2006.How do ordinals measure the strength and computational power of formal theories? This paper is concerned with the connection between ordinal representation systems and theories established in ordinal analyses. It focusses on results which explain the nature of this connection in terms of semantical and computational notions from model theory, set theory, and generalized recursion theory
-
57The strength of Martin-Löf type theory with a superuniverse. Part IArchive for Mathematical Logic 39 (1): 1-39. 2000.Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved that Marti…Read more
-
56Slow consistencyAnnals of Pure and Applied Logic 164 (3): 382-393. 2013.The fact that “natural” theories, i.e. theories which have something like an “idea” to them, are almost always linearly ordered with regard to logical strength has been called one of the great mysteries of the foundation of mathematics. However, one easily establishes the existence of theories with incomparable logical strengths using self-reference . As a result, PA+Con is not the least theory whose strength is greater than that of PA. But still we can ask: is there a sense in which PA+Con is t…Read more
-
54Inaccessible 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
-
54Reverse mathematics and well-ordering principles: A pilot studyAnnals 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
-
53The strength of some Martin-Löf type theoriesArchive for Mathematical Logic 33 (5): 347-385. 1994.One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a construct…Read more
-
52New Orleans Marriott and Sheraton New Orleans New Orleans, Louisiana January 7–8, 2007Bulletin of Symbolic Logic 13 (3). 2007.
-
45Recent advances in ordinal analysis: Π 21-CA and related systemsBulletin of Symbolic Logic 1 (4). 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].Ordin…Read more
-
45The role of parameters in bar rule and bar inductionJournal of Symbolic Logic 56 (2): 715-730. 1991.For several subsystems of second order arithmetic T we show that the proof-theoretic strength of T + (bar rule) can be characterized in terms of T + (bar induction) □ , where the latter scheme arises from the scheme of bar induction by restricting it to well-orderings with no parameters. In addition, we demonstrate that ACA + 0 , ACA 0 + (bar rule) and ACA 0 + (bar induction) □ prove the same Π 1 1 -sentences
-
43Realizing Mahlo set theory in type theoryArchive for Mathematical Logic 42 (1): 89-101. 2003.After introducing the large set notion of Mahloness, this paper shows that constructive set theory with an axiom asserting the existence of a Mahlo set has a realizability interpretation in an extension of Martin-Löf type theory developed by A. Setzer
-
42A note on Bar Induction in Constructive Set TheoryMathematical Logic Quarterly 52 (3): 253-258. 2006.Bar Induction occupies a central place in Brouwerian mathematics. This note is concerned with the strength of Bar Induction on the basis of Constructive Zermelo-Fraenkel Set Theory, CZF. It is shown that CZF augmented by decidable Bar Induction proves the 1-consistency of CZF. This answers a question of P. Aczel who used Bar Induction to give a proof of the Lusin Separation Theorem in the constructive set theory CZF
-
40Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM (review)Archive for Mathematical Logic 33 (1): 35-55. 1994.It is shown how the strong ordinal notation systems that figure in proof theory and have been previously defined by employing large cardinals, can be developed directly on the basis of their recursively large counterparts. Thereby we provide a completely new approach to well-ordering proofs as will be exemplified by determining the proof-theoretic ordinal of the systemKPM of [R91]
-
39Recent Advances in Ordinal Analysis: Π 1 2 — CA and Related SystemsBulletin 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
-
36A note on the theory of positive induction, $${{\rm ID}^*_1}$$Archive for Mathematical Logic 49 (2): 275-281. 2010.The article shows a simple way of calibrating the strength of the theory of positive induction, ${{\rm ID}^{*}_{1}}$ . Crucially the proof exploits the equivalence of ${\Sigma^{1}_{1}}$ dependent choice and ω-model reflection for ${\Pi^{1}_{2}}$ formulae over ACA 0. Unbeknown to the authors, D. Probst had already determined the proof-theoretic strength of ${{\rm ID}^{*}_{1}}$ in Probst, J Symb Log, 71, 721–746, 2006
-
36The strength of Martin-Löf type theory with a superuniverse. Part IIArchive for Mathematical Logic 40 (3): 207-233. 2001.Universes of types were introduced into constructive type theory by Martin-Löf [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?.This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]).It is proved that Martin-Löf type theory with a superunive…Read more
-
35Monotone inductive definitions in explicit mathematicsJournal of Symbolic Logic 61 (1): 125-146. 1996.The context for this paper is Feferman's theory of explicit mathematics, T 0 . We address a problem that was posed in [6]. Let MID be the principle stating that any monotone operation on classifications has a least fixed point. The main objective of this paper is to show that T 0 + MID, when based on classical logic, also proves the existence of non-monotone inductive definitions that arise from arbitrary extensional operations on classifications. From the latter we deduce that MID, when adjoine…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 |