The lack of definable witnesses and provably recursive functions in intuitionistic set theories

DOI10.1016/0001-8708(85)90103-3zbMath0585.03025OpenAlexW2052161854MaRDI QIDQ1071017

Harvey M. Friedman, Andrej Scedrov

Publication date: 1985

Published in: Advances in Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0001-8708(85)90103-3

zbMATH Keywords

Collectionexistence propertyReplacementprovably recursive functionsintuitionistic Zermelo-Fraenkel set theoryDependent Choice

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50)

Related Items (22)

Lindenbaum algebras of intuitionistic theories and free categories ⋮ CZF does not have the existence property ⋮ On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis ⋮ Eighth Latin American Symposium on Mathematical Logic, João Pessoa ⋮ Relating first-order set theories, toposes and categories of classes ⋮ Relativized ordinal analysis: the case of power Kripke-Platek set theory ⋮ Choice and independence of premise rules in intuitionistic set theory ⋮ Constructing the constructible universe constructively ⋮ SEPARATING FRAGMENTS OF WLEM, LPO, AND MP ⋮ From the weak to the strong existence property ⋮ Effectivity properties of intuitionistic set theory with collection scheme ⋮ Intuitionistic sets and ordinals ⋮ Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory ⋮ Independence results around constructive ZF ⋮ Characterizing the interpretation of set theory in Martin-Löf type theory ⋮ Certain partial conservativeness properties of intuitionistic set theory with the principle of double complement of sets ⋮ On the constructive Dedekind reals ⋮ SEPARATING THE FAN THEOREM AND ITS WEAKENINGS II ⋮ The disjunction and related properties for constructive Zermelo-Fraenkel set theory ⋮ Towards a computation system based on set theory ⋮ A categorical reading of the numerical existence property in constructive foundations ⋮ Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Corrigendum to ``Set existence property for intuitionistic theories with dependent choice
• Large sets in intuitionistic set theory
• Descriptive set theory
• Sheaf models for set theory
• Model theory
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On power-like models for hyperinaccessible cardinals
• The consistency of classical set theory relative to a set theory with intu1tionistic logic
• On models with power-like orderings
• Some applications of the notions of forcing and generic sets

This page was built for publication: The lack of definable witnesses and provably recursive functions in intuitionistic set theories