[FOM] Embedding intuitionistic logic in classical

[Joao Marcos]

> 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.

I guess the answer pretty much depends on what you mean by "embedding
a logic into another".

One possibility is to *(conservatively) translate* a logic L1 into a
logic L2 (as in the theorems by Glivenko, Godel and Kuroda), by
providing an inference-preserving mapping from the formulas of L1 into
the formulas of L2.

In that sense, however, a result announced by Jerabek just a few weeks
ago (http://arxiv.org/abs/1108.6263) claims that there are
conservative translations between "(almost) any two reasonable
deductive systems".  It follows from those results that the answer to
your questions (i) and (iii) is yes.  Moreover, the paper also shows
the translations to be computable, in both cases (i) and (ii).

JM

-- 
http://sequiturquodlibet.googlepages.com/