lately I'm reading about descriptive complexity, which I find is a fascinating branch of computational complexity. I found many formulas in $\exists$$SO$ that describe problems with graphs but none that describes the 3SAT language.
Thinking about it, I came to an "atomic" description like this:
Where $v$ is a literal, $C$ is a clause (i.e. the $OR$ of 3 literals) and $P(C)$ means that $C$ is true.
However I'm not satisfied with this definition, I don't think it captures the complexity of the 3SAT language, especially the dependence of the variables on one another. Can you tell me a correct formula to describe this decision problem? Thank you.