Epistemic set theory is a conservative extension of intuitionistic set theory

In [6] Gödel observed that intuitionistic propositional logic can be interpreted in Lewis's modal logic (S4). The idea behind this interpretation is to regard the modal operator □ as expressing the epistemic notion of “informal provability”. With the work of Shapiro [12], Myhill [10], Goodman [7], [8], and Ščedrov [11] this simple idea has developed into a successful program of integrating classical and intuitionistic mathematics.There is one question quite central to the above program that has remained open. Namely:Does Ščedrov's extension of the Gödel translation to set theory provide a faithful interpretation of intuitionistic set theory into epistemic set theory?In the present paper we give an affirmative answer to this question.The main ingredient in our proof is the construction of an interpretation of epistemic set theory into intuitionistic set theory which is inverse to the Gödel translation. This is accomplished in two steps. First we observe that Funayama's theorem is constructively provable and apply it to the power set of 1. This provides an embedding of the set of propositions into a complete topological Boolean algebra . Second, in a fashion completely analogous to the construction of Boolean-valued models of classical set theory, we define the -valued universe V(). V() gives a model of epistemic set theory and, since we use a constructive metatheory, this provides an interpretation of epistemic set theory into intuitionistic set theory.