[FOM] A proof-theoretic proof of NP=PSPACE

[Edward Hermann Haeusler]

Dear prof. Alasdair and all members of FOM,

I have just entered the mail-list. I got aware of the message from prof.
Alasdair regarding Pavel Hrubes result, from a message sent to me by a
friend that takes part of the group. I would like and have to comment below
your concern, professor.

Thank you very much for pointing out this apparent  contradiction with our
result. In fact, there is no contradiction at all. What Pavel Hrubes proved
 is that there is an exponential lower-bound on proofs in intuitionistic
propositional logic carried out  in Frege systems (axiomatic systems). The
size of a proof  in his result is taken as the number of lines. Our result,
on other hand, consider proofs as graphs, in fact dag-like rooted simple
graphs. We show that there is exponential speedup in this case. But, of
course there is a long track until get into dags.

The proofs in our system can be thought  as resulting from collapsing
tree-like normal proofs  in implicational minimal Natural Deduction (N.D.)
system. Of course, we take also in account a cubic translation from
Intuitionistic full propositional language into purely implicational
minimal logic.
The tree-like proofs of a minimal tautology, w.l.g, are take as height
 polynomial upper-bounded proofs, reasons explained in the P.S. That is,
every path from any assumption to the conclusion is polynomially bounded in
these proofs. We then apply a procedure (bottom-up) that collapses vertexes
of this tree that are labeled with the same formula. The resulting graph is
not a tree anymore, it is a dag-like proof, with root (the conclusion).
This collapsing is applied level by level, from bottom-up. Since we have
polynomially many possible sub formulas of the conclusion (we started with
a normal proof in N.D.) and the height is polynomially bounded, the
procedure yields a dag-like proof (rooted) with polynomially many vertexes.
The trickier part is to provide an encoding for the labels of the edges
that takes care of the control whether each leaf-formula is closed
(discharged) or not. Note that even having a polynomial dag, we may have
exponentially many paths. The code of the dag takes care of this feature in
a polynomial way, ensuring also that  the verification is polynomially
bounded regarded to time. This last part is fairly more complicated and
hard to explain in an email message.

Resuming:

We obtain dag-like proofs (with roots) as proofs. The Horizontal
compression that we obtain produces dag-like proofs that at each level (it
is a rooted graph) and roughly for every sub-formula of the conclusion of
the proof, there is at most  one vertex labeled with this formula in this
level. The speedup between Frege systems and our system is exponential,
indeed.


Thank you very much for taking attention to our article.



All the best,


Hermann

P.S. The fact that we can start the demonstration with polynomially bounded
on height Natural Deduction implication minimal logic proofs is a
consequence of a height-bounded map from Hudelmeier's sequent calculus to
Natural Deduction, shown in our article. Hudelmeier sequent calculus
produces cut-free proofs bounded on the height for any minimal logic
tautology (this is not in our article, but can be read in J. Log.
Comput. 3(1)
<http://dblp.uni-trier.de/db/journals/logcom/logcom3.html#Hudelmaier93>:
63-75 (1993)

-- 
Edward Hermann Haeusler
Associate Professor
Department of Informatics
PUC-Rio
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20161012/0ffaeba2/attachment.html>