[FOM] Gödel–McKinsey–Tarski translation

[Sergei Artemov]

Dear David,

This issue has been thoroughly discussed in
    S. Artemov. `Explicit provability and constructive semantics,' 
Bulletin of Symbolic Logic, vol. 7, No.1, pp. 1-36, 2001
(see also S. Artemov. "Modal logic in mathematics,"  Handbook of Modal 
Logic, Elsevier,  2006)

In particular, this paper provides an exact mathematical meaning of "A 
is constructively provable" by recovering Brouwer-Heyting-Kolmorogov 
(BHK) proofs from S4 derivations. This connects the Goedel project of 
providing (classical) provability semantics for intuitionistic logic to 
the intended BHK semantics of proofs for intuitionistic logic.

The main idea of Goedel-McKinsey-Tarski translation is to emulate in 
classical logic the principal intuitionistic paradigm 
"intuitionistically true=provable". Goedel's idea of 1933 was to read 
"provable" in this equation as "provable in the usual classical sense", 
hence reading the aforementioned paradigm as
    "intuitionistically true = classically provable".
Some authors have explored other approaches, e.g. "intuitionistically 
true = intuitionistically provable" with somewhat limited success though 
(cf. a wonderful survey D. van Dalen, Intuitionistic logic, Handbook of 
philosophical logic (D. Gabbay and F. Guenther, editors), vol. 3, 
Reidel, 1986, pp. 225–340. ).

 Kolmogorov's views of 1932 were close to ones by Goedel: to explain 
intuitionisitic logic via classical notions of problem/problem 
solutions/proof.

Given the modal logic S4 as the logic for classical provability, a 
natural reflex is to cast the "intuitionistically true = classically 
provable" paradigm as a translation of a given formula F in the 
intuitionistic language into the language of S4 by prefixing all 
subformulas in F by the provability modality []. We call the result of 
such a translation F^[].  Indeed, imagine a down-top procedure of 
determining the "intuitionistic truth value" if a formula given 
"intuitionistic truth values" of its subformulas. Such a procedure will 
have a classical counterpart, which repeats the same steps on F^[] and 
reads "intuitionistic truth" as "classical provability" since each 
subformula in F^[] is prefixed by the provability modality [].

Getting Goedel translation and McKinsey-Tarski translation from F^[] is 
now a technicality: all three are essentially equivalent in S4.

Due to some logical identities in S4 some of modalities in F^[] are 
redundant. For example, []([]A & []B) <-> ([]A & []B) in S4, hence one 
can save a prefix [] corresponding to the &-clause in the definition of 
F^[]. In addition, S4 proves A iff S4 proves []A, hence one can safely 
drop the outermost [] in F^[]. Finally, []\bot<->\bot in S4. These 
observations give us Goedel's translation F^g from F^[].

In McKinsey-Tarski translation F^mc, one has to box only atoms and 
implications in F. To connect F^mc with F^[] it now suffices to use an 
additional S4-identity
[]([]A v []B) <-> ([]A v []B), which is an easy exercise.

I hope this answers your question.

Regards,
Sergei Artemov
http://web.cs.gc.cuny.edu/~sartemov/





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