[FOM] Embedding intuitionistic logic in classical

[ARF (Richard L. Epstein)]

All these issues except those about length of computation are analyzed both technically and in terms of ideas about what translations mean in the chapter on translations in my Propositional Logics.  Preserving some structure of a language via translation is crucial if we are talking about translations and meaning rather than just mathematical embeddings, but whether the translation need be a homomorphism is not clear.

Staffan Angere wrote:

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