Topological models of epistemic set theory (Q916657)

For several years, the author has been championing the cause of epistemic mathematics, as a kind of synthesis of classical set-theoretical mathematics and intuitionistic mathematics. [See his paper: The knowing mathematician, Synthese 60, 21-38 (1984; Zbl 0543.01006).] Epistemic set theory is set theory with classical S4 as its underlying logic, with a weakened form of extensionality: two sets are taken to be the same if they necessarily have (i.e. if they are known to have) the same elements. It is shown in this paper that one cannot prove in epistemic set theory that there is a discontinuous function which we know to be effective. This generalizes a famous result of Scott's, who found a topological interpretation of intuitionistic analysis, including Brouwer's theorem that all functions are continuous on closed intervals [cf. \textit{D. Scott}, Intuitionism and proof theory, Proc. Summer Conf. Buffalo N.Y. 1968, 235-255 (1970; Zbl 0213.012)]. The paper is divided into three parts. In the first part the author introduces intensional modal set theory and topological models of it. In the second part he develops epistemic set theory and shows how to interpret it in the extensional modal set theory of the first part. In the third part he specializes to Scott's model and he derives the result mentioned above and some other ones, concerning Kripke's scheme and Markov's principle.