Counting Logic

Origin. Neil Immerman and Eric Lander, "Describing graphs: a first-order approach to graph canonization" (in Complexity Theory Retrospective, 1990), introduced the fragments C^k — k variables plus counting quantifiers — as a logical measure of how hard a graph is to identify, and matched them to the Weisfeiler–Leman refinement algorithm. Martin Otto's Bounded Variable Logics and Counting (Lecture Notes in Logic 9, 1997) is the systematic treatment.

Models. Ordinary relational structures, usually finite. What changes is the quantifier stock: ∃^{≥n} counts witnesses directly rather than laying down n distinct variables to do it. On finite structures this is a statement about variable economy, and the interesting objects are the fragments C^k with k variables fixed, whose equivalence classes are exactly the classes the (k−1)-dimensional Weisfeiler–Leman algorithm computes.

Formalism.

Counting quantifiers: ∃^{≥n}x.φ(x): at least n x satisfy φ. ∃^{=n}x.φ(x): exactly n. ∃^{≤n}x.φ(x): at most n. Numerical bounds.

First-order with counting: FO + counting quantifiers. C^k: k-variable fragment with counting. Strictly more expressive than FO^k; no more expressive than full FO.

Definability: |A| = |B| not FO-definable, and not definable by ∃^{≥n} either. ∃^{≥n} defines cardinality bounds only against fixed numerals. Equicardinality needs the Härtig quantifier or a second numeric sort.

No gain without a variable bound: ∃^{≥n}x φ(x) ≡ ∃x₁…∃x_n (⋀_{i<j} x_i ≠ x_j ∧ ⋀_i φ(x_i)). So FO with counting quantifiers = FO in expressive power. The whole content is in how many variables the translation costs.

C² (two-variable counting): x, y + counting. Important fragment. Decidable. Higher expressiveness than FO².

Numerical predicates: BIT(i, j): bit i of j is 1. Linear order arithmetic. Finite model focus.

Descriptive complexity: Over ordered structures with BIT, FO with counting captures uniform TC⁰. Threshold circuits of constant depth. Fixed-point logic with counting, FP+C, sits strictly inside PTIME.

Bounds: C^k ⊊ C^{k+1} on finite structures. Strict hierarchy in k.

Relation to pebble games: k-pebble bijection game (Hella). Spoiler picks a pebble; Duplicator supplies a bijection; Spoiler picks a point in it. Duplicator wins iff the structures agree on C^k.

Symbols.

Metatheory. Counting quantifiers add nothing on their own: ∃^{≥n}x φ(x) is already first-order, at a cost of n variables, so FO(C) and FO define the same classes and all the content is in the fragments C^k. Immerman and Lander (1990) matched C^{k+1}-equivalence with indistinguishability by the k-dimensional Weisfeiler–Leman algorithm, and Hella (1996) characterized the same relation by the k-pebble bijection game, giving a combinatorial and an algorithmic handle on the same equivalence — which is decidable in polynomial time for fixed k. Cai, Fürer, and Immerman, "An optimal lower bound on the number of variables for graph identification" (Combinatorica, 1992), constructed graphs on O(n) vertices that C^n does not separate, which shows the C^k hierarchy is strict and that fixed-point logic with counting fails to capture PTIME. Over ordered structures with BIT, first-order logic with counting captures uniform TC⁰ (Barrington, Immerman, Straubing, 1990). Grädel, Otto, and Rosen (1997) proved C² decidable, and Pratt-Hartmann (2005) settled its satisfiability and finite satisfiability as NEXPTIME-complete.

Applies to. Finite model theory. Complexity. Database theory. Graph isomorphism.

Limitations. Over arbitrary structures with no bound on variables the logic is exactly first-order, so every non-definability result for FO — connectivity, reachability, parity of the universe — carries over unchanged; counting adds power only inside a fixed-variable fragment or against a separate numeric sort. Even then, ∃^{≥n} compares against a fixed numeral and cannot say that two definable sets are equinumerous; equicardinality requires the Härtig quantifier. The Cai–Fürer–Immerman graphs put a hard ceiling on the whole approach: no fixed C^k identifies all graphs, so counting logic does not decide isomorphism, and Atserias, Bulatov, and Dawar (2009) showed that solvability of linear systems over a finite field is in PTIME yet undefinable in FP+C, so adding recursion does not close the gap either. The TC⁰ capturing result needs a built-in linear order and BIT; drop the order and it fails.

© 2026 Lingenic LLC