Models of lower-bounds proofs (Q1107322)

Two models of widely applicable lower bound proofs are introduced. They allow to associate a set \({\mathcal F}\) of Boolean functions with every such a proof. The complexity of functions from \({\mathcal F}\) is suggested as a criterion distinguishing ``effective lower bounds'' from ``noneffective'' ones. It is shown that proofs with \({\mathcal F}\) containing functions of n variables with the size complexity at most s(n) cannot produce a lower bound exceeding \(O(s(n)\cdot (n+s(n)\cdot \log s(n)))\). In all known lower bound proofs it is \(s(n)=O(n)\).