Weighted worlds, with every fact as a variable

DescriptiveComplexity.weightedWorlds_eq_weightedCount reads the count of the weighted worlds as a weighted count over the valuations of the open facts. For computing it, a more uniform reading is convenient: every fact of the schema over the universe is a Boolean variable, with two weights that say everything about its status (DescriptiveComplexity.fullPresWeight, DescriptiveComplexity.fullAbsWeight):

the fact is	weight of presence	weight of absence
certain	1	0
open	its weight of presence	its weight of absence
neither	0	1

A valuation that is not a possible world then has weight 0, and the count is a weighted count over all the valuations (DescriptiveComplexity.weightedWorlds_eq_weightedCount_facts), with no side condition on the worlds: the independence lemmas of DescriptiveComplexity.Counting.Independence apply to it as they stand.

noncomputable def DescriptiveComplexity.fullPresWeight {L : FirstOrder.Language} {A : Type} [(weightedLang L).Structure A] (q : Fact L A) : ℕ

The weight of presence of a fact, whatever its status.

Equations

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

noncomputable def DescriptiveComplexity.fullAbsWeight {L : FirstOrder.Language} {A : Type} [(weightedLang L).Structure A] (q : Fact L A) : ℕ

The weight of absence of a fact, whatever its status.

Equations

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

def DescriptiveComplexity.factWorld {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} (v : Fact L A → Bool) : (worldBlock L).Assignment A

The family of relations of a valuation of all the facts.

Equations

• DescriptiveComplexity.factWorld v p x = (v ⟨p, x⟩ = true)

@[instance_reducible]

noncomputable instance DescriptiveComplexity.factFintype {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [Finite A] : Fintype (Fact L A)

The facts over a finite universe, as a finite type.

Equations

• DescriptiveComplexity.factFintype = Fintype.ofFinite (DescriptiveComplexity.Fact L A)

noncomputable def DescriptiveComplexity.factWorldEquiv (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] (A : Type) : (Fact L A → Bool) ≃ (worldBlock L).Assignment A

Families of relations are valuations of the facts.

Equations

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

theorem DescriptiveComplexity.weightedWorlds_eq_weightedCount_facts {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] [Finite A] [Fintype (Fact L A)] [DecidableEq (Fact L A)] (hlin : IsLinOrd (WLe L A)) (φ : L.Sentence) : (WeightedWorlds φ).Count A = weightedCount fullPresWeight fullAbsWeight fun (v : Fact L A → Bool) => decide (A ⊨ φ)

The count is a weighted count over the valuations of all the facts: on an instance whose positions are linearly ordered, counting the weighted worlds of a sentence is the weighted count of the event that the sentence holds, every fact being a variable.