On the computational content of intuitionistic propositional proofs

DOI10.1016/S0168-0072(01)00040-9MaRDI QIDQ5940143zbMATH OpenOpenAlexFDO

Publication date 22 April 2003

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(01)00040-9

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

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Turing machines and related notions (03D10) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Review text

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.

Recommendations

Cites work

Cited in

(19)

This page was built for publication: On the computational content of intuitionistic propositional proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5940143)