0
$\begingroup$

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

and

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.

| cite | improve this question | |
$\endgroup$
  • 1
    $\begingroup$ I can’t say I understand the question. Any two equivalent formulations of a problem are, well, equivalent. One is as hard to solve as the other. Whether a suggested proof of the other formulation would lead to a natural proof in the sense of Razborov and Rudich depends entirely on the proof, it’s not a property of the formulation of the problem. $\endgroup$ – Emil Jeřábek Nov 26 '19 at 8:06
  • $\begingroup$ Hi, @EmilJeřábeksupportsMonica, so my problem is, as far as I understand; The statement made above makes us approach the separation of NP and coNP via an EF game proof method. Which from the FO examples, I feel would follow a similar pattern of conclusion via a contradiction, the inexpressibility of the logic, in our case above 3-colourability not being expressed via a $\forall$SO formula over the finite structures. Is this proof idea suspect to naturalisation? Can we not conclude in advance that this attempt will lead to a proof that must be a natural proof? $\endgroup$ – Ramit Nov 26 '19 at 9:52
  • 2
    $\begingroup$ This is not a proof idea. This is just a trivial first step that does not really say anything about how the combinatorial core of the proof would proceed, so there is no telling whether it will lead to a natural proof. $\endgroup$ – Emil Jeřábek Nov 26 '19 at 12:58
  • $\begingroup$ Thank you @EmilJeřábeksupportsMonica. I got it. $\endgroup$ – Ramit Nov 27 '19 at 4:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.