First-order sums and products of witness counts

The two first-order quantifiers of ΣQSO(FO) keep witness counts witness counts.

• The sum over the n-tuples (DescriptiveComplexity.WCount.sum): the tuple is guessed too, as n unary relation variables holding one element each.
• The product over the n-tuples (DescriptiveComplexity.WCount.prod): one witness per tuple, i.e., every relation variable of the block takes the tuple as n more arguments (DescriptiveComplexity.SOBlock.extend); the formula reads them by substituting X'(w̄, ȳ) for every atom X(ȳ) (DescriptiveComplexity.extendRel), and holds for every tuple.

The sum over tuples

@[reducible]

def DescriptiveComplexity.tupleBlock (n : ℕ) : SOBlock

n unary relation variables.

Equations

• DescriptiveComplexity.tupleBlock n = { ι := Fin n, ιFinite := ⋯, arity := fun (x : Fin n) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.WCount.wSym {M : FirstOrder.Language} (B : SOBlock) (n : ℕ) (i : Fin n) : (M.sum (B.cons (tupleBlock n)).lang).Relations 1

The i-th unary relation variable, beside the block B.

Equations

• DescriptiveComplexity.WCount.wSym B n i = Sum.inr ⟨Sum.inr i, ⋯⟩

noncomputable def DescriptiveComplexity.WCount.exactlyOneF {M : FirstOrder.Language} {α : Type} (B : SOBlock) (n : ℕ) (i : Fin n) : (M.sum (B.cons (tupleBlock n)).lang).Formula α

“The i-th unary relation variable holds of exactly one element.”

Equations

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

noncomputable def DescriptiveComplexity.WCount.sumKernel {M : FirstOrder.Language} {α : Type} (B : SOBlock) (n : ℕ) (φ : (M.sum B.lang).Formula (α ⊕ Fin n)) : (M.sum (B.cons (tupleBlock n)).lang).Formula α

The kernel of a sum over tuples: each unary relation variable holds of exactly one element, and the tuple of these elements satisfies the formula.

Equations

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

theorem DescriptiveComplexity.WCount.realize_sumKernel {M : FirstOrder.Language} {α : Type} {B : SOBlock} {n : ℕ} {A : Type} [M.Structure A] (φ : (M.sum B.lang).Formula (α ⊕ Fin n)) (ρ : B.Assignment A) (μ : (tupleBlock n).Assignment A) (v : α → A) : (sumKernel B n φ).Realize v ↔ (∀ (i : (tupleBlock n).ι), ∃ (y : A), μ i ![y] ∧ ∀ (z : A), μ i ![z] → z = y) ∧ ∃ (w : Fin n → A), (∀ (i : (tupleBlock n).ι), μ i ![w i]) ∧ φ.Realize (Sum.elim v w)

noncomputable def DescriptiveComplexity.WCount.pickOf {n : ℕ} {A : Type} (μ : (tupleBlock n).Assignment A) (h : ∀ (i : (tupleBlock n).ι), ∃ (y : A), μ i ![y] ∧ ∀ (z : A), μ i ![z] → z = y) (i : Fin n) : A

The element a unary relation variable holding of exactly one element holds of.

Equations

• DescriptiveComplexity.WCount.pickOf μ h i = Classical.choose ⋯

def DescriptiveComplexity.WCount.tupleAssign {n : ℕ} {A : Type} (w : Fin n → A) : (tupleBlock n).Assignment A

The unary relation variables holding of the elements of a tuple.

Equations

• DescriptiveComplexity.WCount.tupleAssign w i x = (x 0 = w i)

theorem DescriptiveComplexity.WCount.tupleAssign_spec {n : ℕ} {A : Type} (w : Fin n → A) (i : Fin n) : ∃ (y : A), tupleAssign w i ![y] ∧ ∀ (z : A), tupleAssign w i ![z] → z = y

noncomputable def DescriptiveComplexity.WCount.sumEquiv' {M : FirstOrder.Language} {α : Type} {B : SOBlock} {n : ℕ} {A : Type} [M.Structure A] (φ : (M.sum B.lang).Formula (α ⊕ Fin n)) (v : α → A) : FWit M (B.cons (tupleBlock n)) (sumKernel B n φ) A v ≃ (w : Fin n → A) × FWit M B φ A (Sum.elim v w)

The witnesses of a sum over tuples are a tuple and a witness for it.

Equations

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

theorem DescriptiveComplexity.WCount.sum {M : FirstOrder.Language} {α : Type} (n : ℕ) {f : (A : Type) → [M.Structure A] → (α ⊕ Fin n → A) → ℕ} (hf : WCount M (α ⊕ Fin n) f) : WCount M α fun (A : Type) (x : M.Structure A) (v : α → A) => ∑ᶠ (w : Fin n → A), f A (Sum.elim v w)

The sum of a witness count over the tuples is a witness count.

The product over tuples

@[reducible]

def DescriptiveComplexity.SOBlock.extend (B : SOBlock) (n : ℕ) : SOBlock

Every relation variable of the block takes n more arguments.

Equations

• B.extend n = { ι := B.ι, ιFinite := ⋯, arity := fun (i : B.ι) => n + B.arity i }

def DescriptiveComplexity.SOBlock.extendAssignEquiv (B : SOBlock) (n : ℕ) (A : Type) : (B.extend n).Assignment A ≃ ((Fin n → A) → B.Assignment A)

The assignments of the extended block are the families of assignments indexed by the n-tuples.

Equations

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

def DescriptiveComplexity.castTerm {M : FirstOrder.Language} {B B' : SOBlock} {γ : Type} : (M.sum B.lang).Term γ → (M.sum B'.lang).Term γ

A term of a relational expansion, read in another expansion of the same base vocabulary.

Equations

• DescriptiveComplexity.castTerm (FirstOrder.Language.var x_1) = FirstOrder.Language.var x_1
• DescriptiveComplexity.castTerm (FirstOrder.Language.func (Sum.inl f) ts) = FirstOrder.Language.func (Sum.inl f) fun (i : Fin l) => DescriptiveComplexity.castTerm (ts i)
• DescriptiveComplexity.castTerm (FirstOrder.Language.func (Sum.inr f) _ts) = isEmptyElim f

def DescriptiveComplexity.extendRel {M : FirstOrder.Language} {α : Type} {B : SOBlock} {n : ℕ} (w : Fin n → α) {k : ℕ} : (M.sum B.lang).BoundedFormula α k → (M.sum (B.extend n).lang).BoundedFormula α k

Substituting X'(w̄, ȳ) for every atom X(ȳ) of a relation variable of the block, w̄ free variables.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.extendRel w FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• DescriptiveComplexity.extendRel w (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.BoundedFormula.equal (DescriptiveComplexity.castTerm t₁) (DescriptiveComplexity.castTerm t₂)
• DescriptiveComplexity.extendRel w (φ.imp ψ) = (DescriptiveComplexity.extendRel w φ).imp (DescriptiveComplexity.extendRel w ψ)
• DescriptiveComplexity.extendRel w φ.all = (DescriptiveComplexity.extendRel w φ).all

theorem DescriptiveComplexity.WCount.prod {M : FirstOrder.Language} {α : Type} (n : ℕ) {f : (A : Type) → [M.Structure A] → (α ⊕ Fin n → A) → ℕ} (hf : WCount M (α ⊕ Fin n) f) : WCount M α fun (A : Type) (x : M.Structure A) (v : α → A) => ∏ᶠ (w : Fin n → A), f A (Sum.elim v w)

The product of a witness count over the tuples is a witness count: one witness per tuple, read off the extended block.