[FOM] can the classicist understand the intuitionist? if not, why?
botocudo at gmail.com
Wed Nov 23 17:40:11 EST 2005
> 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
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?
More information about the FOM