Globalization of intuitionistic set theory (Q1095903)

\textit{R. J. Grayson} has shown [A sheaf approach to models of set theory, M. Sc. Thesis, Oxford (1975)] that in a universe V of intuitionistic set theory \(ZF_ I\) if \(\Omega\) is a complete Heyting algebra (cHa), then one can construct an \(\Omega\)-valued sheaf model \(V^{(\Omega)}\) of \(ZF_ I\), and that the universe V can be embedded in \(V^{(\Omega)}\), that is, there exists a canonical embedding \({\hat{\;}}: V\to V^{(\Omega)}\) such that \(x=y\) implies \([[ \check x=\check y]]=1\) and \(x\in y\) implies \([[ \check x\in \check y]]=1\), where \([[ \phi ]]\) is the truth value of \(\phi\) in \(V^{(\Omega)}\). We call a member of \(V^{(\Omega)}\) of the form \(\check x\) a check set. Furthermore, if an apartness relation to 0 is defined on \(\Omega\), then \(x=y\) iff \([[ \check x=\check y]]=1\) and \(x\in y\) iff \([[ \check x\in \check y]]=1\); thus the universe V is embedded in \(V^{(\Omega)}\) as a submodel. However, the copy \(\check V=\{\check x: x\in V\}\) of V is not expressible in the language of \(ZF_ I\) on \(V^{(\Omega)}\), since the concepts expressible in the language of \(ZF_ I\) on \(v^{(\Omega)}\) are local, whereas \(\check V\) is a global concept. The aim of this paper is to present an intuitionistic set theory in which the global concepts are expressible. We call this theory the global intuitionistic set theory GIZF.