I wished to know if the proof attempts at separation of complexity classes via the methods outlined by Descriptive Complexity theorists naturalise?
By naturalise I'm talking about the Idea of Natural Proofs set forth by Razborov and Rudich to set in stone the futility of many of the current approaches to prove lower bounds for boolean circuits.
If one reads up Kolaitis, Vardi, Libkin et al's book on Finite Model Theory and its applications there are intriguing statements like TFAE :
NP $\not=$ coNP
For every $s_1$,$\ldots$, $s_k$, $r$, there are finite graphs G and H such that
- G is not 3-Colourable and H is 3-Colourable
- the Duplicator wins the (⟨$s_1$,$\ldots$,$s_k$⟩,$r$) EF game on G and H.
This is after setting up the logic characterising the class NP and then coming up with the inexpressibility techniques of the EF games.
Problem becomes that this reduces to another hard combinatorial problem, and I was wondering if there is any follow up work that either shows why work along these lines is hard, like say if it could be showed that solving this problem was a natural proof. Then it would be clear to theorists to abandon that line of attack.