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

theorem DescriptiveComplexity.ArithDef.not {L : FirstOrder.Language} {α : Type} {R : ArithRel L α} (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) => ¬R A v

The negation of a definable relation is definable.

theorem DescriptiveComplexity.ArithDef.and {L : FirstOrder.Language} {α : Type} {R S : ArithRel L α} (h : ArithDef R) (h' : ArithDef S) : 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 ∧ S A v

The conjunction of two definable relations is definable.

theorem DescriptiveComplexity.ArithDef.or {L : FirstOrder.Language} {α : Type} {R S : ArithRel L α} (h : ArithDef R) (h' : ArithDef S) : 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 ∨ S A v

The disjunction of two definable relations is definable.

theorem DescriptiveComplexity.ArithDef.imp {L : FirstOrder.Language} {α : Type} {R S : ArithRel L α} (h : ArithDef R) (h' : ArithDef S) : 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 → S A v

An implication between definable relations is definable.

theorem DescriptiveComplexity.ArithDef.iff {L : FirstOrder.Language} {α : Type} {R S : ArithRel L α} (h : ArithDef R) (h' : ArithDef S) : 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 ↔ S A v

An equivalence between definable relations is definable.

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

The always-true relation is definable.

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

The always-false relation is definable.

theorem DescriptiveComplexity.ArithDef.ite {L : FirstOrder.Language} {α : Type} {R S : ArithRel L α} (c : Prop) [Decidable c] (h : ArithDef R) (h' : ArithDef S) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => if c then R A v else S A v

A case distinction made outside the structure – a condition on the machine, not on the instance – is definable when both branches are.

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

A finite conjunction of definable relations is definable: the index ranges over a Fin k of the machine, not of the instance, so the conjunction is unfolded rather than quantified.

theorem DescriptiveComplexity.ArithDef.forallFinite {L : FirstOrder.Language} {α ι : Type} [Finite ι] {R : ι → ArithRel L α} (h : ∀ (j : ι), ArithDef (R j)) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∀ (j : ι), R j A v

A conjunction over a finite index of the machine, not of the instance: the index type is any finite type, and the conjunction is unfolded rather than quantified.

theorem DescriptiveComplexity.ArithDef.existsFinite {L : FirstOrder.Language} {α ι : Type} [Finite ι] {R : ι → ArithRel L α} (h : ∀ (j : ι), ArithDef (R j)) : ArithDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => ∃ (j : ι), R j A v

A disjunction over a finite index of the machine, by De Morgan.

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

A truth value fixed outside the structure is definable.

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.

theorem DescriptiveComplexity.arithDef_eq {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

Equality between two variables is definable.

theorem DescriptiveComplexity.arithDef_plus {L : FirstOrder.Language} {α : Type} (x y z : α) : 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) => orank (v x) + orank (v y) = orank (v z)

Addition of the ranks of three variables is definable.

theorem DescriptiveComplexity.arithDef_times {L : FirstOrder.Language} {α : Type} (x y z : α) : 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) => orank (v x) * orank (v y) = orank (v z)

Multiplication of the ranks of three 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

theorem DescriptiveComplexity.arithDef_rel {L : FirstOrder.Language} {α : Type} {a : ℕ} (R : L.Relations a) (arg : Fin a → α) : ArithDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => FirstOrder.Language.Structure.RelMap R fun (t : Fin a) => v (arg t)

Reading the input: an atom of the input vocabulary, at a tuple of variables, is definable. This is the only place the instance is looked at – in the machine reading of this logic it is the query instruction.

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.