1 results
EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY
- Part of
-
- Journal:
- The Journal of Symbolic Logic / Volume 88 / Issue 3 / September 2023
- Published online by Cambridge University Press:
- 20 July 2022, pp. 1138-1169
- Print publication:
- September 2023
-
- Article
-
- You have access
- HTML
- Export citation
-
In [17], we introduced an extensional variant of generic realizability [22], where realizers act extensionally on realizers, and showed that this form of realizability provides inner models of
$\mathsf {CZF}$ (constructive Zermelo–Fraenkel set theory) and 
$\mathsf {IZF}$ (intuitionistic Zermelo–Fraenkel set theory), that further validate 
$\mathsf {AC}_{\mathsf {FT}}$ (the axiom of choice in all finite types). In this paper, we show that extensional generic realizability validates several choice principles for dependent types, all exceeding 
$\mathsf {AC}_{\mathsf {FT}}$. We then show that adding such choice principles does not change the arithmetic part of either 
$\mathsf {CZF}$ or 
$\mathsf {IZF}$.
