[FOM] Embedding intuitionistic logic in classical

Alasdair Urquhart urquhart at cs.toronto.edu
Fri Sep 23 12:24:15 EDT 2011

I think a lot depends on what you mean by "embedding", as some
earlier postings have indicated.

For example, the following problem might have various
answers, depedning on the formulation:

> (i) Embedding intuitionistic propositional logic in classical 
> propositional logic.

If you assume that the embedding is efficient (polynomial-time),
then a positive answer would imply (by Statman's result) that
PSPACE = co-NP, a result that is considered unlikely.
On the other hand, intuitionistic propositional logic can
be efficiently embedded in quantified classical propositional
logic.  Rick Statman showed that an efficient embedding in the opposite
direct is also possible, thus showing that intuitionistic logic
is PSPACE-complete.

More information about the FOM mailing list