[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:
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
More information about the FOM
mailing list