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

joeshipman at aol.com joeshipman at aol.com
Wed Oct 12 23:43:37 EDT 2016

Wouldn't that only be the case if the translation went the other way? If the particular deductive calculus for minimal logic that the proof uses has ways to shorten proofs in the intuitionistic propositional calculus that don't translate back into short proofs in the intuitionistic propositional calculus, there isn't a contradiction.

-- JS

-----Original Message-----
From: Alasdair Urquhart <urquhart at cs.toronto.edu>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Wed, Oct 12, 2016 3:19 pm
Subject: [FOM]  Proof-theoretic proof of NP=PSPACE?

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.

FOM mailing list
FOM at cs.nyu.edu

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20161012/aa97b2d0/attachment.html>

More information about the FOM mailing list