Arithmetically definable relations: AC⁰ definability with free variables

DescriptiveComplexity.AC0Definable is a statement about sentences, and a sentence is an awkward thing to build by hand: every construction carries its own variable bookkeeping through FirstOrder.Language.Formula.iExs and Sum.elim. This file does that bookkeeping once, and then never again: DescriptiveComplexity.ArithDef says that a family of relations on valuations – one relation for every nonempty finite ordered structure – is realized by a single formula of the arithmetic expansion, and the lemmas below close the notion under the Boolean connectives and under quantification.

Everything downstream is then semantic. A construction states what its relation means on ranks, chains the closure lemmas, and reads the sentence off at the end with DescriptiveComplexity.ArithDef.ac0Definable; no formula is ever inspected again.

Conventions

Variables are indexed by an arbitrary type α, as Formula α is, and a quantifier binds the variables of Fin 1 in α ⊕ Fin 1 (DescriptiveComplexity.ArithDef.ex, DescriptiveComplexity.ArithDef.all) – the layout of FirstOrder.Language.Formula.iExs, so that no relabeling is needed at the quantifier step. Moving between variable layouts is DescriptiveComplexity.ArithDef.relabel, and a relation with no free variables (α = Empty) is literally a sentence, which is what DescriptiveComplexity.ArithDef.ac0Definable reads.

The three groups of lemmas

• Atoms – the order, the two numeric predicates, equality, and an input relation read at a tuple of variables (DescriptiveComplexity.arithDef_le, _plus, _times, _eq, _rel).
• Connectives – negation, conjunction, disjunction, implication, and the two constants.
• Quantifiers – DescriptiveComplexity.ArithDef.ex and DescriptiveComplexity.ArithDef.all, together with the vector forms DescriptiveComplexity.ArithDef.exs and DescriptiveComplexity.ArithDef.alls binding a whole Fin k of variables at once.

A DescriptiveComplexity.ArithDef.congr lemma lets a relation be replaced by a pointwise-equivalent one, which is how a semantic reformulation – the shape most proofs actually want – is fed to the closure lemmas.

Relations on valuations of a finite ordered structure

@[reducible, inline]

abbrev DescriptiveComplexity.ArithRel (L : FirstOrder.Language) (α : Type) : Type 1

A family of relations on α-indexed valuations: one relation for every nonempty finite ordered L-structure. The instance arguments are those of DescriptiveComplexity.AC0Definable, since that is what the family is eventually read as.

Equations

• DescriptiveComplexity.ArithRel L α = ((A : Type) → [L.Structure A] → [LinearOrder A] → [Finite A] → [Nonempty A] → (α → A) → Prop)

def DescriptiveComplexity.ArithDef {L : FirstOrder.Language} {α : Type} (R : ArithRel L α) : Prop

A family of relations is arithmetically definable when one formula of the arithmetic expansion realizes it in every nonempty finite ordered structure – first-order logic with ≤, + and × on the ranks, with free variables indexed by α.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.ArithDef.congr {L : FirstOrder.Language} {α : Type} {R S : ArithRel L α} (h : ArithDef R) (he : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A] (v : α → A), R A v ↔ S A v) : ArithDef S

Definability transfers along a pointwise equivalence of relations: the formula is unchanged, only the semantic reading of it is.

theorem DescriptiveComplexity.ArithDef.relabel {L : FirstOrder.Language} {α β : Type} {R : ArithRel L α} (h : ArithDef R) (f : α → β) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : β → A) => R A (v ∘ f)

Renaming the free variables: a definable relation read through a substitution of variables is definable.

Connectives

Atoms

theorem DescriptiveComplexity.arithDef_le {L : FirstOrder.Language} {α : Type} (x y : α) : ArithDef fun (x_1 : Type) (x_2 : L.Structure x_1) (x_3 : LinearOrder x_1) (x_4 : Finite x_1) (x_5 : Nonempty x_1) (v : α → x_1) => v x ≤ v y

The order between two variables is definable.

@[reducible, inline]

abbrev DescriptiveComplexity.inSym {L : FirstOrder.Language} {a : ℕ} (R : L.Relations a) : (L.sum FirstOrder.Language.arith).Relations a

An input relation symbol, in the arithmetic expansion of its vocabulary. Named, as every symbol of a sum vocabulary in this library is, so that rw matches it.

Equations

• DescriptiveComplexity.inSym R = Sum.inl R

Quantifiers

theorem DescriptiveComplexity.ArithDef.ex {L : FirstOrder.Language} {α : Type} {R : ArithRel L (α ⊕ Fin 1)} (h : ArithDef R) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∃ (a : A), R A (Sum.elim v fun (x : Fin 1) => a)

Existential quantification of one variable: the variable of Fin 1 in α ⊕ Fin 1, which is the layout FirstOrder.Language.Formula.iExs binds.

theorem DescriptiveComplexity.ArithDef.all {L : FirstOrder.Language} {α : Type} {R : ArithRel L (α ⊕ Fin 1)} (h : ArithDef R) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∀ (a : A), R A (Sum.elim v fun (x : Fin 1) => a)

Universal quantification of one variable, in the same layout.

theorem DescriptiveComplexity.ArithDef.exs {L : FirstOrder.Language} {α : Type} {k : ℕ} {R : ArithRel L (α ⊕ Fin k)} (h : ArithDef R) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∃ (w : Fin k → A), R A (Sum.elim v w)

Existential quantification of a block of k variables at once.

theorem DescriptiveComplexity.ArithDef.alls {L : FirstOrder.Language} {α : Type} {k : ℕ} {R : ArithRel L (α ⊕ Fin k)} (h : ArithDef R) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∀ (w : Fin k → A), R A (Sum.elim v w)

Universal quantification of a block of k variables at once.

From a closed relation to a sentence

theorem DescriptiveComplexity.ArithDef.ac0Definable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} {R : ArithRel L Empty} (h : ArithDef R) (hP : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A], P.Holds A ↔ R A Empty.elim) : AC0Definable P

The bridge to DescriptiveComplexity.AC0Definable: a definable relation with no free variables is an AC⁰ definition of the problem it states – a formula over Empty is a sentence.