Globalization of intuitionistic set theory
type: Item
instance of: scholarly article
title: Globalization of intuitionistic set theory
zbMATH Open document ID: 0633.03050
DOI: 10.1016/0168-0072(87)90081-9
author: Gaisi Takeuti
author: Satoko Titani
published in: Annals of Pure and Applied Logic
publication date: 1987-01-01T00:00:00Z
review text: \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.
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03E40
zbMATH DE Number: 4029549
zbMATH Keywords: complete Heyting algebra
zbMATH Keywords: sheaf model
zbMATH Keywords: embedding
zbMATH Keywords: apartness relation
zbMATH Keywords: global concepts
zbMATH Keywords: global intuitionistic set theory GIZF
MaRDI profile type: Publication
full work available at URL: 0168-0072(87)90081-9
OpenAlex ID: W2026053661
cites work: Q5793835
cites work: Q3852176
cites work: Extending Gödel's negative interpretation to ZF
cites work: Q5559220
cites work: Q3939796
cites work: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory
Recommended article: Completeness of global intuitionistic set theory
Recommended article: Global quantification in Zermelo-Fraenkel set theory
Recommended article: Q5498681
Recommended article: Global intuitionistic analysis
Recommended article: Intuitionistic fixed point theories over set theories
Recommended article: Q3720593
Recommended article: The intuitionistic alternative set theory
Recommended article: Sets, Topoi and Intuitionism
Recommended article: Q5691486
Recommended article: On the quantificational logic of intuitionistic set theory
description: scientific article; zbMATH DE number 4029549