Substitution Frege and extended Frege proof systems in non-classical logics
type: Item
instance of: scholarly article
title: Substitution Frege and extended Frege proof systems in non-classical logics
zbMATH Open document ID: 1173.03044
author: Emil Jeřábek
published in: Annals of Pure and Applied Logic
publication date: 2009-06-10T00:00:00Z
review text: Substitution Frege (SF) proof systems have the substitution rule \(\phi\vdash \phi[p_1/\phi_1,\ldots,p_n/\phi_n]\) in addition to axiom schemata and the rule of modus ponens. Extended Frege (EF) systems have extension axioms \(q\Leftrightarrow \psi\) for a fresh propositional letter \(q\) instead of the substitution rule. It was known that SF and EF are polynomially equivalent for the classical propositional logic. The author proves the same result for all extensions of KB, all tabular logics, all logics of finite depth and width, in most cases by a polynomial intertranslation with the classical logic. For all modal and superintuitionistic logics of infinite branching a polynomial speed-up of SF over EF is established, extending recent result by P. Hrubeš.
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B55
zbMATH DE Number: 5563891
zbMATH Keywords: propositional proof complexity
zbMATH Keywords: Frege system
zbMATH Keywords: modal logic
zbMATH Keywords: intermediate logic
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: j.apal.2008.10.005
OpenAlex ID: W2155797483
cites work: The monotone circuit complexity of Boolean functions
cites work: Monotone simulations of non-monotone proofs.
cites work: Modal logic
cites work: Polynomial size proofs of the propositional pigeonhole principle
cites work: The complexity of the disjunction and existential properties in intuitionistic logic
cites work: On the computational content of intuitionistic propositional proofs
cites work: Q3128959
cites work: The relative efficiency of propositional proof systems
cites work: On the complexity of the disjunction property in intuitionistic and modal logics
cites work: Lower bounds for modal logics
cites work: A lower bound for intuitionistic logic
cites work: Dual weak pigeonhole principle, Boolean complexity, and derandomization
cites work: Admissible Rules of Modal Logics
cites work: Frege systems for extensible modal logics
cites work: Q4856172
cites work: Q5460922
cites work: Q4068699
cites work: Canonical formulas for K4. Part II: Cofinal subframe logics
DOI: 10.1016/J.APAL.2008.10.005
description: scientific article; zbMATH DE number 5563891