<p>I wished to know if the proof attempts at separation of complexity classes via the methods outlined by Descriptive Complexity theorists naturalise?</p>
<p>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.</p>
<p>If one reads up Kolaitis, Vardi, Libkin et al's book on Finite Model Theory and its applications there are intriguing statements like TFAE :</p>
<blockquote>
<p>NP <span class="math-container">$\not=$</span> coNP</p>
</blockquote>
<p>and</p>
<blockquote>
<p>For every <span class="math-container">$s_1$</span>,<span class="math-container">$\ldots$</span>, <span class="math-container">$s_k$</span>, <span class="math-container">$r$</span>, there are finite graphs <strong>G</strong> and <strong>H</strong> such that</p>
<ul>
<li><strong>G</strong> is not 3-Colourable and <strong>H</strong> is 3-Colourable</li>
<li>the Duplicator wins the (⟨<span class="math-container">$s_1$</span>,<span class="math-container">$\ldots$</span>,<span class="math-container">$s_k$</span>⟩,<span class="math-container">$r$</span>) EF game on <strong>G</strong> and <strong>H</strong>.</li>
</ul>
</blockquote>
<p>This is after setting up the logic characterising the class NP and then coming up with the inexpressibility techniques of the EF games.</p>
<p>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.</p>

CC BY-SA 4.0
2019-11-26T08:06:14.257Z
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*.
Emil Jeřábek
CC BY-SA 4.0
2019-11-26T09:52:46.063Z
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?
Ramit
CC BY-SA 4.0
2019-11-26T12:58:38.980Z
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.
Emil Jeřábek
CC BY-SA 4.0
2019-11-27T04:40:24.033Z
Thank you @EmilJeřábeksupportsMonica. I got it.
Ramit
<complexity-classes><descriptive-complexity><natural-proofs>
Does Descriptive Complexity techniques have the naturalisation barrier?
Ramit
# Does Descriptive Complexity techniques have the naturalisation barrier?

(Asked by: username_0 on 2019-11-26)

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.

**Tags:** complexity-classes, descriptive-complexity, natural-proofs
> **Comments:**
> **username_1**: 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*.  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: Thank you @EmilJeřábeksupportsMonica. I got it.  

---

## 0 answers

