Substitution Frege and extended Frege proof systems in non-classical logics

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

Abstract

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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,774

External links

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

Through your library

Analytics

Added to PP
2013-12-22

Downloads
36 (#119,765)

6 months
14 (#987,135)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Rules with parameters in modal logic I.Emil Jeřábek - 2015 - Annals of Pure and Applied Logic 166 (9):881-933.
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.
Rules with parameters in modal logic II.Emil Jeřábek - 2020 - Annals of Pure and Applied Logic 171 (10):102829.
Expander construction in VNC1.Sam Buss, Valentine Kabanets, Antonina Kolokolova & Michal Koucký - 2020 - Annals of Pure and Applied Logic 171 (7):102796.

View all 8 citations / Add more citations

References found in this work

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