[FOM] Embedding intuitionistic logic in classical

[Staffan Angere]

It is indeed a very surprising result, at least to me. Of course, one could require that the translations be some kind of homomorphisms, and thereby exclude the ones given in Jerabek's paper, but this seems somewhat arbitrary, at least if we want to use translatability to compare the expressive power of logic systems. For that, it seems like it should be quite enough that the translation should be computable.

As  a corollary, one could argue that the question of which logic is the "right" one is misplaced. The main disadvantage of working intuitionistically in classical propositional logic would be that the sentences used will be a lot longer and more complex than they are in intuitionistic logic. But this is a purely pragmatic difference, so in a way Carnap might have been entirely right to hold the choice of language (and logic) to be nothing but a practical problem.

The disclaimer here is, of course, that the result doesn't guarantee computability of the translation for predicate logics. I wonder if it could be extended?

Staffan

________________________________________
Från: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] för Joao Marcos [botocudo at gmail.com]
Skickat: den 25 september 2011 18:50
Till: fom at cs.nyu.edu
Ämne: Re: [FOM] Embedding intuitionistic logic in classical

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/
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom