[FOM] Embedding intuitionistic logic in classical

[ARF (Richard L. Epstein)]

The first and third of these questions are answered in the negative in my book Propositional Logics.

R. Epstein

Staffan Angere wrote:

> Dear FOMathicians,
>
> this may be a somewhat trivial question, but I have not found the answer anywhere yet, and I have not managed to prove or disprove it on my own. Classical propositional logic can be embedded in intuitionistic propositional logic via Glivenko's theorem, and classical predicate logic can be embedded in intuitionistic predicate logic using the negative translation. Furthermore, intuitionistic propositional logic can be embedded in classical S4 logic. But is any of the following possible?
>
> (i) Embedding intuitionistic propositional logic in classical propositional logic.
> (ii) Embedding intuitionistic predicate logic in classical predicate logic.
> (iii) Embedding intuitionistic S4 propositional logic in classical S4 propositional logic.
>
> My (current) guess would be no to all of these, but I have not been able to prove this. It does, however, feel like it should be common knowledge among logicians.
>
> Best wishes,
> Staffan
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom