Witness counts with free variables, and their closure properties

A function of a structure and a valuation is a witness count (DescriptiveComplexity.WCount) when it counts the assignments of a block of relation variables satisfying a first-order formula with those free variables. Witness counts are closed under every construction of ΣQSO(FO):

• a formula, counting 1 or 0 (DescriptiveComplexity.WCount.ind), and a constant (DescriptiveComplexity.WCount.const);
• the product of two (DescriptiveComplexity.WCount.mul): the two blocks side by side, the two formulas conjoined;
• the sum of two (DescriptiveComplexity.WCount.add): the two blocks and a selector of arity zero, as in DescriptiveComplexity.pairKernel;
• the second-order sum (DescriptiveComplexity.WCount.sosum): the summed block joins the block of the count.

The first-order sum and product are in DescriptiveComplexity.Counting.QSOQuantifiers.

@[reducible, inline]

abbrev DescriptiveComplexity.FWit (M : FirstOrder.Language) (B : SOBlock) {α : Type} (φ : (M.sum B.lang).Formula α) (A : Type) [M.Structure A] (v : α → A) : Type

The witnesses of a formula with free variables, under a valuation.

Equations

• DescriptiveComplexity.FWit M B φ A v = { ρ : B.Assignment A // φ.Realize v }

def DescriptiveComplexity.WCount (M : FirstOrder.Language) (α : Type) (f : (A : Type) → [M.Structure A] → (α → A) → ℕ) : Prop

A witness count: on finite structures, the number of witnesses of a formula with free variables, for some block.

Equations

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

theorem DescriptiveComplexity.WCount.ind {M : FirstOrder.Language} {α : Type} (φ : M.Formula α) : WCount M α fun (x : Type) (x_1 : M.Structure x) (v : α → x) => if φ.Realize v then 1 else 0

A formula counts 1 or 0: the trivial block.

Products

noncomputable def DescriptiveComplexity.WCount.liftFstF {M : FirstOrder.Language} {α : Type} (B C : SOBlock) (φ : (M.sum B.lang).Formula α) : (M.sum (B.cons C).lang).Formula α

A formula over the expansion by B, read over the expansion by SOBlock.cons B C.

Equations

• DescriptiveComplexity.WCount.liftFstF B C φ = (DescriptiveComplexity.mergeStep M B C).onFormula (FirstOrder.Language.LHom.sumInl.onFormula φ)

noncomputable def DescriptiveComplexity.WCount.liftSndF {M : FirstOrder.Language} {α : Type} (B C : SOBlock) (φ : (M.sum C.lang).Formula α) : (M.sum (B.cons C).lang).Formula α

A formula over the expansion by C, read over the expansion by SOBlock.cons B C.

Equations

• DescriptiveComplexity.WCount.liftSndF B C φ = (DescriptiveComplexity.mergeStep M B C).onFormula ((FirstOrder.Language.LHom.sumInl.sumMap (FirstOrder.Language.LHom.id C.lang)).onFormula φ)

theorem DescriptiveComplexity.WCount.mul {M : FirstOrder.Language} {α : Type} {f g : (A : Type) → [M.Structure A] → (α → A) → ℕ} (hf : WCount M α f) (hg : WCount M α g) : WCount M α fun (A : Type) (x : M.Structure A) (v : α → A) => f A v * g A v

The product of two witness counts is a witness count: the two blocks side by side, the two formulas conjoined.

Second-order sums

theorem DescriptiveComplexity.WCount.sosum {M : FirstOrder.Language} {α : Type} (C : SOBlock) {g : (A : Type) → [(M.sum C.lang).Structure A] → (α → A) → ℕ} (hg : WCount (M.sum C.lang) α g) : WCount M α fun (A : Type) (inst : M.Structure A) (v : α → A) => ∑ᶠ (X : C.Assignment A), g A v

The second-order sum of a witness count is a witness count: the summed block joins the block of the count.

Sums

noncomputable def DescriptiveComplexity.WCount.emptyF {M : FirstOrder.Language} {α : Type} (B : SOBlock) : (M.sum B.lang).Formula α

“The relation variables of the block are empty”, as a formula.

Equations

• DescriptiveComplexity.WCount.emptyF B = FirstOrder.Language.Formula.relabel Empty.elim (DescriptiveComplexity.emptyBlockS B)

@[reducible, inline]

abbrev DescriptiveComplexity.WCount.sumBlock (B C : SOBlock) : SOBlock

The block of a sum: the two blocks and a selector.

Equations

• DescriptiveComplexity.WCount.sumBlock B C = B.cons (C.cons DescriptiveComplexity.boolBlock)

noncomputable def DescriptiveComplexity.WCount.selF {M : FirstOrder.Language} {α : Type} (B C : SOBlock) : (M.sum (sumBlock B C).lang).Formula α

“The selector holds.”

Equations

• DescriptiveComplexity.WCount.selF B C = FirstOrder.Language.Relations.formula (Sum.inr ⟨Sum.inr (Sum.inr ()), ⋯⟩) finZeroElim

noncomputable def DescriptiveComplexity.WCount.sumF {M : FirstOrder.Language} {α : Type} (B C : SOBlock) (φ : (M.sum B.lang).Formula α) (ψ : (M.sum C.lang).Formula α) : (M.sum (sumBlock B C).lang).Formula α

The kernel of a sum: the first formula of the first block when the selector holds, the second block being empty; the second formula of the second block otherwise, the first block being empty.

Equations

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

def DescriptiveComplexity.WCount.emptyAssign (C : SOBlock) (A : Type) : C.Assignment A

The empty assignment.

Equations

• DescriptiveComplexity.WCount.emptyAssign C A x✝¹ x✝ = False

def DescriptiveComplexity.WCount.selAssign (b : Prop) (A : Type) : boolBlock.Assignment A

The selector, true or false.

Equations

• DescriptiveComplexity.WCount.selAssign b A x✝¹ x✝ = b

theorem DescriptiveComplexity.WCount.add {M : FirstOrder.Language} {α : Type} {f g : (A : Type) → [M.Structure A] → (α → A) → ℕ} (hf : WCount M α f) (hg : WCount M α g) : WCount M α fun (A : Type) (x : M.Structure A) (v : α → A) => f A v + g A v

The sum of two witness counts is a witness count.

theorem DescriptiveComplexity.WCount.const {M : FirstOrder.Language} {α : Type} (s : ℕ) : WCount M α fun (x : Type) (x_1 : M.Structure x) (x_2 : α → x) => s

A constant is a witness count.