Possible worlds are weighted worlds of weight one

The unweighted problem of DescriptiveComplexity.Counting.PossibleWorlds, where every uncertain fact is present with probability 1/2, is the case of DescriptiveComplexity.Counting.WeightedWorlds in which every fact has the weights 1 and 1.

• DescriptiveComplexity.unitWeightStructure: the weighted instance of an ordered instance, the weight 1 being the single bit of the least position (DescriptiveComplexity.binNum_isBot);
• DescriptiveComplexity.weightedWorlds_unitWeight: its weighted worlds are counted like the worlds of the instance, every product of weights being 1;
• DescriptiveComplexity.possibleWorlds_ordered_parsimonious_weightedWorlds: the instance is first-order definable (DescriptiveComplexity.unitWeightInterp), so counting worlds reduces parsimoniously to counting weighted worlds. The reduction is an ordered one: writing the number 1 means naming the least position.

So a hardness result for the unweighted problem is a hardness result for the weighted one, at uniform probability 1/2.

@[instance_reducible]

def DescriptiveComplexity.unitWeightStructure {L : FirstOrder.Language} (A : Type) [(L.sum L).Structure A] [LinearOrder A] : (weightedLang L).Structure A

The weighted instance of an instance with certain and uncertain facts, over a linear order: every weight is 1, written as the single bit of the least position.

Equations

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

theorem DescriptiveComplexity.binNum_isBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : (binNum (fun (a b : A) => a ≤ b) (fun (x : A) => True) fun (i : A) => IsBot i) = 1

The number whose only bit is at the least position is 1.

theorem DescriptiveComplexity.weightedWorlds_unitWeight {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(L.sum L).Structure A] [LinearOrder A] [L.IsRelational] [Finite A] [Nonempty A] (φ : L.Sentence) : (WeightedWorlds φ).Count A = (PossibleWorlds φ).Count A

With every weight equal to one, counting weighted worlds is counting worlds.

The interpretation

@[reducible, inline]

abbrev DescriptiveComplexity.uwCert {L : FirstOrder.Language} {n : ℕ} (R : L.Relations n) : ((L.sum L).sum FirstOrder.Language.order).Relations n

The certain facts of a symbol, over the ordered expansion.

Equations

• DescriptiveComplexity.uwCert R = Sum.inl (Sum.inl R)

@[reducible, inline]

abbrev DescriptiveComplexity.uwUnc {L : FirstOrder.Language} {n : ℕ} (R : L.Relations n) : ((L.sum L).sum FirstOrder.Language.order).Relations n

The uncertain facts of a symbol, over the ordered expansion.

Equations

• DescriptiveComplexity.uwUnc R = Sum.inl (Sum.inr R)

@[reducible, inline]

abbrev DescriptiveComplexity.uwLe (L : FirstOrder.Language) : ((L.sum L).sum FirstOrder.Language.order).Relations 2

The order symbol of the ordered expansion.

Equations

• DescriptiveComplexity.uwLe L = Sum.inr FirstOrder.Language.leSymb

noncomputable def DescriptiveComplexity.unitWeightInterp (L : FirstOrder.Language) : FOInterpretation ((L.sum L).sum FirstOrder.Language.order) (weightedLang L) Unit 1

The weighted instance of weight one, drawn first-order from an ordered instance: the facts are kept, the order of the positions is the order of the instance, and the only bit of every weight is at the least element.

Equations

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

noncomputable def DescriptiveComplexity.unitWeightLEquiv {L : FirstOrder.Language} (A : Type) [(L.sum L).Structure A] [LinearOrder A] : (weightedLang L).Equiv ((unitWeightInterp L).Map A) A

The interpreted structure is the weighted instance of weight one.

Equations

• DescriptiveComplexity.unitWeightLEquiv A = { toEquiv := (DescriptiveComplexity.unitWeightInterp L).mapEquivSelf A, map_fun' := ⋯, map_rel' := ⋯ }

noncomputable def DescriptiveComplexity.possibleWorlds_ordered_parsimonious_weightedWorlds {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) : OrderedParsimoniousReduction (PossibleWorlds φ) (WeightedWorlds φ)

Counting possible worlds reduces parsimoniously to counting weighted worlds, by giving every fact the weights 1 and 1. The reduction is ordered: it names the least position.

Equations

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