Quantified propositional logic and the number of lines of tree-like proofs
type: Item
instance of: scholarly article
title: Quantified propositional logic and the number of lines of tree-like proofs
zbMATH Open document ID: 0956.03049
DOI: 10.1023/A:1005281425560
author: Alessandra Carbone
published in: Studia Logica
publication date: 2001-03-07T00:00:00Z
review text: Rules for quantifiers over propositions are added to the sequent calculus for propositional logic. The rules are formulated in the obvious way and they are similar to the usual rules for first-order quantification. In contrast, Substitution Frege systems are formulated in the sequent calculus for propositional logic as well; however, instead of the quantifier rules they feature a rule that allows for uniform substitution of propositional parameters by arbitrary propositional formulas. The introduction of the propositional quantifiers induces an exponential speed-up of proofs of propositional tautologies (with respect to the number of lines in a proof) over Substitution Frege systems.
reviewed by: Volker Halbach
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B05
zbMATH DE Number: 1501384
zbMATH Keywords: quantified propositional logic
zbMATH Keywords: tree-like proofs
zbMATH Keywords: polynomial simulation
zbMATH Keywords: speed-up
zbMATH Keywords: number of lines in proofs
zbMATH Keywords: sequent calculus
zbMATH Keywords: substitution Frege systems
MaRDI profile type: Publication
full work available at URL: a:1005281425560
OpenAlex ID: W1497902529
description: scientific article; zbMATH DE number 1501384