# [FOM] Gödel–McKinsey–Tarski translation

Sergei Artemov sartemov at gc.cuny.edu
Sat Feb 23 15:09:04 EST 2008

```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
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",
"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
[]([]A v []B) <-> ([]A v []B), which is an easy exercise.

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

```