Some formulas in Descriptive Complexity Theory

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

(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)