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

Wed Oct 19 04:09:07 EDT 2016

Dear prof. Richard Zach,

        Thank very much for your observation on the representation of
Natural Deduction proofs. The lower-bounds obtained in Reckow's thesis as
well in Hrubes paper is strongly based on the fact that  an axiomatic
system is used and each line in the proof is  a formula, opposed to set of
formulas.   The understanding that a dag-like proof can be obtained  from a
Frege system by allowing  the use of a formula  more than once as a premise
is correct,  but does not applies directly to what we are doing and to
Lemmon style ND too.  One of the main features of ND is the discharging of
hypothesis, a device that Frege systems obtains  by means of the Deduction
Theorem (a Meta-Theorem). The implication-introduction rule is a powerful
device to shorten proofs, since we can have with it provide formation of
lemmas .Reckow's thesis discusses Natural Deduction in pages 64-68.  Below
we can read an excerpt of page 64, where  "this theorem"  is the Deduction
Theorem.

The important thing to note about this theorem, however, is that it provides
a new kind of inference rule. This rule· allows one to infer something
about the derivability of a certain formula from a certain set of formulas by
showing
a (possibly easier) derivation of a slightly different formula from a slightly
different set of hypotheses. Thus, there is the potential, at least, for much
shorter derivations by appealing to this rule.

The solution Reckow provides, afterwards,  for incorporating Natural
Deduction to Frege-like systems was to consider each line, in a more
general Frege system approach, as a pair  S |- A, where S is a set of
formulas and A is a formula. In this way, the Deduction Theorem is turned
into an inference rule, infer   S|- B -> A from S,B |- A.
But now, we have a problem for ensuring compression. There are
exponentially  many subsets of  sub formulas of the conclusion (the
sub-formula property).  The combinatorics changes against compression of
proofs if we consider this way of representing ND systems. There are proofs
of some formulas that have more than polynomially many pairs of the above
kind, we cannot ensure any more that a super-polynomially sized graph is
labeled with polynomially many labels (the lines), and hence there is at
least one  label (formula) that occurs polynomially many times in the
graph. It is essential in our approach that there are only polynomially
many  possible labels  (in fact there are only linearly many sub formulas
of the conclusion of the proof). The compression of the proof is provided
by collapsing these formulas that occurs super-polynomially many times, and
they exist because of the super-polynomial gap between the amount of labels
of the vertexes and the size of the graph itself.

Finally, if we consider Lemmon Style Natural Deduction, each line is a
formula plus the annotation indicating the premises (number line) used to
derive this formula.  As discussed above this system is more economical
than the (natural) solution proposed by Reckow thesis, that is in fact
quite close to those proof representations implemented by Gentzen's Sequent
Systems and Tableaux.

On the other hand, the use of Lemmon Style ND does not allow us to conclude
that the existent lower bound for Frege systems directly apply to ND.   A
dag-like proof, even in Lemmon Style,  cannot simply indicate that you  are
using a formula more than once. Each formula has it is own natural
dependency set of formulas. We cannot collapse equal formulas derived  from
different set of formulas without taking care of annotating the new
dependency, if we take this control seriously, we end up in a dag-like
proof as defined in our article, and having to adjust the annotations to
polynomial size and so on.

All the Best

On Tue, Oct 18, 2016 at 2:43 PM, Richard Zach <rzach at ucalgary.ca> wrote:

> Reckow's thesis is available here: https://www.cs.toronto.edu/~sa
> cook/homepage/reckhow_thesis.pdf
>
> If I understand the dag-like ND proofs used in the paper correctly, it's
> simply a matter of allowing a formula in a proof to be used more than once
> as a premise of a rule. So such a proof can be written as a sequence of
> formulas (eg, Lemmon style natural deduction)?  In any case, Reckow's
> result applies to dag-like ND systems, not just tree ND systems (afaict).
>
> -R
>
>
> On 2016-10-17 12:30 PM, Alasdair Urquhart wrote:
>
>> It's an old result that natural deduction systems for the
>> classical propositional calculus do not provide more than
>> a polynomial speedup over Hilbert-style proof systems.
>> This result already appears in the doctoral dissertation
>> of Robert Reckhow (U of Toronto 1975); it adapts immediately
>> to minimal and intuitionistic logic.
>>
>> Consequently, the claimed polynomial upper bound for the Prawitz
>> system of natural deduction also implies a polynomial upper
>> bound for minimal and hence intuitionistic propositional
>> logic in a Hilbert-style proof system.  This contradicts
>> Hrubes's exponential lower bound.
>>
>>
>> On Fri, 14 Oct 2016, Lew Gordeew wrote:
>>
>> Just adding my 5 cents to Hermann's exhaustive response to Alasdair's
>>> reply of Oct. 11, 2016.
>>>
>>> There is no contradiction. The APAL paper in question deals with
>>> Hilbert-style proof system IL, whereas our construction yields daglike
>>> natural deductions (ND). The corresponding daglike ND provablity is more
>>> sophisticated and the correlated dag-to-tree unfolding usually requires
>>> exponential growth in size. We don't see how to pass from our polysize
>>> daglike ND to a polysize proof in IL or any other Hilbert-Frege-style
>>> system (w.r.t. intuitionistic and/or minimal logic).
>>>
>>> Best,
>>> LG
>>>
>>> ---------------------------------------
>>> From: Alasdair Urquhart <urquhart at cs.toronto.edu>
>>> Date: Tue, Oct 11, 2016 at 10:34 PM
>>> Subject: [FOM]  Proof-theoretic proof of NP=PSPACE?
>>> To: Foundations of Mathematics <fom at cs.nyu.edu>
>>>
>>>
>>> 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.
>>>
>>
>>
> --
> Richard Zach ...... http://www.ucalgary.ca/rzach/
> Professor,             Department  of  Philosophy
> University of Calgary, Calgary AB T2N 1N4, Canada
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>

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