Proof complexity of intuitionistic implicational formulas

DOI10.1016/J.APAL.2016.09.003MaRDI QIDQ331054zbMATH OpenOpenAlexFDO

Authors Emil Jeřábek

Publication date 26 October 2016

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

Full work available at URL https://arxiv.org/abs/1512.05667

zbMATH Keywords

intuitionistic logicproof complexityimplicational fragment

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Intermediate logics (03B55) Complexity of proofs (03F20)

Abstract: We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubev{s} cite{hru:lbint}, generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jev{r}'abek cite{ej:sfef}, can be realized by implicational tautologies.

Recommendations

• A lower bound for intuitionistic logic
• Complexity of intuitionistic propositional logic and its fragments
• On the computational content of intuitionistic propositional proofs
• On lengths of proofs in non-classical logics
• Proof complexity of substructural logics

Cites work

• scientific article; zbMATH DE number 1003731 (Why is no real title available?)
• scientific article; zbMATH DE number 3737629 (Why is no real title available?)
• scientific article; zbMATH DE number 3751028 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• scientific article; zbMATH DE number 2187723 (Why is no real title available?)
• A lower bound for intuitionistic logic
• Admissible rules in the implication-negation fragment of intuitionistic logic
• Algebraizable logics
• Frege systems for extensible modal logics
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for modal logics
• On lengths of proofs in non-classical logics
• On the computational content of intuitionistic propositional proofs
• Positive formulas in intuitionistic and minimal logic
• Substitution Frege and extended Frege proof systems in non-classical logics
• The complexity of the disjunction and existential properties in intuitionistic logic
• The separation theorem of intuitionist propositional calculus

Cited in

(15)

• A simplified lower bound for implicational logic
• Complexity of subclasses of the intuitionistic propositional calculus
• A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝] Frege systems
• Intuitionistic implication makes model checking hard
• Admissibility in positive logics
• Studying provability in implicational intuitionistic logic: the formula tree approach
• Exploring Computational Contents of Intuitionist Proofs
• On the proof complexity of logics of bounded branching
• Proof finding algorithms for implicational logics
• Computer Science Logic
• An algorithm for the class of pure implicational formulas
• Implicit proofs
• Essential structure of proofs as a measure of complexity
• On the unprovability of circuit size bounds in intuitionistic \(\mathsf{S}^1_2\)
• Inductive Complexity of Goodstein’s Theorem

This page was built for publication: Proof complexity of intuitionistic implicational formulas

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