Counting weighted possible worlds

DescriptiveComplexity.Counting.PossibleWorlds counts the possible worlds of an instance with certain and uncertain facts, each uncertain fact being present with probability 1/2. Here every uncertain fact carries its own probability, as two natural weights: a for its being present and c for its being absent, the probability being a / (a + c). The quantity counted is the weighted number of worlds in which a sentence φ of the schema holds,

W(φ) = ∑ over the worlds satisfying φ of ∏ over the open facts of their weight,

and the probability of φ is W(φ) / W(⊤) (DescriptiveComplexity.ProbAssignment.funcProb_ofWeights).

The instances

DescriptiveComplexity.weightedLang L: for each symbol of the schema L, of arity n, the certain facts and the uncertain ones, and two relations of arity n + 1 holding the bits of the two weights of each fact; and one order relation on the bit positions, which are all the elements. Weights are in binary: the encoding in which a probability of a database is honestly written, and the one for which membership is the stronger statement.

Why this is in #P

A weight multiplies a count, and a count cannot be multiplied by a number of the instance directly. The witness therefore carries, beside the world, one number per open fact, below the weight that fact takes in the world: each world is then counted once per unit of the product of its weights. “Below” is first-order, by the highest position at which two binary numbers differ (DescriptiveComplexity.numLtFormula, generic in the arity of the fact), and the numbers below a weight are as many as the weight (DescriptiveComplexity.card_binNum_lt).

• DescriptiveComplexity.WeightedWorlds φ is the witness count of that kernel, hence in #P for every first-order φ (DescriptiveComplexity.weightedWorlds_mem_sharpP).
• DescriptiveComplexity.weightedWorlds_eq_weightSum: on an instance whose order is linear, it is the weighted number of worlds. The proof sorts the witnesses by world (DescriptiveComplexity.weightedWorlds_eq_sum), then counts the numbers allowed at each fact (DescriptiveComplexity.card_numCond).
• On an instance whose order relation is not linear the count is zero (DescriptiveComplexity.weightedWorlds_of_not_isLinOrd): the kernel asks for linearity, such an instance carrying no number.

The probability

The open facts of an instance are independent Boolean variables, and a world is a valuation of them (DescriptiveComplexity.worldOfVal). So the count is a weighted count in the sense of DescriptiveComplexity.Counting.Probability (DescriptiveComplexity.weightedWorlds_eq_weightedCount), and

Pr(φ) = WeightedWorlds φ / WeightedWorlds ⊤

(DescriptiveComplexity.funcProb_holdsEvent_eq_ratio): the probability of any first-order query over a tuple-independent database is a ratio of two #P numbers.

The vocabulary

inductive DescriptiveComplexity.WeightedRel (L : FirstOrder.Language) : ℕ → Type

The relation symbols of a weighted instance over the schema L: for each symbol of the schema, the certain facts, the uncertain facts, and the bits of the two weights of each fact; and one order, on the bit positions.

• cert {L : FirstOrder.Language} {n : ℕ} (R : L.Relations n) : WeightedRel L n

  The certain facts.

• unc {L : FirstOrder.Language} {n : ℕ} (R : L.Relations n) : WeightedRel L n

  The uncertain facts.

• pres {L : FirstOrder.Language} {n : ℕ} (R : L.Relations n) : WeightedRel L (n + 1)

  pres R (x̄, i): the bit of position i of the weight of the fact R(x̄) being present.

• abs {L : FirstOrder.Language} {n : ℕ} (R : L.Relations n) : WeightedRel L (n + 1)

  abs R (x̄, i): the bit of position i of the weight of the fact R(x̄) being absent.

• le {L : FirstOrder.Language} : WeightedRel L 2

  The order of the bit positions.

def DescriptiveComplexity.weightedLang (L : FirstOrder.Language) : FirstOrder.Language

The vocabulary of weighted instances over the schema L.

Equations

• DescriptiveComplexity.weightedLang L = { Functions := fun (x : ℕ) => Empty, Relations := DescriptiveComplexity.WeightedRel L }

instance DescriptiveComplexity.instIsRelationalWeightedLang (L : FirstOrder.Language) : (weightedLang L).IsRelational

def DescriptiveComplexity.weightBlock (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] : SOBlock

The block guessing a weighted world: a world, and for each fact a number, as the set of its bits.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.weightKernelLang (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] : FirstOrder.Language

The vocabulary of the kernel.

Equations

• DescriptiveComplexity.weightKernelLang L = (DescriptiveComplexity.weightedLang L).sum (DescriptiveComplexity.weightBlock L).lang

@[reducible, inline]

abbrev DescriptiveComplexity.wkCert {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (weightKernelLang L).Relations p.fst

The certain facts of a symbol, in the kernel vocabulary.

Equations

• DescriptiveComplexity.wkCert p = Sum.inl (DescriptiveComplexity.WeightedRel.cert p.snd)

@[reducible, inline]

abbrev DescriptiveComplexity.wkUnc {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (weightKernelLang L).Relations p.fst

The uncertain facts of a symbol, in the kernel vocabulary.

Equations

• DescriptiveComplexity.wkUnc p = Sum.inl (DescriptiveComplexity.WeightedRel.unc p.snd)

@[reducible, inline]

abbrev DescriptiveComplexity.wkPres {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (weightKernelLang L).Relations (p.fst + 1)

The bits of the weight of presence, in the kernel vocabulary.

Equations

• DescriptiveComplexity.wkPres p = Sum.inl (DescriptiveComplexity.WeightedRel.pres p.snd)

@[reducible, inline]

abbrev DescriptiveComplexity.wkAbs {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (weightKernelLang L).Relations (p.fst + 1)

The bits of the weight of absence, in the kernel vocabulary.

Equations

• DescriptiveComplexity.wkAbs p = Sum.inl (DescriptiveComplexity.WeightedRel.abs p.snd)

@[reducible, inline]

abbrev DescriptiveComplexity.wkWorld {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (weightKernelLang L).Relations p.fst

The guessed world, in the kernel vocabulary.

Equations

• DescriptiveComplexity.wkWorld p = Sum.inr ⟨Sum.inl p, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.wkNum {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (weightKernelLang L).Relations (p.fst + 1)

The guessed numbers, in the kernel vocabulary.

Equations

• DescriptiveComplexity.wkNum p = Sum.inr ⟨Sum.inr p, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.wkLe (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] : (weightKernelLang L).Relations 2

The order of the positions, in the kernel vocabulary.

Equations

• DescriptiveComplexity.wkLe L = Sum.inl DescriptiveComplexity.WeightedRel.le

Atoms about a fact and a position

def DescriptiveComplexity.factAtom {L' : FirstOrder.Language} {α : Type} {n : ℕ} (S : L'.Relations n) (e : Fin n → α) : L'.Formula α

The atom S(x̄), the tuple being read off the free variables through e.

Equations

• DescriptiveComplexity.factAtom S e = S.formula fun (m : Fin n) => FirstOrder.Language.var (e m)

def DescriptiveComplexity.bitAtom {L' : FirstOrder.Language} {α : Type} {n : ℕ} (S : L'.Relations (n + 1)) (e : Fin n → α) (i : α) : L'.Formula α

The atom S(x̄, i): a fact and a position.

Equations

• DescriptiveComplexity.bitAtom S e i = S.formula (Fin.snoc (fun (m : Fin n) => FirstOrder.Language.var (e m)) (FirstOrder.Language.var i))

Comparing two numbers attached to a fact

noncomputable def DescriptiveComplexity.numLtFormula {L' : FirstOrder.Language} {n : ℕ} (N W : L'.Relations (n + 1)) (Le : L'.Relations 2) : L'.Formula (Fin n)

“The number N(x̄, ·) is below the number W(x̄, ·)”, by the highest position at which they differ: some position carries 1 in W and 0 in N, and the two agree strictly above it.

Equations

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

noncomputable def DescriptiveComplexity.linOrdSentence {L' : FirstOrder.Language} (Le : L'.Relations 2) : L'.Sentence

“The relation Le is a linear order”, as a sentence.

Equations

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

noncomputable def DescriptiveComplexity.numZeroFormula {L' : FirstOrder.Language} {n : ℕ} (N : L'.Relations (n + 1)) : L'.Formula (Fin n)

“The number N(x̄, ·) is zero”: it has no bit.

Equations

• DescriptiveComplexity.numZeroFormula N = FirstOrder.Language.Formula.iAlls Unit (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.bitAtom N Sum.inl (Sum.inr ())))

theorem DescriptiveComplexity.realize_linOrdSentence {L' : FirstOrder.Language} (Le : L'.Relations 2) {M : Type} [L'.Structure M] : M ⊨ linOrdSentence Le ↔ IsLinOrd fun (a b : M) => FirstOrder.Language.Structure.RelMap Le ![a, b]

The kernel

def DescriptiveComplexity.worldOf {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} (σ : (weightBlock L).Assignment A) : (worldBlock L).Assignment A

The world of an assignment of the block.

Equations

• DescriptiveComplexity.worldOf σ p x = σ (Sum.inl p) x

def DescriptiveComplexity.numOf {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} (σ : (weightBlock L).Assignment A) (p : (n : ℕ) × L.Relations n) (x : Fin p.fst → A) : A → Prop

The number an assignment of the block attaches to a fact, as its set of bits.

Equations

• DescriptiveComplexity.numOf σ p x i = σ (Sum.inr p) (Fin.snoc x i)

def DescriptiveComplexity.bitsOf {L : FirstOrder.Language} {A : Type} [(weightedLang L).Structure A] {n : ℕ} (S : WeightedRel L (n + 1)) (x : Fin n → A) : A → Prop

The bits of a weight of a fact, read through a symbol of arity one more than the fact's.

Equations

• DescriptiveComplexity.bitsOf S x i = FirstOrder.Language.Structure.RelMap S (Fin.snoc x i)

def DescriptiveComplexity.WLe (L : FirstOrder.Language) (A : Type) [(weightedLang L).Structure A] (a b : A) : Prop

The order of the positions of a weighted instance.

Equations

• DescriptiveComplexity.WLe L A a b = FirstOrder.Language.Structure.RelMap DescriptiveComplexity.WeightedRel.le ![a, b]

def DescriptiveComplexity.BitLt {A : Type} (Le : A → A → Prop) (b w : A → Prop) : Prop

One set of bits is below another, by the highest position at which they differ.

Equations

• DescriptiveComplexity.BitLt Le b w = ∃ (i : A), w i ∧ ¬b i ∧ ∀ (j : A), Le i j → j ≠ i → (b j ↔ w j)

def DescriptiveComplexity.WeightCond {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] (σ : (weightBlock L).Assignment A) (p : (n : ℕ) × L.Relations n) (x : Fin p.fst → A) : Prop

What the kernel asks of an assignment at one fact: the world keeps a certain fact and contains only certain or uncertain ones; at an open fact – uncertain and not certain – the number is below the weight of presence if the world keeps the fact, and below the weight of absence if not; at any other fact the number is zero.

Equations

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

noncomputable def DescriptiveComplexity.weightFormulaAt {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (weightKernelLang L).Formula (Fin p.fst)

The condition of the kernel at one fact, as a formula in the fact.

Equations

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

noncomputable def DescriptiveComplexity.weightSentence (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] : (weightKernelLang L).Sentence

The sentence asking the condition of the kernel at every fact.

Equations

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

def DescriptiveComplexity.toWeightWorld (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] : L →ᴸ weightKernelLang L

Reading a sentence of the schema in the guessed world.

Equations

• DescriptiveComplexity.toWeightWorld L = { onFunction := fun {x : ℕ} (f : L.Functions x) => isEmptyElim f, onRelation := fun {n : ℕ} (R : L.Relations n) => DescriptiveComplexity.wkWorld ⟨n, R⟩ }

noncomputable def DescriptiveComplexity.weightKernel {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) : (weightKernelLang L).Sentence

The kernel: the positions are linearly ordered, the condition holds at every fact, and the sentence holds in the world.

Equations

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

The counting problem

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

Counting weighted possible worlds: the witnesses are the worlds in which the sentence φ holds, each with one number per open fact below the weight that fact takes in the world. On an instance whose positions are linearly ordered this is the weighted count of the worlds satisfying φ, and on any other instance it is zero.

Equations

• DescriptiveComplexity.WeightedWorlds φ = DescriptiveComplexity.CountingProblem.ofKernel (DescriptiveComplexity.weightBlock L) (DescriptiveComplexity.weightKernel φ)

theorem DescriptiveComplexity.weightedWorlds_apply {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) (A : Type) [(weightedLang L).Structure A] : (WeightedWorlds φ).Count A = Nat.card { σ : (weightBlock L).Assignment A // IsLinOrd (WLe L A) ∧ (∀ (p : (n : ℕ) × L.Relations n) (x : Fin p.fst → A), WeightCond σ p x) ∧ A ⊨ φ }

theorem DescriptiveComplexity.weightedWorlds_of_not_isLinOrd {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) (A : Type) [(weightedLang L).Structure A] (h : ¬IsLinOrd (WLe L A)) : (WeightedWorlds φ).Count A = 0

On an instance whose positions are not linearly ordered, the count is zero: such an instance carries no number. Registered in the Lax archive as Lax794877.ProbabilityRatio.weightedWorlds_of_not_isLinOrd.

theorem DescriptiveComplexity.weightedWorlds_mem_sharpP {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) : SharpP.Mem (WeightedWorlds φ)

Counting the weighted worlds of a first-order sentence is in #P, whatever the sentence. Registered in the Lax archive as Lax794877.WorldsInSharpP.weightedWorlds_mem_sharpP.

The count

@[reducible, inline]

abbrev DescriptiveComplexity.Fact (L : FirstOrder.Language) (A : Type) : Type

The facts over a universe: a symbol of the schema and a tuple.

Equations

• DescriptiveComplexity.Fact L A = ((p : (n : ℕ) × L.Relations n) × (Fin p.fst → A))

def DescriptiveComplexity.IsOpen {L : FirstOrder.Language} {A : Type} [(weightedLang L).Structure A] (q : Fact L A) : Prop

The fact is open: uncertain and not certain.

Equations

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

def DescriptiveComplexity.IsWeightedWorld {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] (ρ : (worldBlock L).Assignment A) : Prop

The family of relations is a possible world of the weighted instance.

Equations

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

def DescriptiveComplexity.NumCond {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] (ρ : (worldBlock L).Assignment A) (q : Fact L A) (b : A → Prop) : Prop

What the kernel asks of the number attached to a fact, in a world.

Equations

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

def DescriptiveComplexity.weightAssignEquiv (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] (A : Type) : (weightBlock L).Assignment A ≃ (worldBlock L).Assignment A × (Fact L A → A → Prop)

An assignment of the block is a world and a number per fact.

Equations

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

theorem DescriptiveComplexity.weightedWorlds_eq_sum {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] [Finite A] (hlin : IsLinOrd (WLe L A)) (φ : L.Sentence) : (WeightedWorlds φ).Count A = ∑ᶠ (ρ : { ρ : (worldBlock L).Assignment A // IsWeightedWorld ρ ∧ A ⊨ φ }), ∏ᶠ (q : Fact L A), Nat.card { b : A → Prop // NumCond (↑ρ) q b }

The witnesses, sorted by world: the count is the sum, over the worlds satisfying the sentence, of the product over the facts of the number of numbers the kernel allows there.

noncomputable def DescriptiveComplexity.factWeight {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] (ρ : (worldBlock L).Assignment A) (q : Fact L A) : ℕ

The weight of a fact in a world: the weight of presence of an open fact the world keeps, the weight of absence of an open fact it drops, and 1 for a fact that is not open. Weights are read in binary on the order of the instance.

Equations

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

theorem DescriptiveComplexity.card_numCond {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] [Finite A] (hlin : IsLinOrd (WLe L A)) (ρ : (worldBlock L).Assignment A) (q : Fact L A) : Nat.card { b : A → Prop // NumCond ρ q b } = factWeight ρ q

The numbers the kernel allows at a fact are as many as its weight.

theorem DescriptiveComplexity.weightedWorlds_eq_weightSum {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] [Finite A] (hlin : IsLinOrd (WLe L A)) (φ : L.Sentence) : (WeightedWorlds φ).Count A = ∑ᶠ (ρ : { ρ : (worldBlock L).Assignment A // IsWeightedWorld ρ ∧ A ⊨ φ }), ∏ᶠ (q : Fact L A), factWeight (↑ρ) q

The count is the weighted number of worlds: on an instance whose positions are linearly ordered, the count is the sum, over the possible worlds in which the sentence holds, of the product of the weights of the facts.

Worlds as valuations of the open facts

@[instance_reducible]

noncomputable instance DescriptiveComplexity.openFactFintype {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] [Finite A] : Fintype { q : Fact L A // IsOpen q }

The open facts of a finite instance, as a finite type: the independent Boolean variables of the instance.

Equations

• DescriptiveComplexity.openFactFintype = Fintype.ofFinite { q : DescriptiveComplexity.Fact L A // DescriptiveComplexity.IsOpen q }

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

The weight of presence of an open fact.

Equations

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

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

The weight of absence of an open fact.

Equations

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

def DescriptiveComplexity.worldOfVal {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] (v : { q : Fact L A // IsOpen q } → Bool) : (worldBlock L).Assignment A

The world of a valuation of the open facts: the certain facts, and the open facts the valuation makes true.

Equations

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

noncomputable def DescriptiveComplexity.holdsEvent {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] (φ : L.Sentence) (v : { q : Fact L A // IsOpen q } → Bool) : Bool

The event “the sentence holds in the world”, as a Boolean function of the valuation of the open facts.

Equations

• DescriptiveComplexity.holdsEvent φ v = decide (A ⊨ φ)

theorem DescriptiveComplexity.isWeightedWorld_worldOfVal {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(weightedLang L).Structure A] (v : { q : Fact L A // IsOpen q } → Bool) : IsWeightedWorld (worldOfVal v)

theorem DescriptiveComplexity.weightedWorlds_eq_weightedCount {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] [Finite A] (hlin : IsLinOrd (WLe L A)) (φ : L.Sentence) : (WeightedWorlds φ).Count A = weightedCount presWeight absWeight (holdsEvent φ)

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

theorem DescriptiveComplexity.funcProb_holdsEvent_eq_ratio {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] [Finite A] (hlin : IsLinOrd (WLe L A)) (hpos : ∀ (x : { q : Fact L A // IsOpen q }), 0 < presWeight x + absWeight x) (φ : L.Sentence) : (ProbAssignment.ofWeights presWeight absWeight hpos).funcProb (holdsEvent φ) = ↑((WeightedWorlds φ).Count A) / ↑((WeightedWorlds ⊤).Count A)

The probability of a first-order sentence is a ratio of two #P numbers. Over a weighted instance whose positions are linearly ordered, let each open fact be present independently, with probability its weight of presence over the sum of its two weights. Then the probability that φ holds is the count of the weighted worlds of φ, divided by the count of all the weighted worlds; and both counting problems are in #P (DescriptiveComplexity.weightedWorlds_mem_sharpP).

noncomputable def DescriptiveComplexity.worldProb {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] [Finite A] (φ : L.Sentence) (hpos : ∀ (x : { q : Fact L A // IsOpen q }), 0 < presWeight x + absWeight x) : ℚ

The probability of a sentence over a weighted instance: each open fact is present independently, with probability its weight of presence over the sum of its two weights, and the probability is that of the event that the sentence holds in the resulting world.

Equations

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

theorem DescriptiveComplexity.worldProb_eq_ratio {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] {A : Type} [(weightedLang L).Structure A] [Finite A] (hlin : IsLinOrd (WLe L A)) (φ : L.Sentence) (hpos : ∀ (x : { q : Fact L A // IsOpen q }), 0 < presWeight x + absWeight x) : worldProb φ hpos = ↑((WeightedWorlds φ).Count A) / ↑((WeightedWorlds ⊤).Count A)

The probability of a first-order sentence is a ratio of two #P numbers: DescriptiveComplexity.funcProb_holdsEvent_eq_ratio, for the packaged probability. Registered in the Lax archive as Lax794877.ProbabilityRatio.worldProb_eq_ratio.