[FOM] can the classicist understand the intuitionist? if not, why?
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
> 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,
 /\  /\  /\ (k) k ||- phi,
should have been
 /\  /\  -> (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