Annals of Pure and Applied Logic 159 (1-2):1-48 (2009)

We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual system for classical logic with respect to a naturally defined translation.On the other hand, we establish exponential speed-up of over for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2008.10.005
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 54,536
Through your library

References found in this work BETA

Dual Weak Pigeonhole Principle, Boolean Complexity, and Derandomization.Emil Jeřábek - 2004 - Annals of Pure and Applied Logic 129 (1-3):1-37.
A Lower Bound for Intuitionistic Logic.Pavel Hrubeš - 2007 - Annals of Pure and Applied Logic 146 (1):72-90.

View all 9 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.
Rules with Parameters in Modal Logic I.Emil Jeřábek - 2015 - Annals of Pure and Applied Logic 166 (9):881-933.
Topological Differential Fields and Dimension Functions.Nicolas Guzy & Françoise Point - 2012 - Journal of Symbolic Logic 77 (4):1147-1164.

Add more citations

Similar books and articles

Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
Quantum Deduction Rules.Pavel Pudlák - 2009 - Annals of Pure and Applied Logic 157 (1):16-29.
Frege on Indirect Proof.Ivan Welty - 2011 - History and Philosophy of Logic 32 (3):283-290.
Frege Systems for Extensible Modal Logics.Emil Jeřábek - 2006 - Annals of Pure and Applied Logic 142 (1):366-379.
Frege's Proof of Referentiality.Øystein Linnebo - 2004 - Notre Dame Journal of Formal Logic 45 (2):73-98.
What Frege's Theory of Identity is Not.Robert May - 2012 - Thought: A Journal of Philosophy 1 (1):41-48.


Added to PP index

Total views
21 ( #481,686 of 2,385,584 )

Recent downloads (6 months)
1 ( #560,835 of 2,385,584 )

How can I increase my downloads?


My notes