On lengths of proofs in non-classical logics

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

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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2008.09.013
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 39,951
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

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.
Lower Bounds for Modal Logics.Pavel Hrubeš - 2007 - Journal of Symbolic Logic 72 (3):941 - 958.

View all 8 references / Add more references

Citations of this work BETA

Proof Complexity of Intuitionistic Implicational Formulas.Emil Jeřábek - 2017 - Annals of Pure and Applied Logic 168 (1):150-190.
Towards NP – P Via Proof Complexity and Search.Samuel R. Buss - 2012 - Annals of Pure and Applied Logic 163 (7):906-917.

Add more citations

Similar books and articles

Fragments of Bounded Arithmetic and the Lengths of Proofs.Pavel Pudl'ak - 2008 - Journal of Symbolic Logic 73 (4):1389-1406.
Proofs and Countermodels in Non-Classical Logics.Sara Negri - 2014 - Logica Universalis 8 (1):25-60.
Automatic Checking Properties of Non-Classical Logics.Pavel Schreiner - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):507-516.
A Universal Logic Approach to Adaptive Logics.Diderik Batens - 2007 - Logica Universalis 1 (1):221-242.
Operations on Proofs and Labels.Tatiana Yavorskaya & Natalia Rubtsova - 2007 - Journal of Applied Non-Classical Logics 17 (3):283-316.


Added to PP index

Total views
9 ( #724,630 of 2,235,842 )

Recent downloads (6 months)
1 ( #978,704 of 2,235,842 )

How can I increase my downloads?


My notes

Sign in to use this feature