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.
- SAT doesn't have $n^2$-size circuits. Since SAT is in $\Sigma_2$, we are done.
- 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.