The complexity of the disjunction and existential properties in intuitionistic logic.

*(English)*Zbl 0939.03064As 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.

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.

Reviewer: M.Yasuhara (Princeton)

##### MSC:

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.) |

##### Keywords:

complexity; disjunction property; existential property; intuitionistic logic; fragment of arithmetic
PDF
BibTeX
XML
Cite

\textit{S. Buss} and \textit{G. Mints}, Ann. Pure Appl. Logic 99, No. 1--3, 93--104 (1999; Zbl 0939.03064)

Full Text:
DOI

**OpenURL**

##### References:

[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.