<p>I finally managed to track down the paper that I was struggling to recall.</p>
<p><a href="https://doi.org/10.1109/FOCS.2019.00080" rel="noreferrer">Why are Proof Complexity Lower Bounds Hard?</a> by Ján Pich and Rahul Santhanam, FOCS 2019.</p>
<p>Their main result is:</p>
<blockquote>
<p><b>Theorem 1.</b> Rudich's Conjecture does not admit feasible propositional proofs.</p>
</blockquote>
<p>By &quot;Rudich's Conjecture&quot; they mean the following:</p>
<blockquote>
<p><b>Rudich's Conjecture:</b> For any proof system <i>R</i> verifiable in polynomial size, most Boolean functions on <span class="math-container">$n$</span> bits do not have short (i.e., poly(2<sup><i>n</i></sup>)) size <i>R</i>-proofs of hardness.</p>
</blockquote>
<p>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.</p>
<blockquote>
<p>If Rudich's Conjecture is false, we show using standard techniques (together with an amplification argument) that there is a propositional proof system <i>R</i> with polynomial advice in which most circuit lower bound tautologies for functions on <i>n</i> inputs have short proofs, for infinitely many <i>n</i>. In this case, the <i>R</i>-proof lower bound formulas aren't tautologies, with high probability, and hence they cannot have polynomial-size <i>S</i>-proofs (or indeed proofs of any size) for any sound propositional proof system <i>S</i>.<br><br>
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 <i>self-defeating</i> in the  propositional setting: its truth implies its unprovability.</p>
</blockquote>

CC BY-SA 4.0
2024-03-01T19:42:28.037Z
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.
Dan Doel
CC BY-SA 4.0
2024-03-01T17:02:03.480Z
2024-03-01T17:02:03.480Z
Timothy Chow
<p>There are several other non-constructive arguments that work along similar Karp-Lipton-esque lines, such as Santhanam's proof (STOC 2009) that <span class="math-container">$PromiseMA$</span> is not in <span class="math-container">$SIZE(n^k)$</span> for some <span class="math-container">$k$</span>, and Kabanets-Impagliazzo-Volkovich's proof (CCC 2018) that <span class="math-container">$ZPEXP^{MCSP}$</span> is not in <span class="math-container">$P/poly$</span>.</p>
<p>For a slightly different kind of example (but still regarding types of circuit lower bounds), Rahul Santhanam and I proved (CCC 2013):</p>
<p><span class="math-container">$P$</span> is not in <span class="math-container">$P$</span>-uniform <span class="math-container">$SIZE(n^k)$</span> for every fixed <span class="math-container">$k$</span>.</p>
<p>(Paper at: <a href="https://people.csail.mit.edu/rrw/WeakUniformity-journal-rev.pdf" rel="noreferrer">https://people.csail.mit.edu/rrw/WeakUniformity-journal-rev.pdf</a>)</p>
<p>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 <span class="math-container">$P$</span>-function (otherwise, we could take some generic simulation language as the hard function).</p>
<p>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 <span class="math-container">$n^2$</span> that isn't in <span class="math-container">$LOGSPACE$</span>-uniform <span class="math-container">$SIZE(n^{1+o(1)})$</span>. See <a href="https://drops.dagstuhl.de/opus/volltexte/2017/7542/" rel="noreferrer">https://drops.dagstuhl.de/opus/volltexte/2017/7542/</a></p>

CC BY-SA 4.0
2023-09-12T02:18:15.000Z
2023-09-12T02:18:15.000Z
Ryan Williams
<p>A recent <a href="https://blog.computationalcomplexity.org/2023/08/what-makes-constructive-proof.html" rel="noreferrer">blog post by Lance Fortnow</a> discusses non-constructive proofs, where &quot;non-constructive&quot; here means that the <a href="https://en.wikipedia.org/wiki/Law_of_excluded_middle" rel="noreferrer">law of the excluded middle</a> is used in a substantive way. That is, one takes some proposition <span class="math-container">$P$</span> whose truth is unknown, and splits the proof into two cases: (1) <span class="math-container">$P$</span> is true, and (2) <span class="math-container">$P$</span> is false. In both cases we deduce the desired theorem, but by totally different arguments.  Fortnow gives an example from complexity theory:</p>
<blockquote>
<p>In complexity, a well-known non-constructive theorem is by Kannan, showing that <span class="math-container">$\Sigma_2^P$</span> does not have <span class="math-container">$n^2$</span>-size circuits.</p>
<ol>
<li>SAT doesn't have <span class="math-container">$n^2$</span>-size circuits. Since SAT is in <span class="math-container">$\Sigma_2$</span>, we are done.</li>
<li>SAT has <span class="math-container">$n^2$</span>-size circuits. Then by Karp–Lipton, <span class="math-container">$\Sigma_4 = \Sigma_2$</span> so L is in <span class="math-container">$\Sigma_2$</span> and we are done.</li>
</ol>
</blockquote>
<p>My question is, are there other proofs of results in complexity theory that are non-constructive in this sense?</p>
<p>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.</p>

CC BY-SA 4.0
2023-09-11T20:12:30.607Z
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...
Joshua Grochow
CC BY-SA 4.0
2023-09-11T20:16:10.720Z
Related: https://cstheory.stackexchange.com/q/12162/129, https://cstheory.stackexchange.com/q/19980/129, https://cstheory.stackexchange.com/q/41651/129
Joshua Grochow
CC BY-SA 4.0
2023-09-11T20:31:36.137Z
@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.
Timothy Chow
CC BY-SA 4.0
2023-09-12T14:58:16.373Z
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](https://blog.computationalcomplexity.org/2014/08/sixteen-years-in-making.html), from which that snippet was copied-and-pasted.
Damiano Mazza
CC BY-SA 4.0
2023-09-12T15:33:34.947Z
@DamianoMazza Thank you! I was just about to ask 'What is L?"
Vincent
CC BY-SA 4.0
2024-03-01T17:35:19.880Z
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.
Emil Jeřábek
CC BY-SA 4.0
2024-03-01T17:38:26.580Z
Though, this does not work if the theorem is formulated as an existential statement: “there exists a language in $\Sigma^P_2$ that does not have circuits of size $n^2$”.
Emil Jeřábek
<cc.complexity-theory><lower-bounds><constructive-mathematics>
Law of the Excluded Middle in complexity theory
Timothy Chow
# Law of the Excluded Middle in complexity theory

(Asked by: username_0 on 2023-09-11)

A recent [blog post by Lance Fortnow](https://blog.computationalcomplexity.org/2023/08/what-makes-constructive-proof.html) discusses non-constructive proofs, where "non-constructive" here means that the [law of the excluded middle](https://en.wikipedia.org/wiki/Law_of_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.

**Tags:** cc.complexity-theory, lower-bounds, constructive-mathematics

> **Comments:**
> **username_1**: 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...  
> **username_1**: Related: https://cstheory.stackexchange.com/q/12162/129, https://cstheory.stackexchange.com/q/19980/129, https://cstheory.stackexchange.com/q/41651/129  
> **username_0**: @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.  
> **username_2**: 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](https://blog.computationalcomplexity.org/2014/08/sixteen-years-in-making.html), from which that snippet was copied-and-pasted.  
> **username_3**: @DamianoMazza Thank you! I was just about to ask 'What is L?"  
> **username_4**: 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.  
> **username_4**: Though, this does not work if the theorem is formulated as an existential statement: “there exists a language in $\Sigma^P_2$ that does not have circuits of size $n^2$”.  

---

## 2 answers

### Answer by username_6 on 2023-09-12. Score: 14 | Accepted answer

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/>


---

### Answer by username_0 on 2024-03-01. Score: 5

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

[Why are Proof Complexity Lower Bounds Hard?](https://doi.org/10.1109/FOCS.2019.00080) 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(2*n*)) 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.

> **Comments:**
> **username_5**: 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.  

---

