In the spirit of a previous posting of his to the Foundations of Mathematics list that I quoted before in this blog, Timothy Chow has posted a nice observation, this time indicating how the truth of some widely believed statements about computational classes could actually lead to their unprovability in certain formal systems, via the identification of fast growing functions. I quote his message below:
Recall that
is the non-uniform analogue of
: It is the class of Boolean functions computable by polynomial-size Boolean circuits. It is widely believed that
is not contained in
.
Conjecture
is a somewhat stronger conjecture than
, but weaker than the conjecture that the polynomial hierarchy does not collapse.
Suppose that
is indeed true, but only “barely true,” i.e., there exists some function
that is just barely superpolynomial, such that there exist Boolean circuits of size
that correctly solve an
-complete problem. Then the promised “simple observation” is that
is then unprovable.
To see this, fix some way of encoding
instances. Let
be the smallest integer
such that no Boolean circuit with
inputs and
gates correctly solves every instance of
(of the appropriate size). If there is no such
then
is undefined. Then
asserts that
is total.
The point is that if
is barely true, then
grows very fast. As Andreas puts it,
because the left side is enough gates to solve
-sized instances of
while the right side isn’t. Then for
(and therefore also for
not of this form with just a minor change in the estimates)
. Now if
is just barely superpolynomial, then the exponent here,
, must be just barely above constant, and so
grows very fast. If it grows fast enough then your favorite formal system won’t be able to prove that it is total.
Tim
It turns out that Chow’s observation had been done before, in “On the independence of
versus
,” by Ben-David and Halevi, a technical report from 1991 available here as of this writing.
Let
denote
,
augmented with all true
statements. In their report, Ben-David and Halevi prove:
Theorem.
if and only if there some
such that the function
of the Wainer hierarchy dominates the approximation rate of
to
.
Here, the approximation rate
is defined by fixing a (canonical) enumeration of the class
, say
, and setting
. This function only depends superficially on the specific enumeration being considered, and it is a total function under the assumption that
is not in
.
Scott Aaronson has a survey on the question of logical independence of “
,” Is
Versus
Formally Independent?, Bulletin of the EATCS 81, October 2003, as of this writing available at his website. Aaronson’s survey is not really aimed at logicians, but it is self contained and nicely written.