[FOM] can the classicist understand the intuitionist? if not, why?

[Joao Marcos]

> Arnon Avron wrote:
> >2) Can one define in intuitionistic logic counterparts of the
> >classical connectives so that the resulting translation
> >preserves the consequence relation of classical logic?
>
Giovanni Sambin then wrote:
> The so-called double-negation interpretation, or Goedel-Gentzen
> translation of the 30s, which sends a formula A to a formula A*,
> allows one to prove that:
>   Gamma|- Delta is provable in classical logic
> if and only if
> Gamma*|- Delta* is provable in intuitionistic logic,
> actually, in minimal logic (Gamma* is of course A1*,...,An*
> if Gamma=A1,...An)
> (for a proof, see e.g. Troelstra-van Dalen, Constructivism in
> mathematics, an introduction, vol. 1, North-Holland 1988, pp. 57-59)
>
> When I explain this to students I say: the intuitionist can
> understand what the classicist says, including his proofs,
> but not conversely (unless one adds an extra modality).

This last observation makes me wonder:

Does anyone know of a PROOF that there is NO converse translation,
from (the consequence relation of) intuitionistic logic into classical
logic, i.e., a proof that there is no (recursive?) mapping * such that

Gamma |- Delta is provable in intuitionistic logic
iff
Gamma* |- Delta* is provable in classical logic

???

Or maybe someone can exhibit here such a translation, for my illustration?

***

BTW, how is the procedure of "adding an extra modality" that will help
the classicist understand the intuitionist?

JM