Counting Logic

Origin. Immerman, Lander (1990), various. Counting quantifiers. Cardinality comparison. Extends first-order. Foundation of descriptive complexity.

Models. Counting quantifiers. Numerical predicates. Cardinality in logic. Beyond first-order expressiveness.

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. More expressive than FO.

Definability: |A| = |B| not FO-definable. ∃^{≥n} defines cardinality bounds. Counting extends expressiveness.

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: FO + counting: captures TC⁰. Threshold circuits. Complexity class characterization.

Bounds: C^k < C^{k+1} on suitable structures. Hierarchy. Strict increase.

Relation to pebble games: k-pebble bijection games. Captures C^k equivalence. Counting moves.

Symbols.

Symbol	Unicode	Meaning
∃^{≥n}	—	at least n
∃^{=n}	—	exactly n
C^k	—	k-variable counting
FO(C)	—	first-order + counting

Metatheory. Counting quantifiers. Variable fragments. Descriptive complexity. Pebble games.

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

Limitations. Finite focus. Not full counting power. Complexity boundaries. Technical.