×

zbMATH — the first resource for mathematics

On the computational content of intuitionistic propositional proofs. (English) Zbl 1009.03027
In this paper the complexity of the disjunction property of intuitionistic propositional logic is investigated. The proof of cut elimination for intuitionistic propositional and first-order logic is repeated. Let \(\text{ Cl}(P)\) for proofs \(P\) be the smallest set containing the sequents in \(P\) and closed under cut rule, weakening and, in case of first-order logic, term substitution. With this definition it is shown that for the cut-free proof \(P'\) obtained by the cut-elimination theorem from a proof \(P\) we have \(\text{ Cl}(P') \subseteq \text{ Cl}(P)\). Then the authors show that there exists an oracle machine which for every proof \(P\) of a sequent \(\Gamma B_0 \lor B_1\), with \(\Gamma\) consisting only of atomic formulas and implications, computes in polynomial time an \(i\) s.t. \(\Gamma\rightarrow B_i \in \text{ Cl}(P)\) or a sequent \(C \supset D\) in \(\rightarrow \Gamma\) s.t. \(\Gamma\rightarrow C \in \text{ Cl}(P)\). The oracle makes a decision only in case a disjunction \(C \lor D\) occurs in a sequent occurring while carrying out the search procedure, and all such sequents are in a set \(\text{ Cl}^+(P)\).
It follows that the disjunction property with Harrop formulas is polynomial-time computable: there exists a polynomial-time algorithm which for given intuitionistic proofs \(P\) of a sequent \(A_1 ,\ldots, A_n \rightarrow B_1 \lor B_m\), where \(A_i\) are Harrop formulas, computes an \(i\) and a proof \(P'\) of \(A_1 ,\ldots, A_n \rightarrow B_i\).
The authors then show that if \(\text{NP} \cap \text{coNP} \not \subseteq \text{P/poly}\), then the lengths of shortest proofs in the intuitionistic propositional calculus cannot be bounded by a polynomial in the size of the proved formula. Further they show that if factoring is not computable in polynomial time, then there is more than polynomial speedup between the classical and propositional calculus.
Next, the authors show that the disjunction property mentioned before is P-hard. This is shown by defining for every Boolean circuit \(\mathcal C(x_1 ,\ldots, x_n)\) in logarithmic space formulas \(B_0\) and \(B_1\), depending on variables \(x_i\) and possibly some other variables \(u_i\), and an intuitionistic proof \(P\) of \(x_1 \lor \neg x_1 ,\ldots, x_n \lor \neg x_n \rightarrow B_0 \lor B_1\), s.t. \(\mathcal C(a_1 ,\ldots, a_n) = i\) iff \(B_i(a_1 ,\ldots, a_n,\vec{u})\) is an intuitionistic tautology.
The article is well written and easy to read.

MSC:
03F20 Complexity of proofs
03F05 Cut-elimination and normal-form theorems
03F07 Structure of proofs
03D15 Complexity of computation (including implicit computational complexity)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
03D10 Turing machines and related notions
03B20 Subsystems of classical logic (including intuitionistic logic)
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] M.L. Bonet, T. Pitassi, R. Raz, No feasible interpolation for TC0-Frege proofs, in: Proceedings of the 38th Annual Symposium on Foundations of Computer Science, Piscataway, NJ, IEEE Computer Society Press, Silver Spring, MD, pp. 254-263.
[2] Buss, S.R, An introduction to proof theory, (), 1-78 · Zbl 0912.03024
[3] Buss, S.R; Mints, G, The complexity of the disjunction and existence properties in intuitionistic logic, Ann. pure appl. logic, 99, 93-104, (1999) · Zbl 0939.03064
[4] A. Goerdt, Efficient interpolation for the intuitionistic sequent calculus, Technische Universität Chemnitz, CSR-00-02, January 2000, preprint.
[5] Krajı́ček, J, Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic, J. symbolic logic, 62, 457-486, (1997) · Zbl 0891.03029
[6] Mundici, D, Tautologies with a unique Craig interpolant, Ann. pure appl. logic, 27, 265-273, (1984) · Zbl 0594.03022
[7] Pudlák, P, Lower bounds for resolution and cutting plane proofs and monotone computations, J. symbolic logic, 62, 981-998, (1997) · Zbl 0945.03086
[8] Pudlák, P, (), 197-218
[9] Pudlák, P; Sgall, J, Algebraic models of computation and interpolation for algebraic systems, DIMACS ser. discrete math. theor. comp. sci., 39, 279-295, (1998) · Zbl 0901.03033
[10] Schöning, U, Logik fük informatiker, (1989), Wissenschaftsverlag Mannheim
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.