On the computational content of intuitionistic propositional proofs (Q5940143)

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.