Epistemic and intuitionistic formal systems (Q580343)

Recent interest in epistemic formal systems (that is, formal systems based on Lewis' modal logic (S4)) stems from efforts to `integrate' classical and intuitionistic mathematics. For this purpose the interpretation \((\cdot)^{\square}\) of intuitionistic propositional logic into epistemic propositional logic, described by \textit{J. McKinsey} and \textit{A. Tarksi} [J. Symb. Logic 13, 1-15 (1948; Zbl 0037.294)], has been extended to mathematical systems such as first-order arithmetic, type theory and set theory. For each of these it has been shown that \((\cdot)^{\square}\) provides a sound and faithful interpretation of the intuitionistic formal system into the corresponding epistemic one. The proofs that \((\cdot)^{\square}\) is conservative are quite different for different formal systems. The goal of the present paper is to describe one uniform method which can be used to obtain these conservative extension results for all the formal systems considered thus far. Our arguments are based on a syntactic formulation of Funayama's Theorem which asserts that any complete Heyting algebra can be embedded in a complete Boolean algebra by a map preserving finite meets and arbitrary joins. The second author has observed that another method of embedding a Heyting algebra into a Boolean algebra can be used to obtain our results. In this approach one formally adds Boolean terms in disjdunctive normal form. Here the interior operator has a simple syntactic description. The resulting Boolean algebra may not be complete, but, one works with regular open subsets.