Proof complexity of substructural logics

Subsystems of classical logic (including intuitionistic logic) (03B20) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Complexity of proofs (03F20) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Abstract: In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system

m a t h b f P

at least as strong as Full Lambek calculus,

m a t h b f F L

, and polynomially simulated by the extended Frege system for some infinite branching super-intuitionistic logic, we present an exponential lower bound on the proof lengths. More precisely, we will provide a sequence of

m a t h b f P

-provable formulas

{A_{n}}_{n = 1}^{i n f t y}

such that the length of the shortest

m a t h b f P

-proof for

A_{n}

is exponential in the length of

A_{n}

. The lower bound also extends to the number of proof-lines (proof-lengths) in any Frege system (extended Frege system) for a logic between

m a t h s f F L

and any infinite branching super-intuitionistic logic. We will also prove a similar result for the proof systems and logics extending Visser's basic propositional calculus

m a t h b f B P C

and its logic

m a t h s f B P C

, 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

m a t h b f C F L_{e w}

.

Review text

The article is well written and organized, no typos where found. Three results are proved; the first one, is an exponential lower bound on the length of the proof of a sequence of hard \textbf{P}-tautologies \((\mathrm{Clique}_{n,k}\), and \(\mathrm{Color}_{n,m})\), namely a sequence of \textbf{P}-provable formulas \(\{A_n\}^\infty_{n=1}\), that is, the length of the shortest \textbf{P}-proof for \(A_n\) is exponential in \(|A_n|\), where \textbf{P} is a proof system as strong as full Lambek calculus (\textbf{FL}), and it is polynomially simulated by \textbf{eF} (extended Frege) for some superintuitionistic logic of \(\infty\)-branching, denoted by L-\textbf{EF}. The second result is a similar proof of the previous one but for a proof system and logic extending Visser's basic propositional calculus (\textbf{BPC}). And the third result is in the classical setting, again, an exponential lower bound on the number of proof line of any proof system polynomially simulated by \textbf{CLF}\(^{-}_{ew}\).

Recommendations

Cites work

Cited in

(16)

This page was built for publication: Proof complexity of substructural logics

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