First-order definable queries belong to nonuniform AC0

The characteristic family of the existing binary query language has polynomial size and constant depth. The circuits reject malformed encodings and cover every input length, including zero. At positive length N, sentence φ has a circuit of size at most φ.validatedPolynomial.eval N and depth at most φ.size + 5.

This implements the finite quantifier construction in Immerman's Descriptive Complexity, Section 5.4, Theorem 5.22, for this library's unordered FO syntax and encoding. The ordered FO[BIT] characterization of uniform AC0 is a further result.

theorem Complexity.DescriptiveComplexity.queryFamily_eq_true {V : Vocabulary} (Q : BooleanQuery V) {N : ℕ} (input : BitString N) : queryFamily Q N input = true ↔ List.ofFn input ∈ queryLanguage Q

The query family is the characteristic function of the induced binary language.

@[simp]

theorem Complexity.DescriptiveComplexity.queryFamily_zero {V : Vocabulary} (Q : BooleanQuery V) (input : BitString 0) : queryFamily Q 0 input = false

Every induced query language rejects the empty input.

theorem Complexity.DescriptiveComplexity.Sentence.exists_circuit_on_length {V : Vocabulary} (φ : Sentence V) (N : ℕ) [NeZero N] : ∃ (gates : ℕ) (c : Circuit Basis.unboundedAndOr N 1 gates), c.size ≤ Polynomial.eval N φ.validatedPolynomial ∧ c.depth ≤ Formula.size φ + 5 ∧ ∀ (input : BitString N), c.eval input 0 = queryFamily (fun (A : FinStruct V) => Models A φ) N input

A fixed FO sentence has polynomial-size, constant-depth circuits at all positive lengths.

theorem Complexity.DescriptiveComplexity.Sentence.queryFamily_mem_AC0 {V : Vocabulary} (φ : Sentence V) : (queryFamily fun (A : FinStruct V) => Models A φ) ∈ AC0

The binary language defined by a first-order sentence has a nonuniform AC0 family.

theorem Complexity.DescriptiveComplexity.FODefinable.queryFamily_mem_AC0 {V : Vocabulary} {Q : BooleanQuery V} (hQ : FODefinable Q) : queryFamily Q ∈ AC0

Every FO-definable query induces a binary language in nonuniform AC0.