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

DOI10.1016/0001-8708(85)90103-3zbMATH Open0585.03025OpenAlexW2052161854MaRDI QIDQ1071017FDOQ1071017

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

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

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)

Cites Work

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

Cited In (25)

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

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)