[FOM] Embedding intuitionistic logic in classical

[Alasdair Urquhart]

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.