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

[Alasdair Urquhart]

Formulate minimal (ML) and intuitionistic logic (IL) with a propositional
constant F (falsum), axiom schemes and modus ponens.
Then IL has the extra axiom scheme F -> A for any
formula A.

Let B be any formula of IL, and F(B) the conjunction of all formulas
F -> p, where p is a variable in B.  Then F(B) -> B is provable
in ML if and only if B is provable in IL.  Furthermore,
the proof of B in IL is only a little longer
than the proof of F(B) -> B in ML.

Hence, if there is a polynomial bound on the length of
proofs in ML, there is also a polynomial bound
on the length of proofs in IL, contradicting
the result of Pavel Hrubes.

On Wed, 12 Oct 2016, joeshipman at aol.com wrote:

> 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.