Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
type: Item
instance of: scholarly article
title: Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
zbMATH Open document ID: 1022.03045
DOI: 10.1016/S0168-0072(02)00065-9
author: Sergei Tupailo
published in: Annals of Pure and Applied Logic
publication date: 2003-03-16T00:00:00Z
review text: The paper contributes to the investigation of proof-theoretic problems, which involve the comparison of three different formal frameworks relevant to the foundations of constructive mathematics: Martin-Löf's type theories, Feferman's explicit mathematics, constructive set theories (Myhill, Friedman, Aczel). In particular, the paper establishes lower bounds on the strength of Feferman's system T\(_0\) for explicit mathematics, expanded with axioms M and M\(^+\) (respectively) implying (suitable forms of) Mahlo principles. It has to be noticed that in this area of proof theory lower bound results are often established by means of well-ordering proofs. Yet the author follows a different route: he is able to embed Aczel's constructive set theories extended with corresponding set-theoretic Mahlo principles -- to be named CZFM and CZFM\(^+\) -- into \(T_0+\text{M}\) and and \(T_0+\text{M}^+\) (respectively). As usual, Aczel's CZF includes (in the language of set theory) extensionality, foundation, union, pair, bounded separation, a strong form of collection, subset collection, infinity. Concerning the axioms of \(T_0\), they include axioms for partial extended combinatory logic, natural numbers, elementary comprehension, join (i.e. uniform disjoint sum) and inductive generation (there is an operation \(i\) picking out uniformly of any pair \(\alpha\), \( \beta\) of classes the class \(i(\alpha,\beta)\), representing the largest well-founded part of \(\alpha\) with respect to the relation encoded by \(\beta\)). As to Mahloness, the first principle -- called M -- states that (i) there is an operation \(u\) which associates to any class \(\alpha\) a universe \(u\alpha\), namely a class of classes, which contains \(\alpha\) and is closed under elementary comprehension and join; (ii) there exists an operation \(m\) such that that, if \(f\) is an operation mapping (non-extensional) classes into themselves, then \(m(f)\) is a universe closed under \(f\). The second principle, \(…
reviewed by: Andrea Cantini
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F65
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F25
zbMATH DE Number: 1882255
zbMATH Keywords: explicit mathematics
zbMATH Keywords: constructive set theory
zbMATH Keywords: realizability
zbMATH Keywords: foundations of constructive mathematics
zbMATH Keywords: Martin-Löf's type theories
zbMATH Keywords: Mahlo principles
zbMATH Keywords: lower bound
zbMATH Keywords: set representative
MaRDI profile type: Publication
cites work: Q3937387
cites work: Q3679172
cites work: Q4128540
cites work: Q3882452
cites work: Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
cites work: The strength of some Martin-Löf type theories
cites work: A well-ordering proof for Feferman's theoryT 0
cites work: Q3035279
cites work: First order theories for nonmonotone inductive definitions: Recursively inaccessible and Mahlo
cites work: Q4941991
cites work: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
cites work: Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
cites work: Constructive set theory
cites work: Ordinal notations based on a weakly Mahlo cardinal
cites work: Proof-theoretic analysis of KPM
cites work: Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM
cites work: Proof theory of reflection
cites work: Realizing Mahlo set theory in type theory
cites work: Q4944921
cites work: Inaccessibility in constructive set theory and type theory
cites work: Well-ordering proofs for Martin-Löf type theory
cites work: Extending Martin-Löf type theory by one Mahlo-universe
cites work: Wellordering proofs for metapredicative Mahlo
cites work: Q4936128
cites work: Q4215635
cites work: Realization of analysis into Explicit Mathematics
Recommended article: Generalizing realizability and Heyting models for constructive set theory
Recommended article: Q5477363
Recommended article: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
Recommended article: Q3079623
Recommended article: Q4453640
Recommended article: On the Constructive Dedekind Reals: Extended Abstract
Recommended article: EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS
Recommended article: Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
Recommended article: Realisability for infinitary intuitionistic set theory
Recommended article: The semantics of realizability for the constructive set theory based on hyperarithmetical predicates
description: scientific article; zbMATH DE number 1882255