zbMATH — the first resource for mathematics

The complexity of the disjunction and existential properties in intuitionistic logic. (English) Zbl 0939.03064
As immediate consequences of Gentzen’s Hauptsatz, one has disjunction and existential properties of intuitionistic logic. (They are: if \(\lvdash A\vee B\) then \(\lvdash A\) or \(\lvdash B\), and if \(\lvdash\exists x C(x)\) then \(\lvdash C(t)\) for some term \(t\), respectively.) However, to find which disjunct or which term is beyond recursive means. [The authors remind us to think of the halting problem.]
In this paper, the authors take up a somewhat different aspect: namely, given a proof of \(A\vee B\), or \(\exists x C(x)\), how efficiently…? The answer depends on the logic used. In propositional logic, polynomial time is enough to construct a proof of a disjunct. In predicate logic without function symbols, both properties can be shown in exponential times. But, with function symbols, super-exponential bounds are necessary. Optimality is shown by considering a fragment of arithmetic with a binary predicate for \(y= 2^x\) for the existential property, and for the disjunction property a Turing machine whose future states are hard to predict. This last construction is ingeneous, the reviewer thinks.

03F20 Complexity of proofs
03F55 Intuitionistic mathematics
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
Full Text: DOI
[1] Gentzen, G.; Gentzen, G.; Gentzen, G., Untersuchungen über das logische schliessen, (), 39, 68-131, (1934), English translation in · JFM 60.0846.01
[2] Gentzen, G., ()
[3] Ladner, R.E., The computational complexity of provability in systems of modal propositional logic, SIAM J. comput., 6, 467-480, (1977) · Zbl 0373.02025
[4] Orevkov, V.P.; Orevkov, V.P., Lower bounds for lengthening of proofs after cut-elimination, (), J. soviet mathematics, 20, 2337-2350, (1982), In Russian: English translation · Zbl 0492.03023
[5] Prawitz, D., Natural deduction: A proof-theoretical study, (1965), Almqvist & Wiksell Stockholm · Zbl 0173.00205
[6] Pudlák, P., The lengths of proofs, (), 547-637 · Zbl 0920.03056
[7] Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoretical computer science, 9, 67-72, (1979) · Zbl 0411.03049
[8] Statman, R., Lower bound on Herbrand’s theorem, (), 104-107 · Zbl 0411.03048
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.