Studia Logica

, Volume 107, Issue 1, pp 53–83 | Cite as

Proof Compression and NP Versus PSPACE

  • L. GordeevEmail author
  • E. H. Haeusler


We show that arbitrary tautologies of Johansson’s minimal propositional logic are provable by “small” polynomial-size dag-like natural deductions in Prawitz’s system for minimal propositional logic. These “small” deductions arise from standard “large” tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying geometric idea: if the height, \(h\left( \partial \right) \), and the total number of distinct formulas, \(\phi \left( \partial \right) \), of a given tree-like deduction \(\partial \) of a minimal tautology \(\rho \) are both polynomial in the length of \(\rho \), \(\left| \rho \right| \), then the size of the horizontal dag-like compression \(\partial ^{{\textsc {c}} }\) is at most \(h\left( \partial \right) \times \phi \left( \partial \right) \), and hence polynomial in \(\left| \rho \right| \). That minimal tautologies \( \rho \) are provable by tree-like natural deductions \(\partial \) with \(\left| \rho \right| \)-polynomial \(h\left( \partial \right) \) and \(\phi \left( \partial \right) \) follows via embedding from Hudelmaier’s result that there are analogous sequent calculus deductions of sequent \(\Rightarrow \rho \). The notion of dag-like provability involved is more sophisticated than Prawitz’s tree-like one and its complexity is not clear yet. Our approach nevertheless provides a convergent sequence of NP lower approximations of PSPACE-complete validity of minimal logic (Savitch in J Comput Syst Sci 4(2):177–192, 1970); Statman in Theor Comput Sci 9(1):67–72, 1979; Svejdar in Arch Math Log 42(7):711–716, 2003).


Minimal logic Proof theory Digraphs Propositional complexity 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.



This work arose in the context of term- and proof-compression research supported by the ANR/DFG projects HYPOTHESES and BEYOND LOGIC [DFG Grants 275/16-1, 16-2, 17-1] and the CNPq project Proofs: Structure, Transformations and Semantics [Grant 402429/2012-5]. We thank L. C. Pereira and all colleagues in PUC-Rio for their contribution as well as P. Schroeder-Heister (EKUT) and M. R. F. Benevides (UFRJ) for their support of these projects. Special thanks goes to S. Buss, R. Dyckhoff, F. Gilbert, G. Kalachev and (very special) to T. Klimpel for insightful comments and valuable suggestions.


  1. 1.
    Gordeev, L., Basic dag compressions, Manuscript 2015.Google Scholar
  2. 2.
    Hudelmaier, J., An \(o\left( n\log n\right)\)-space decision procedure for intuitionistic propositional logic, Journal of Logic and Computation 3(1): 63–75, 1993.CrossRefGoogle Scholar
  3. 3.
    Johansson, I., Der minimalkalkül, ein reduzierter intuitionistischer formalismus, Compositio Mathematica 4: 119–136, 1936.Google Scholar
  4. 4.
    Gordeev, L., E. H. Haeusler, and V. G. da Costa, Proof compressions with circuit-structured substitutions, Journal of Mathematical Sciences 158(5): 645–658, 2009.CrossRefGoogle Scholar
  5. 5.
    Gordeev, L., E. H. Haeusler, and L. C. Pereira, Propositional proof compressions and dnf logic, Logic Journal of the IGPL 19(1): 62–86, 2011.CrossRefGoogle Scholar
  6. 6.
    Prawitz, D., Natural deduction: a proof-theoretical study, Almqvist & Wiksell, 1965.Google Scholar
  7. 7.
    Quispe-Cruz, M., E. H. Haeusler, and L. Gordeev, Proof-graphs for minimal implicational logic, in M. Ayala-Rincón, E. Bonelli, and I. Mackie, (eds.), Proceedings 9th International Workshop on Developments in Computational Models, Buenos Aires, Argentina, 26 August 2013, vol. 144 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2014, pp. 16–29.Google Scholar
  8. 8.
    Savitch, W. J., Relationships between nondeterministic and deterministic tape complexities, J. Comput. Syst. Sci. 4(2): 177–192, 1970.CrossRefGoogle Scholar
  9. 9.
    Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoretical Computer Science 9(1): 67–72, 1979.CrossRefGoogle Scholar
  10. 10.
    Svejdar, V., On the polynomial-space completeness of intuitionistic propositional logic Arch. Math. Log. 42(7): 711–716, 2003.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V., part of Springer Nature 2017

Authors and Affiliations

  1. 1.Wilhelm-Schickard-InstitutUniversität TübingenTübingenGermany
  2. 2.Depto de InformáticaPUC-RioRio de JaneiroBrazil

Personalised recommendations