Documentation

Complexity.Computability.Circuit.Boolean.FirstOrder.Parity

Parity is not first-order definable #

Parity is not first-order definable [FSS84], [Ajt83], [Imm99], even with arbitrary numerical relations: for a relational language L with finitely many relation symbols and a unary relation symbol P, and any interpretation N n of the symbols of L on each universe Fin n, no first-order sentence φ of L holds, for all large n and all sets S of elements, in the structure interpreting P as S and the other symbols as N n (ModelChecking.Expansion) exactly when S has an even number of elements (ModelChecking.not_eventually_forall_realize_expansion_iff_even). The numerical relations may be an order, BIT, or any relations at all, chosen separately for each size of universe, so parity is not in FO[Arb], the logical counterpart of nonuniform AC⁰ [Imm99]. In particular no sentence defines the even cardinality of P on all large finite structures (ModelChecking.not_forall_realize_iff_even_card).

The proof combines the two directions of the correspondence between first-order logic and constant-depth circuits. A sentence is decided on the structures with n elements, given by their atomic facts, by an unbounded fan-in formula of depth independent of n and size polynomial in n (ModelChecking.toUnbounded). Substituting the input bits for the facts P(a) and constants for the facts about the numerical relations (Formula.bind, Formula.depth_bind_le, Formula.size_bind_le, ModelChecking.leafSize_toUnbounded_le) gives formulas of constant depth and polynomial size on n inputs computing parity, against Håstad's theorem (Unbounded.two_pow_le_size_of_formula_computes_parity).

The language is relational, as in ModelChecking.toUnbounded, and has finitely many relation symbols, so that a structure on Fin n has finitely many atomic facts. Constant symbols, such as min and max in [Imm99], are not covered; a numerical constant can be expressed by a unary numerical relation holding of one element.

Main definitions #

Main results #

References #

Expansions by a unary relation #

source
def Cslib.Circuits.Boolean.ModelChecking.Expansion {L : FirstOrder.Language} {n : ℕ} (_P : L.Relations 1) (_N : L.Structure (Fin n)) (_S : Finset (Fin n)) :
Type

The universe Fin n with the structure interpreting the unary relation symbol P as the set S and every other relation symbol as the structure N does: the expansion of the numerical relations N by the input S.

Instances For
    source
    @[instance_reducible]
    instance Cslib.Circuits.Boolean.ModelChecking.Expansion.instStructure {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} {P : L.Relations 1} {N : L.Structure (Fin n)} {S : Finset (Fin n)} :
    L.Structure (Expansion P N S)
    source
    @[simp]
    theorem Cslib.Circuits.Boolean.ModelChecking.Expansion.relMap_self {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} {P : L.Relations 1} {N : L.Structure (Fin n)} {S : Finset (Fin n)} (t : Fin 1 → Expansion P N S) :
    FirstOrder.Language.Structure.RelMap P t ↔ t 0 ∈ S

    P holds of the elements of S.

    source
    theorem Cslib.Circuits.Boolean.ModelChecking.Expansion.relMap_of_ne {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} {P : L.Relations 1} {N : L.Structure (Fin n)} {S : Finset (Fin n)} {l : ℕ} {R : L.Relations l} (h : ⟨l, R⟩ ≠ ⟨1, P⟩) (t : Fin l → Expansion P N S) :
    FirstOrder.Language.Structure.RelMap R t ↔ FirstOrder.Language.Structure.RelMap R t

    The other relation symbols are interpreted as in N.

    Parity is not first-order definable #

    source
    theorem Cslib.Circuits.Boolean.ModelChecking.not_eventually_forall_realize_expansion_iff_even {L : FirstOrder.Language} [L.IsRelational] [Finite ((l : ℕ) × L.Relations l)] (P : L.Relations 1) (N : (n : ℕ) → L.Structure (Fin n)) (φ : L.Sentence) :
    ¬∀ᶠ (n : ℕ) in Filter.atTop, ∀ (S : Finset (Fin n)), Expansion P (N n) S ⊨ φ ↔ Even S.card

    Parity is not first-order definable, with arbitrary numerical relations [FSS84], [Ajt83], [Imm99]. Let L be a relational language with finitely many relation symbols, P a unary relation symbol of L, and N n any interpretation of the symbols of L on Fin n, for each n. No first-order sentence φ of L satisfies, for all large n and all sets S of elements of Fin n, that the structure interpreting P as S and the other symbols as N n satisfies φ exactly when S has an even number of elements.

    source
    theorem Cslib.Circuits.Boolean.ModelChecking.not_forall_realize_iff_even_card {L : FirstOrder.Language} [L.IsRelational] [Finite ((l : ℕ) × L.Relations l)] (P : L.Relations 1) (φ : L.Sentence) (n₀ : ℕ) :
    ¬∀ (M : Type) [inst : L.Structure M] [Finite M], n₀ ≤ Nat.card M → (M ⊨ φ ↔ Even (Nat.card { m : M // FirstOrder.Language.Structure.RelMap P ![m] }))

    Parity is not first-order definable [FSS84], [Ajt83], [Imm99]. For a relational language L with finitely many relation symbols and a unary relation symbol P, no first-order sentence of L holds, among the finite structures with at least n₀ elements, in exactly those in which P holds of an even number of elements.