Proof Compression and NP Versus PSPACE II

Lew Gordeev; Edward Hermann Haeusler

Bulletin of the Section of Logic (2020)

  • Volume: 49, Issue: 3, page 213-230
  • ISSN: 0138-0680

Abstract

top
We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight (= total number of symbols) and time complexity of the provability involved are both polynomial in the weight of ρ. As is [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had (by the definition of validity) a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size (= total number of nodes), and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is (possible but) not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP.

How to cite

top

Lew Gordeev, and Edward Hermann Haeusler. "Proof Compression and NP Versus PSPACE II." Bulletin of the Section of Logic 49.3 (2020): 213-230. <http://eudml.org/doc/296796>.

@article{LewGordeev2020,
abstract = {We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight (= total number of symbols) and time complexity of the provability involved are both polynomial in the weight of ρ. As is [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had (by the definition of validity) a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size (= total number of nodes), and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is (possible but) not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP.},
author = {Lew Gordeev, Edward Hermann Haeusler},
journal = {Bulletin of the Section of Logic},
keywords = {natural deduction; sequent calculus; minimal logic; computational complexity},
language = {eng},
number = {3},
pages = {213-230},
title = {Proof Compression and NP Versus PSPACE II},
url = {http://eudml.org/doc/296796},
volume = {49},
year = {2020},
}

TY - JOUR
AU - Lew Gordeev
AU - Edward Hermann Haeusler
TI - Proof Compression and NP Versus PSPACE II
JO - Bulletin of the Section of Logic
PY - 2020
VL - 49
IS - 3
SP - 213
EP - 230
AB - We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight (= total number of symbols) and time complexity of the provability involved are both polynomial in the weight of ρ. As is [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had (by the definition of validity) a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size (= total number of nodes), and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is (possible but) not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP.
LA - eng
KW - natural deduction; sequent calculus; minimal logic; computational complexity
UR - http://eudml.org/doc/296796
ER -

References

top
  1. [1] S. Arora, B. Barak, Computational Complexity: A Modern Approach, 1st ed., Cambridge University Press, USA (2009). 
  2. [2] L. Gordeev, Proof compression and NP versus PSPACE. Part 2, CoRR, vol. abs/1907.03858 (2019), URL: http://arxiv.org/abs/1907.03858 
  3. [3] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica, vol. 107(1) (2019), pp. 53–83, DOI: http://dx.doi.org/10.1007/s11225-017-9773-5 
  4. [4] J. Holm, E. Rotenberg, M. Thorup, Planar Reachability in Linear Space and Constant Time, CoRR, vol. abs/1411.5867 (2014), URL: http://arxiv.org/abs/1411.5867 
  5. [5] J. Hudelmaier, An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic, Journal of Logic and Computation, vol. 3(1) (1993), pp. 63–75, DOI: http://dx.doi.org/10.1093/logcom/3.1.63 
  6. [6] H. Ishihara, H. Schwichtenberg, Embedding classical in minimal implicational logic, Mathematical Logic Quarterly, vol. 62(1–2) (2016), pp. 94–101, DOI: http://dx.doi.org/10.1002/malq.201400099 
  7. [7] I. Johansson, Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compositio Mathematica, vol. 4 (1937), pp. 119–136, URL: http://www.numdam.org/item/CM_1937__4__119_0 
  8. [8] C. H. Papadimitriou, Computational complexity, Addison-Wesley (1994). 
  9. [9] D. Prawitz, Natural Deduction: A Proof-theoretical Study, Almqvist & Wiksell (1965). 
  10. [10] D. Prawitz, P.-E. Malmnäs, A Survey of Some Connections Between Classical, Intuitionistic and Minimal Logic, [in:] H. A. Schmidt, K. Schütte, H.-J. Thiele (eds.), Contributions to Mathematical Logic, vol. 50 of Studies in Logic and the Foundations of Mathematics, Elsevier (1968), pp. 215–229, DOI: http://dx.doi.org/10.1016/S0049-237X(08)70527-5 
  11. [11] R. Statman, Intuitionistic Propositional Logic is Polynomial-Space Complete, Theoretical Computer Science, vol. 9 (1979), pp. 67–72, DOI: http://dx.doi.org/10.1016/0304-3975(79)90006-9 
  12. [12] V. Svejdar, On the polynomial-space completeness of intuitionistic propositional logic, Archive for Mathematical Logic, vol. 42(7) (2003), pp. 711–716, DOI: http://dx.doi.org/10.1007/s00153-003-0179-x 
  13. M. Thorup, Compact oracles for reachability and approximate distances in planar digraphs, Journal of the ACM, vol. 51(6) (2004), pp. 993–1024, DOI: http://dx.doi.org/10.1145/1039488.1039493 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.