On meta complexity of propositional formulas and propositional proofs
type: Item
instance of: scholarly article
title: On meta complexity of propositional formulas and propositional proofs
zbMATH Open document ID: 1148.03037
author: Pavel Naumov
published in: Archive for Mathematical Logic
publication date: 2008-08-20T00:00:00Z
review text: Proof complexity is usually measured by the number of the symbols used in the proof, or by the number of proof steps. Likewise the size of a formula is taken to be the number of its symbols. The analysis of the minimal proof size as a function of the tautology size is the core of propositional proof complexity. In the paper under review, the author defines Boolean recursions which enable him to bring about the expressions like \(\bigvee_{i=1}^{n}p_i\) and \(\bigwedge_{i=1}^{n}p_i\), thus expanding the language of propositional logic. Then he takes the minimal size of the \textbf{PA}-proof of the statement Taut\((\overline{\varphi})\) as the meta proof complexity of the propositional formula \(\varphi\), where Taut\((x)\) is an arithmetical formula stating that \(x\) is the Gödel number of a propositional tautology, and \(\overline{\varphi}\) is the Gödel number of \(\varphi\). The main result of the paper is that for any function \(f\) that is polynomially dominated by the exponentiation function, there exists a propositional tautology \(\varphi\) -- defined by a system of Boolean recursions -- whose meta complexity proof is greater than \(f(\overline{\varphi})\). Thus we have a super-polynomial lower bound on the meta proof complexity of Boolean recursive propositional formulas. The proof of the above theorem uses a beautiful Boolean encoding of arithmetical proofs, which is a novel and smart idea first introduced in the present paper.
reviewed by: Saeed Salehi
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 5314399
zbMATH Keywords: proof complexity
zbMATH Keywords: propositional systems
zbMATH Keywords: Boolean recursions
MaRDI profile type: Publication
full work available at URL: s00153-008-0068-4
OpenAlex ID: W2045675862
cites work: The relative efficiency of propositional proof systems
cites work: On the complexity of cutting-plane proofs
cites work: The intractability of resolution
cites work: Diagonalization in proof complexity
cites work: Implicit proofs
cites work: Q5718678
cites work: An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
cites work: Some Results on the Length of Proofs
cites work: Exponential lower bounds for the pigeonhole principle
DOI: 10.1007/S00153-008-0068-4
Recommended article: Q5457670
Recommended article: Q5457669
Recommended article: Q5593816
Recommended article: The Complexity of Propositional Proofs
Recommended article: Q4790400
Recommended article: Q4390867
Recommended article: Q4934563
Recommended article: Q4723713
Recommended article: Q3724328
description: scientific article; zbMATH DE number 5314399