Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most ...natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever (∃x)ϕ(x) is provable, there is a formula χ(x) such that (∃!x)ϕ(x)∧χ(x) is provable. It has been known since the 80s that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has remained open until now whether EP holds for the most well known constructive set theory, CZF. In this paper we show that EP fails for CZF.
Full text
Available for:
GEOZS, IJS, IMTLJ, KILJ, KISLJ, NLZOH, NUK, OILJ, PNG, SAZU, SBCE, SBJE, UILJ, UL, UM, UPCLJ, UPUK, ZAGLJ, ZRSKP
This article presents a common generalization of the two main methods for obtaining class models of constructive set theory. Heyting models are a generalization of the Boolean models for classical ...set theory which are a variant of forcing, while realizability is a decidedly constructive method that has first been developed for number theory by Kleene and was later very fruitfully adapted to constructive set theory. In order to achieve the generalization, a new kind of structure (applicative topologies) is introduced, which contains both elements of formal topology and applicative structures. This approach not only deepens the understanding of class models and leads to more efficiency in proofs about these kinds of models, but also makes it possible to prove new results about the two special cases that were not known before and to construct new models.
► Realizability and Heyting constructions provide models for constructive set theory. ► We work in the predicative framework of CZF. ► We propose a common generalization of the two constructions. ► This can be used to construct new models and generalize results.
Full text
Available for:
GEOZS, IJS, IMTLJ, KILJ, KISLJ, NLZOH, NUK, OILJ, PNG, SAZU, SBCE, SBJE, UILJ, UL, UM, UPCLJ, UPUK, ZAGLJ, ZRSKP
PDF
