On the computational content of intuitionistic propositional proofs. (English) Zbl 1009.03027

Buss, Samuel R.; Pudlák, Pavel

Ann. Pure Appl. Logic 109, No. 1-2, 49-64 (2001).

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.

Reviewer: Anton Setzer (Swansea)

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

Keywords:

cut-elimination; intuitionistic logic; propositional proof systems; polynomial time; disjunction property; Craig interpolation; realizability; circuit complexity; feasible algorithms

References:

[1]	M.L. Bonet, T. Pitassi, R. Raz, No feasible interpolation for \(TC^0\); M.L. Bonet, T. Pitassi, R. Raz, No feasible interpolation for \(TC^0\)
[2]	Buss, S. R., An introduction to proof theory, (Buss, S. R., Handbook of Proof Theory (1998), North-Holland: North-Holland Amsterdam), 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.; 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., (On the complexity of propositional calculus, Sets and proofs, in Logic Colloquium ’97 (1999), Cambridge University Press: Cambridge University Press Cambridge), 197-218 · Zbl 0939.03065
[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: Wissenschaftsverlag Mannheim · Zbl 0677.03001