NATURAL PROOFS

We introduce the notion of natural proof. We argue that the known proo fs of lower bounds on the complexity of explicit Boolean functions in nonmonotone models fall within our definition of natural. We show, bas ed on a hardness assumption, that natural proofs can not prove superpo lynomial lower bounds for general circuits. Without the hardness assum ption, we are able to show that they can not prove exponential lower b ounds (for general circuits) for the discrete logarithm problem. We sh ow that the weaker class of AC(0)-natural proofs which is sufficient t o prove the parity lower bounds of Furst, Saxe, and Sipser, Yao, and H astad is inherently incapable of proving the bounds of Razborov and Sm olensky. We give some formal evidence that natural proofs are indeed n atural by showing that every formal complexity measure, which can prov e superpolynomial lower bounds for a single function, can do so for al most all functions, which is one of the two requirements of a natural proof in our sense. (C) 1997 Academic Press.