15
$\begingroup$

A recent blog post by Lance Fortnow discusses non-constructive proofs, where "non-constructive" here means that the law of the excluded middle is used in a substantive way. That is, one takes some proposition $P$ whose truth is unknown, and splits the proof into two cases: (1) $P$ is true, and (2) $P$ is false. In both cases we deduce the desired theorem, but by totally different arguments. Fortnow gives an example from complexity theory:

In complexity, a well-known non-constructive theorem is by Kannan, showing that $\Sigma_2^P$ does not have $n^2$-size circuits.

  1. SAT doesn't have $n^2$-size circuits. Since SAT is in $\Sigma_2$, we are done.
  2. SAT has $n^2$-size circuits. Then by Karp–Lipton, $\Sigma_4 = \Sigma_2$ so L is in $\Sigma_2$ and we are done.

My question is, are there other proofs of results in complexity theory that are non-constructive in this sense?

Sometime in the past five years, I remember seeing such a paper, but unfortunately I can't remember anything else about it. I think it was a paper that had been recently published (though there's a chance it was an older paper that I had only just learned about). I also think the topic was circuit lower bounds, though I'm even less sure about that. Anyway, I'm interested in any examples, not just the one that I'm struggling to recall.

$\endgroup$
7
  • 4
    $\begingroup$ What about results that use the existence of a finite obstruction set for minor-closed families? (Many algorithms parametrized by genus, for example, use this.) It's a bit more indirect than the example from Kannan's Thm, but I think still nonconstructive... $\endgroup$ Commented Sep 11, 2023 at 20:12
  • 1
    $\begingroup$ @JoshuaGrochow Yes, that counts. I was thinking more of lower bounds than upper bounds, but I didn't say so explicitly in my question, so that sort of thing is fair game. $\endgroup$ Commented Sep 11, 2023 at 20:31
  • 3
    $\begingroup$ This has nothing to do with the question, it's just for the sake of clarity: the quoted proof from Fortnow's article is a bit puzzling because it mentions an undefined problem $\mathsf{L}$, which is not defined in the rest of the blog article either. Someone on the blog commented that $\mathsf{L}$ is a problem having no $n^2$-size circuits by diagonalization and which may be shown to be in $\Sigma_4$, as mentioned in this older blog article, from which that snippet was copied-and-pasted. $\endgroup$ Commented Sep 12, 2023 at 14:58
  • 1
    $\begingroup$ @DamianoMazza Thank you! I was just about to ask 'What is L?" $\endgroup$
    – Vincent
    Commented Sep 12, 2023 at 15:33
  • 1
    $\begingroup$ The quoted statement of Kannan’s theorem is perfectly constructive if you reorder the proof to make it a straight proof of negation rather than a proof by cases: suppose that $\Sigma^P_2$ has $n^2$-size circuits. Then SAT has $n^2$-size circuits, hence $\Sigma^P_2=\Sigma^P_4$, hence “L” (cf. the comments above) has $n^2$-size circuits, which is a contradiction. Thus, $\Sigma^P_2$ does not have $n^2$-size circuits. $\endgroup$ Commented Mar 1 at 17:35

2 Answers 2

13
$\begingroup$

There are several other non-constructive arguments that work along similar Karp-Lipton-esque lines, such as Santhanam's proof (STOC 2009) that $PromiseMA$ is not in $SIZE(n^k)$ for some $k$, and Kabanets-Impagliazzo-Volkovich's proof (CCC 2018) that $ZPEXP^{MCSP}$ is not in $P/poly$.

For a slightly different kind of example (but still regarding types of circuit lower bounds), Rahul Santhanam and I proved (CCC 2013):

$P$ is not in $P$-uniform $SIZE(n^k)$ for every fixed $k$.

(Paper at: https://people.csail.mit.edu/rrw/WeakUniformity-journal-rev.pdf)

The proof is not constructive: it does not name any function in P that exhibits the lower bound. We don't even know a time upper bound on the hard $P$-function (otherwise, we could take some generic simulation language as the hard function).

I've tried off and on for some years to give a specific function satisfying the lower bound. The best I could do so far is with Cody Murray, where we showed that there is a function in time $n^2$ that isn't in $LOGSPACE$-uniform $SIZE(n^{1+o(1)})$. See https://drops.dagstuhl.de/opus/volltexte/2017/7542/

$\endgroup$
5
$\begingroup$

I finally managed to track down the paper that I was struggling to recall.

Why are Proof Complexity Lower Bounds Hard? by Ján Pich and Rahul Santhanam, FOCS 2019.

Their main result is:

Theorem 1. Rudich's Conjecture does not admit feasible propositional proofs.

By "Rudich's Conjecture" they mean the following:

Rudich's Conjecture: For any proof system R verifiable in polynomial size, most Boolean functions on $n$ bits do not have short (i.e., poly(2n)) size R-proofs of hardness.

For our present purposes, the key point is that their proof of Theorem 1 splits into two cases, depending on whether Rudich's Conjecture is true or false.

If Rudich's Conjecture is false, we show using standard techniques (together with an amplification argument) that there is a propositional proof system R with polynomial advice in which most circuit lower bound tautologies for functions on n inputs have short proofs, for infinitely many n. In this case, the R-proof lower bound formulas aren't tautologies, with high probability, and hence they cannot have polynomial-size S-proofs (or indeed proofs of any size) for any sound propositional proof system S.

The crux of our proof is the argument that when Rudich's Conjecture is true, then Rudich's Conjecture does not admit feasible proofs. Thus Rudich's Conjecture is self-defeating in the propositional setting: its truth implies its unprovability.

$\endgroup$
1
  • $\begingroup$ But Theorem 1 as quoted is a negative statement, so proceeding by cases on the truth of Rudich's conjecture is constructively admissible. It seems like the content of case 1 is more likely to be a problem, although perhaps it could be fixed. $\endgroup$
    – Dan Doel
    Commented Mar 1 at 19:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.