Proof complexity of substructural logics

0549748 - MÚ 2022 NL eng J - Journal Article
Jalali Keshavarz, Raheleh
Proof complexity of substructural logics.
Annals of Pure and Applied Logic. Roč. 172, č. 7 (2021), č. článku 102972. ISSN 0168-0072. E-ISSN 1873-2461
R&D Projects: GA ČR(CZ) GA19-05497S
Institutional support: RVO:67985840
Keywords : proof complexity * subintuitionistic logics * substructural logics
OECD category: Pure mathematics
Impact factor: 0.776, year: 2021
Method of publishing: Limited access
https://doi.org/10.1016/j.apal.2021.102972

In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system P at least as strong as Full Lambek calculus, FL, and polynomially simulated by the extended Frege system for some superintuitionistic logic of infinite branching, we present an exponential lower bound on the proof lengths. More precisely, we will provide a sequence of P-provable formulas {An}n=1∞ such that the length of the shortest P-proof for An is exponential in the length of An. The lower bound also extends to the number of proof lines (proof lengths) in any Frege system (extended Frege system) for a logic between FL and any superintuitionistic logic of infinite branching. As an example, Hilbert-style proof systems for any finitely axiomatizable extension of FL that are weaker than the intuitionistic logic, in particular the usual Hilbert-style proof systems for the logics FLS for the set of structural rules S⊆{e,i,o,c}, fall in this category. We will also prove a similar result for the proof systems and logics extending Visser's basic propositional calculus BPC and its logic BPC, respectively. Finally, in the classical substructural setting, we will establish an exponential lower bound on the number of proof lines in any proof system polynomially simulated by the cut-free version of CFLew.
Permanent Link: http://hdl.handle.net/11104/0325667