The lack of definable witnesses and provably recursive functions in intuitionistic set theories
type: Item
instance of: scholarly article
title: The lack of definable witnesses and provably recursive functions in intuitionistic set theories
zbMATH Open document ID: 0585.03025
DOI: 10.1016/0001-8708(85)90103-3
author: Harvey M. Friedman
author: Andre Scedrov
published in: Advances in Mathematics
publication date: 1985-01-01T00:00:00Z
review text: Let \(ZFI_ R\), \(ZFI_ C\) be intuitionistic Zermelo-Fraenkel set theory formulated with Replacement, resp. Collection. It is known that \(ZFI_ R\) has the existence property. It is shown that \(ZFI_ C\) does not have the existence property. This remains true if one adds Dependent Choice and all true \(\Sigma_ 1\)-sentences of ZF. It is known that ZF and \(ZFI_ C\) have the same provably recursive functions. It is shown that this is not true for \(ZFI_ C\) and \(ZFI_ R\). (From the authors' summary).
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 3937170
zbMATH Keywords: intuitionistic Zermelo-Fraenkel set theory
zbMATH Keywords: Replacement
zbMATH Keywords: Collection
zbMATH Keywords: existence property
zbMATH Keywords: Dependent Choice
zbMATH Keywords: provably recursive functions
reviewed by: B. van Rootselaar
MaRDI profile type: Publication
full work available at URL: 0001-8708(85)90103-3
OpenAlex ID: W2052161854
cites work: Q3866108
cites work: Model theory
cites work: Some applications of the notions of forcing and generic sets
cites work: Sheaf models for set theory
cites work: Q3050433
cites work: Q3214890
cites work: The consistency of classical set theory relative to a set theory with intu1tionistic logic
cites work: Q4179016
cites work: Corrigendum to ``Set existence property for intuitionistic theories with dependent choice''
cites work: Large sets in intuitionistic set theory
cites work: Q3852176
cites work: Q3852172
cites work: Q5622191
cites work: Descriptive set theory
cites work: Q3214891
cites work: Q5573961
cites work: On power-like models for hyperinaccessible cardinals
cites work: On models with power-like orderings
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
Recommended article: Provably recursive functions of constructive and relatively constructive theories
Recommended article: INDEFINITENESS IN SEMI-INTUITIONISTIC SET THEORIES: ON A CONJECTURE OF FEFERMAN
Recommended article: Q5551452
Recommended article: Intuitionistic logic and implicit definability
Recommended article: Q5753927
Recommended article: Q3824312
Recommended article: Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics
Recommended article: Inaccessibility in constructive set theory and type theory
Recommended article: Q4214077
Recommended article: A negationless interpretation of intuitionistic theories
description: scientific article; zbMATH DE number 3937170