[FOM] Gödel–McKinsey–Tarski translation

[David Fontaine]

Dear all,

I would like to start here a discussion on the
Gödel–McKinsey–Tarski translation: a formula is
provable in propositional intuitionistic logic if and
only if its translation is provable in the classical
modal logic S4.  S4 is the so-called "modal companion"
of intuitionistic logic.

My interest in this translation lies in the fact that
it provides a classical point of view of non-classical
logics. This is very useful for my
classically-educated mind :-) I read that, in this
context, a formula []A in S4 (where [] is the modality
of S4) should be understood as "A is constructively
provable". For example, an atomic formula p is  then
translated into []p. Could anyone provide some
intuitive explanation on why this translation works
and on its philosophical meaning?

This translation can be generalized to intermediate
logic up to classical logic whose modal companion is
then S5. I also found a similar result by GoldBlatt
which provides a translation from MQL (minimal quantum
logic) to the classical modal logic B. a formula is
provable in MQL if and only if its translation is
provable in B. In this case an atomic formula p is
translated into []<>p (where <> is ~[]~, where ~ is
negation). I cannot see the intuitive meaning of this
translation and would appreciate some explanation.

Is there a similar result for linear logic? In my
opinion a formula A->B in linear logic should be
translated into something like A -> <>B meaning that
if I have A, then I CAN have B.  From A -> <>B and A
-> <>C one can deduce A -> (<>B /\ <>C), but cannot
deduce A -> <>(B /\ C). It would explain why in linear
logic from A->B and A->C you cannot deduce A->(B/\C).
This idea seems obvious and has probably been studied
before. Would you have any reference?

Are there other similar translation from non-classical
logics to classical modal logic? Can they be put in a
unified framework? 

Thanks in advance for your comments and replies.

David






      _____________________________________________________________________________ 
Ne gardez plus qu'une seule adresse mail ! Copiez vos mails vers Yahoo! Mail http://mail.yahoo.fr