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

Todd Wilson twilson at csufresno.edu
Thu Nov 24 15:48:54 EST 2005

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:


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

More information about the FOM mailing list