[FOM] Embedding intuitionistic logic in classical

[Joao Marcos]

Hello, Staffan:

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

This "iff" is precisely the definition of *conservative translation*,
which I mentioned in my earliest response.

What the recent positive (and somewhat surprising) result by Jerabek
shows is that it is really easy to produce such kinds of (effective)
"embedding" between two given logics (consequence relations) --- and
between classical and intuitionistic logics in particular.  What the
negative result by Epstein shows, on the other hand, is that this very
definition of "embedding" (as conservative translation) does NOT
really preserve enough structure: if your notion of "embedding" is
_grammatical_ then the result you're looking for turns out
unobtainable.

So, it would seem "grammaticality" should qualify your reading of
Gödel's intuitions concerning translations between logic systems.

Joao Marcos

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