On meta complexity of propositional formulas and propositional proofs (Q937212)

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.