The complexity of the disjunction and existential properties in intuitionistic logic

Annals of Pure and Applied Logic 99 (1-3):93-104 (1999)

This paper considers the computational complexity of the disjunction and existential properties of intuitionistic logic. We prove that the disjunction property holds feasibly for intuitionistic propositional logic; i.e., from a proof of A v B, a proof either of A or of B can be found in polynomial time. For intuitionistic predicate logic, we prove superexponential lower bounds for the disjunction property, namely, there is a superexponential lower bound on the time required, given a proof of A v B, to produce one of A and B which is true. In addition, there is superexponential lower bound on the size of terms which fulfill the existential property of intuitionistic predicate logic. There are superexponential upper bounds for these problems, so the lower bounds are essentially optimal
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/s0168-0072(99)00002-0
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 40,000
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Lengths of Proofs.[author unknown] - 2000 - Bulletin of Symbolic Logic 6 (4):473-475.

Add more references

Citations of this work BETA

A Lower Bound for Intuitionistic Logic.Pavel Hrubeš - 2007 - Annals of Pure and Applied Logic 146 (1):72-90.
Frege Systems for Extensible Modal Logics.Emil Jeřábek - 2006 - Annals of Pure and Applied Logic 142 (1):366-379.
On Lengths of Proofs in Non-Classical Logics.Pavel Hrubeš - 2009 - Annals of Pure and Applied Logic 157 (2-3):194-205.

View all 7 citations / Add more citations

Similar books and articles

Empirical Meaningfulness and Intuitionistic Logic.John Myhill - 1972 - Philosophy and Phenomenological Research 33 (2):186-191.
A New Solution to a Problem of Hosoi and Ono.Michael Zakharyaschev - 1994 - Notre Dame Journal of Formal Logic 35 (3):450-457.
On the Derivability of Instantiation Properties.Harvey Friedman - 1977 - Journal of Symbolic Logic 42 (4):506-514.
Towards Intuitionistic Dynamic Logic.J. W. Degen & J. M. Werner - 2006 - Logic and Logical Philosophy 15 (4):305-324.
Combining Possibilities and Negations.Greg Restall - 1997 - Studia Logica 59 (1):121-141.
Finite Sets and Natural Numbers in Intuitionistic TT.Daniel Dzierzgowski - 1996 - Notre Dame Journal of Formal Logic 37 (4):585-601.
On the Beth Properties of Some Intuitionistic Modal Logics.C. Luppi - 2002 - Archive for Mathematical Logic 41 (5):443-454.


Added to PP index

Total views
7 ( #829,993 of 2,236,156 )

Recent downloads (6 months)
1 ( #989,564 of 2,236,156 )

How can I increase my downloads?


My notes

Sign in to use this feature