[FOM] Proof-theoretic proof of NP=PSPACE?

Alasdair Urquhart urquhart at cs.toronto.edu
Tue Oct 11 22:34:06 EDT 2016

I think there must be an error in this proof somewhere.
Pavel Hrubes proved an exponential lower bound on
proofs in the intuitionistic propositional calculus
(Annals of Pure and Applied Logic, Volume 146 (2007),
pp. 72-90.  There is an efficient translation from
intuitionistic logic into minimal logic, so the
claimed result contradicts the theorem of Hrubes.

More information about the FOM mailing list