[FOM] Embedding intuitionistic logic in classical

[Staffan Angere]

Thank you all for the pointers; I guess I should have been much more explicit about what I meant with "embedding". I was thinking in terms of a function f between logics L, L' such that A |- p in L iff f[A] |- f(p) in L', i.e. a kind of structure-preserving and reflecting mapping, where the structure is given by the consequence relation.

The reason I have been interested in this question is because I think that either mutual embeddability or its negation would tell us something important about the expressive strength of classical versus intuitionistic logic. As is known, Gödel saw his translation as an indication that intuitionistic logic is richer than classical, but this strictly only holds if the converse translation is impossible.

Again, thanks for all the pointers!

Staffan