 Jónsson and Tarski (1951, Thm. 3.14) showed that any closure algebra is isomorphic to an algebraic system formed by a set equipped with a reflexive and transitive  relation.[67]  As a matter of fact, the relevant algebraic structure is precisely that of the propositional modal logic \(\mathbf{S4}\). Hence the propositional part of \(\mathbf{EIFL}\) has the same algebraic structure as \(\mathbf{S4}\). By a well-known result due to Gödel (1933) and McKinsey &amp; Tarski (1948), intuitionistic propositional logic can be interpreted in \(\mathbf{S4}\), via a translation \(t\) such that \(\phi\) is intuitionistically provable iff \(t(\phi)\) is a valid \(\mathbf{S4}\) formula. Thus, intuitionistic propositional logic is interpretable in  \(\mathbf{EIFL}\).[68]