Some formulas in Descriptive Complexity Theory

Here is a collection of logical formulas (hopefully) demonstrating the computational complexity of certain problems. Note that the quoted complexity class corrsponds to the formula, not the actual known complexity class.

Some formulas may be nonsense!

(c.f. Existential Second-Order Logic Over Graphs: A Complete Complexity-Theoretic Classification for the syntax-complexity correspondances)

Decision problems for basic graphs, in which E represents the edge relation, unary relations are represented as Cx for C(x), and binary relations R are represented as xRy for R(x,y). Below the table are some formulas expressing some first order properties and the notation used:
Problem Class Formula Quantifier form
2-Colourable L ∃C ∀uv (uEv → ¬((Cu∧Cv)∨(¬Cu∧¬Cv))) Eaa
Disconnected NL ∃E ∃xy∀uv (Cx∧¬Cy)∧((Cu∧¬Cv) → ¬uEv) E1e*aa
Square Root NP ∃R ∀uv R⊆E∧(uEv ↔ (uRv∨uR²v)) Eaaae
not-CIS NP ∃CS (MAXCLIQUE(C)∧MAXSTABLE(S)∧∀u¬(Cu∧Su)) E*(ae)*
Property Formula Notation
All edges of R are edges of E ∀uv (uRv → uEv) R⊆E
There is a vertex between u and v for the relation R ∃w(uRw∧wRv) uR²v
C is a maximal clique ∀uv((Cu∧Cv∧u≠v) → uEv)∧∀u(¬Cu → ∃v(Cv∧¬uEv)) MAXCLIQUE(C)
C is a maximal stable set ∀uv((Cu∧Cv) → ¬uEv)∧∀u(¬Cu → ∃v(Cv∧uEv)) MAXSTABLE(C)

Decision problems for knots, with an untwisted link diagram represented as a directed graph G with vertices V, edges E, functions s, e from V to E signifying the start and end vertices of an edge, and a binary relation O(v,e) signifying that the crossing at he vertex v of the edge e at the vertex is "over". When not explicit, large AND symbols are over all the non-specified parameters.
Problem Class Formula Quantifier form
Tricolourability NP ∃C1C2C3(⋀∃uCiu)∧∀u(⋀i≠j¬Ciu∧Cju)∧∀uefgh(V(u,e,f,g,h) → (⋀(Cie ↔ Cif)∧(⋀k=g,h¬(Cie∧Cik))∧(⋀¬Cig∧Cih))) E*(ae)*
Property Formula Notation
v is a vertex with edges e,f,g,h, with e and g ending at v, f and h starting at v, and e,f correspond to the arc passing over the crossing s(e)=v∧s(g)=v∧t(f)=v∧t(h)=v∧O(v,e)∧O(v,f)∧¬O(v,g)∧¬O(v,h) V(v,e,f,g,h)