I want to know if there is a translation from intuitionistic propositional logic formulas to classical propositional logic formulas satisfying the properties I'm looking for.
Actually first part of my question is about existence of a mapping between two different model theories, for example between Heyting Algebras and Boolean Algebras. In the following you will understand that my main question is dependent to an answer to this question. I am speaking about a mapping which saves structure in a sense which I don't know how to express it formally.( I guess that it would be similar to a mapping from groups to rings! I mean they are from two different categories!) So what I'm asking here is that do we have such mappings? Did somebody ever try to make such a thing or maybe find a reason to do so?
After that, in the main part of my question, I want to know if we have a function which maps every formula in IPL to a formula in CPL while it saves it's value completely with respect to two model theories for IPL and CPL which are correspondent in the sense that I said.
More formally I am talking about a function $g$ and two model theories $\mathbb{M_\mathsf{I}}$ and $\mathbb{M_\mathsf{C}}$ which are respectively theories for IPL and CPL where $g$ is: $$g:\mathbb{M_\mathsf{I}}\rightarrow\mathbb{M_\mathsf{C}}$$
Be aware that $g$ has a property that I don't know how to express it formally! Intuitively I can say that it's a correspondence and it saves structure.
Can we have a function $f$ such that it gives a formula $\phi$ in IPL and maps it to a formula in IPC such that $$f(\phi)=\psi \Leftrightarrow {\Large \forall} \mathcal{M_\mathsf{I}} \in \mathbb{M_\mathsf{I}} : (\mathcal{M_\mathsf{I}} \models \phi \Rightarrow g(\mathcal{M_\mathsf{I}}) \models \psi) $$?
I have to say that my question comes from an intuitive thought that we maybe can translate a formula like ($\phi \lor \neg \phi$) from IPL to CPL and expect to have another formula with possibly different face and look which means exactly like what ($\phi \lor \neg \phi$) means in IPL!