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

[joeshipman at aol.com]

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
http://www.cs.nyu.edu/mailman/listinfo/fom

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