On lengths of proofs in non-classical logics

Annals of Pure and Applied Logic 157 (2-3):194-205 (2009)
  Copy   BIBTEX

Abstract

We give proofs of the effective monotone interpolation property for the system of modal logic K, and others, and the system IL of intuitionistic propositional logic. Hence we obtain exponential lower bounds on the number of proof-lines in those systems. The main results have been given in [P. Hrubeš, Lower bounds for modal logics, Journal of Symbolic Logic 72 941–958; P. Hrubeš, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 72–90]; here, we give considerably simplified proofs, as well as some generalisations

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2008.09.013

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,174

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A lower bound for intuitionistic logic.Pavel Hrubeš - 2007 - Annals of Pure and Applied Logic 146 (1):72-90.
Substitution Frege and extended Frege proof systems in non-classical logics.Emil Jeřábek - 2009 - Annals of Pure and Applied Logic 159 (1-2):1-48.
Lower Bounds for Modal Logics.Pavel Hrubeš - 2007 - Journal of Symbolic Logic 72 (3):941 - 958.
The complexity of the disjunction and existential properties in intuitionistic logic.Sam Buss & Grigori Mints - 1999 - Annals of Pure and Applied Logic 99 (1-3):93-104.
Frege systems for extensible modal logics.Emil Jeřábek - 2006 - Annals of Pure and Applied Logic 142 (1):366-379.
On the computational content of intuitionistic propositional proofs.Samuel R. Buss & Pavel Pudlák - 2001 - Annals of Pure and Applied Logic 109 (1-2):49-64.
The canonical pairs of bounded depth Frege systems.Pavel Pudlák - 2021 - Annals of Pure and Applied Logic 172 (2):102892.
Hypersequent calculi for intuitionistic logic with classical atoms.Hidenori Kurokawa - 2010 - Annals of Pure and Applied Logic 161 (3):427-446.
Feasibly constructive proofs of succinct weak circuit lower bounds.Moritz Müller & Ján Pich - 2020 - Annals of Pure and Applied Logic 171 (2):102735.
Provability logics with quantifiers on proofs.Rostislav E. Yavorsky - 2001 - Annals of Pure and Applied Logic 113 (1-3):373-387.

Analytics

Added to PP
2013-12-22

Downloads
30 (#753,100)

6 months
5 (#1,047,105)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Proof complexity of intuitionistic implicational formulas.Emil Jeřábek - 2017 - Annals of Pure and Applied Logic 168 (1):150-190.
Proof complexity of substructural logics.Raheleh Jalali - 2021 - Annals of Pure and Applied Logic 172 (7):102972.
On the proof complexity of logics of bounded branching.Emil Jeřábek - 2023 - Annals of Pure and Applied Logic 174 (1):103181.
Towards NP – P via proof complexity and search.Samuel R. Buss - 2012 - Annals of Pure and Applied Logic 163 (7):906-917.

View all 7 citations / Add more citations

References found in this work

A lower bound for intuitionistic logic.Pavel Hrubeš - 2007 - Annals of Pure and Applied Logic 146 (1):72-90.
Frege systems for extensible modal logics.Emil Jeřábek - 2006 - Annals of Pure and Applied Logic 142 (1):366-379.

View all 8 references / Add more references