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

[Todd Wilson]

Joao Marcos wrote:
> 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?

I did exactly that in my FOM posting of Wed Nov 9 01:36:33 EST 2005:

     http://www.cs.nyu.edu/pipermail/fom/2005-November/009321.html

The translation was based on the completeness of Kripke semantics for 
Intuitionistic Predicate Logic.  Also, let me take this opportunity to 
make a small correction to that posting that was pointed out to me by 
Arnon Avron:  The last formula appearing there,

     [1] /\ [2] /\ [3] /\ (k) k ||- phi,

should have been

     [1] /\ [2] /\ [3] -> (Ak) k ||- phi.

--
Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh