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

DOI10.1016/0001-8708(85)90103-3MaRDI QIDQ1071017zbMATHOpenAlexFDO

Authors Harvey M. Friedman, Andre 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)

Recommendations

• Provably recursive functions of constructive and relatively constructive theories
• Indefiniteness in semi-intuitionistic set theories: on a conjecture of Feferman
• scientific article; zbMATH DE number 3264932
• Intuitionistic logic and implicit definability
• scientific article; zbMATH DE number 4189692
• scientific article; zbMATH DE number 4099295
• Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics
• Inaccessibility in constructive set theory and type theory
• scientific article; zbMATH DE number 1211956
• A negationless interpretation of intuitionistic theories

Cites work

• scientific article; zbMATH DE number 3645093 (Why is no real title available?)
• scientific article; zbMATH DE number 3427308 (Why is no real title available?)
• scientific article; zbMATH DE number 3427309 (Why is no real title available?)
• scientific article; zbMATH DE number 3652325 (Why is no real title available?)
• scientific article; zbMATH DE number 3652330 (Why is no real title available?)
• scientific article; zbMATH DE number 3668598 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• scientific article; zbMATH DE number 3346351 (Why is no real title available?)
• Corrigendum to ``Set existence property for intuitionistic theories with dependent choice
• Descriptive set theory
• Large sets in intuitionistic set theory
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Model theory
• On models with power-like orderings
• On power-like models for hyperinaccessible cardinals
• Sheaf models for set theory
• Some applications of the notions of forcing and generic sets
• The consistency of classical set theory relative to a set theory with intu1tionistic logic

Cited in

(25)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1071017)