Every formula over decided relations is decided

The induction that removes first-order structure around walks: if every relation variable of a block is decided by a DescriptiveComplexity.Decider – at the tuple as parameters – then every first-order formula over the base vocabulary expanded by the block is decided by one (DescriptiveComplexity.Decider.exists_of_formula), and the decider is functional when the block's are.

The induction is on FirstOrder.Language.BoundedFormula, whose constructors are exactly the algebra of DescriptiveComplexity.TransitiveClosureDecide: ⊥, equality and a base relation are atoms, an atom of the block is its decider with the parameters renamed to the atom's arguments, implication is DescriptiveComplexity.Decider.imp, and ∀ is DescriptiveComplexity.Decider.all with the bound variable frozen.

Stated for a block whose assignment is a function of the structure, as the reachability relations of a family of walks are (DescriptiveComplexity.TCFamily.reachAssign); the deciders of those are built in DescriptiveComplexity.TransitiveClosureDecideReach and DescriptiveComplexity.TransitiveClosureDecideReachDet.

@[reducible, inline]

abbrev DescriptiveComplexity.Decider.ExpRealize {L : FirstOrder.Language} {B : SOBlock} (ρ : (A : Type) → [L.Structure A] → [LinearOrder A] → B.Assignment A) {A : Type} [L.Structure A] [LinearOrder A] {α : Type} {n : ℕ} (φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula α n) (v : α → A) (xs : Fin n → A) : Prop

Realization of a formula over the expansion of the ordered base by a block, at the assignment the block has on the structure.

Equations

• DescriptiveComplexity.Decider.ExpRealize ρ φ v xs = φ.Realize v xs

theorem DescriptiveComplexity.Decider.exists_of_formula {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} (ρ : (A : Type) → [L.Structure A] → [LinearOrder A] → B.Assignment A) (Dq : (q : B.ι) → Decider L (Fin (B.arity q))) (hD : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (q : B.ι) (w : Fin (B.arity q) → A), (Dq q).Decides w (ρ A q w)) {α : Type} {n : ℕ} (φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula α n) : ∃ (D : Decider L (α ⊕ Fin n)), (∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (v : α → A) (xs : Fin n → A), D.Decides (Sum.elim v xs) (ExpRealize ρ φ v xs)) ∧ ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A], (∀ (q : B.ι), (Dq q).Functional A) → D.Functional A

Every formula over decided relations is decided. Given, for each relation variable of the block, a decider of its assignment at the tuple as parameters, every first-order formula over the expansion has a decider at its free variables as parameters, functional when the given ones are.