Descriptive Complexity

Origin. Fagin (1974), Immerman, Vardi (1982). Characterizes computational complexity classes by logical expressiveness over finite structures. Companion to Finite Model Theory, focused on the capture program.

Models. A complexity class is "captured" by a logic when exactly the class-decidable properties of finite structures are the logic-definable ones. Resources correspond to expressive power, independent of any machine model.

Formalism.

Capture: Logic L captures class C iff for every property P of finite (ordered) structures: P ∈ C ⟺ P definable in L.

Fagin's theorem: NP = ∃SO (existential second-order). No ordering required.

Immerman-Vardi: P = FO(LFP) = FO(IFP) on ordered structures. Least/inflationary fixed point.

Transitive closure: NL = FO(TC). L = FO(DTC) (deterministic TC). Immerman-Szelepcsényi: NL closed under complement.

Capture catalog (ordered): AC⁰ = FO(BIT). L = FO(DTC). NL = FO(TC). P = FO(LFP). PSPACE = FO(PFP) = SO(TC). EXPTIME = SO(LFP).

Methodology: Reductions rendered as first-order interpretations. Lower bounds via Ehrenfeucht-Fraïssé games and quantifier rank.

Symbols.

Symbol	Unicode	Name	Meaning
⁰	U+2070	Superscript zero	Circuit depth, as in AC⁰
∃	U+2203	Existential quantifier	Second-order block in Fagin's theorem
∈	U+2208	Element of	Membership in a complexity class
⟺	U+27FA	If and only if	The capture biconditional
FO	—	First-order logic	Base logic, capturing AC⁰ with order and BIT
SO	—	Second-order logic	Quantification over relations; SO = PH
∃SO	—	Existential SO	Fagin's logic for NP, no order needed
FO(LFP)	—	Least fixed point	Logic for P on ordered structures
FO(IFP)	—	Inflationary fixed point	Equal in power to LFP (Gurevich–Shelah)
FO(PFP)	—	Partial fixed point	Logic for PSPACE on ordered structures
FO(TC)	—	Transitive closure	Logic for NL
FO(DTC)	—	Deterministic TC	Logic for L
SO(TC)	—	Second-order TC	Another capture of PSPACE
SO(LFP)	—	Second-order LFP	Logic for EXPTIME
FP+C	—	Fixed point with counting	Fixed point plus counting quantifiers
BIT	—	Bit predicate	BIT(i,j): bit i of j is 1
<	—	Linear order	Built-in order most captures require
P, NP	—	Polynomial time classes	Deterministic and nondeterministic
L, NL	—	Logarithmic space classes	Deterministic and nondeterministic

Metatheory. Fagin (1974) proved NP = ∃SO over finite structures with no built-in order, which remains the only major capture that is order-free; iterating it gives SO = PH level by level. Immerman (1986) and Vardi (1982) independently proved P = FO(LFP) on ordered structures, and Gurevich and Shelah (1986) showed inflationary and least fixed points have the same expressive power there, so FO(IFP) = FO(LFP). Immerman's (1988) logical proof that FO(TC) is closed under complement is the same argument as NL = coNL, obtained simultaneously by Szelepcsényi. Order is not a technicality: Abiteboul and Vianu (1991) proved that FO(LFP) = FO(PFP) as query languages on unordered finite structures if and only if P = PSPACE, so the separation questions transfer exactly. Gurevich (1988) conjectured no logic captures P without order; Cai, Fürer, and Immerman (1992) ruled out FP+C, and Grohe (2010) showed FP+C does capture P on every class of graphs with an excluded minor.

Applies to. Complexity theory foundations. Database query languages. Constraint satisfaction. Parameterized complexity. Separation questions via logical inexpressibility.

Limitations. Every capture below NP depends on a built-in linear order, and the order is an artefact the answer must not see, so what is really wanted is order-invariant definability — which is not an effective syntax, since by Trakhtenbrot's theorem the order-invariant sentences are not decidable, and a logic in the capture sense is supposed to have a recursive syntax. Without order the captures fail for a concrete reason: fixed-point logic cannot express the parity of the universe, and adding counting does not repair it, as the Cai–Fürer–Immerman graphs show. Trakhtenbrot also denies the field any completeness theorem over finite models, so the classical model-theoretic toolkit is unavailable. The programme has produced no separations: P versus NP becomes FO(LFP) versus ∃SO on ordered structures, and Ehrenfeucht–Fraïssé games, which are the only general lower-bound method here, are defeated by the order they need. Real lower bounds exist only in monadic fragments (Ajtai–Fagin) and do not generalize.

See Finite Model Theory for the broader theory of logic over finite structures (0-1 laws, locality).