Distribution Semantics: Logic Meets Probability

📍 Where we are: Part II · Probabilistic Logic and Circuits — Chapter 4. From Fuzzy to Neural closed Part I with truth as a differentiable degree attached to each formula; this chapter takes the other fork and attaches probability to whole worlds instead.

Part I ended with an honest bill. The fuzzy pipeline computes a truth degree for any formula in one cheap bottom-up pass, but the number it produces depends on which t-norm you chose, and nothing in the machinery tells you which choice is right. This chapter takes the road not taken. The logic stays completely crisp: the rules are exactly Volume 1's Horn rules, and inside any single situation every atom is plainly true or plainly false. The uncertainty moves to a different place: some facts are no longer certain, and each carries a probability of being true. The definition that turns this into a probability for every query is the distribution semantics [1], and it is the exactness anchor of this entire volume: every system in the chapters ahead, from compiled circuits to neural predicates, is ultimately judged by whether it reproduces or approximates the number this chapter defines. On the academic world everything is small enough to enumerate outright, which is precisely what makes the definition auditable before the next chapter runs into the computational wall.

The simple version

Imagine a detective's corkboard. Pins are facts, threads are rules of inference, and most pins are solid. But eleven of them are shaky: each has a sticky note reading "90% sure" or "55% sure". To answer "how likely is it that the conclusion holds?", the honest procedure is exhaustive: consider every possible way the shaky pins could turn out (each pin either holds or falls, so 2 × 2 × ⋯ × 2 = 2,048 scenarios), redo the ordinary crisp detective work inside each scenario as if it were settled fact, weigh each scenario by how likely that particular combination of pins was, and report the total weight of the scenarios where the conclusion follows. Nothing is ever "60% true" inside a scenario; every scenario is fully classical. The probability measures only your ignorance about which scenario you are in.

What this chapter covers

• The fork from Part I: what "truth-functional" means precisely, a two-line proof that probability is not truth-functional, and why that difference sets up the exactness-versus-tractability arc of this Part.
• The probabilistic program: eleven edges of the academic world become independent coins in distsem.py, while Volume 1's rules are imported untouched.
• The definition, formalized: total choices, world weights, and the success probability, with every symbol decoded and the independence assumption examined.
• Exact inference as honest brute force: the committed 2,048-world enumeration loop, the normalization proof, and a single-proof sanity check worked by hand next to the real output.
• The disjoint-sum problem, the chapter's centerpiece: a query with two overlapping proofs whose naive sum of proof products is 1.575, the overcount identified as exactly the doubly counted conjunction, and inclusion-exclusion recovering the enumerated 0.8865 to the committed 1e-12 tolerance.
• Monotonicity made runnable: a proof that adding a probabilistic fact can never lower a success probability, then the committed before/after table that executes it.
• The unsolved part: the independence of the coins is a modeling fiction, and the semantics offers no native way to learn the correlations it ignores.

Two ways to attach a number to logic

State the fork precisely before choosing a side. A semantics is truth-functional when the value of a compound formula is a fixed function of the values of its immediate parts, and of nothing else. Part I's fuzzy logic is truth-functional by construction: a valuation $v$ assigns each atom a degree in the interval $[0,1]$, and a conjunction is computed from its conjuncts, $v(\varphi \wedge \psi) = T(v(\varphi), v(\psi))$ for whichever t-norm $T$ was chosen, where $\varphi$ and $\psi$ stand for arbitrary formulas and the wedge $\wedge$ reads "and". Knowing the two input degrees is always enough; the formula's history, and how its parts relate to one another, never matters.

Probability refuses this. A probability attaches numbers not to formulas but to worlds, complete classical descriptions of how things could be, and a formula inherits its probability as the total weight of the worlds where it is classically true. Under that reading, the probability of a conjunction is provably not a function of the probabilities of its parts. The proof is a two-line counterexample. Let $\varphi$ be "a fair coin lands heads", so $P(\varphi) = 0.5$. First take $\psi = \varphi$: then $\varphi \wedge \psi$ is just $\varphi$, and $P(\varphi \wedge \psi) = 0.5$. Now instead take $\psi = \neg\varphi$ (the symbol $\neg$ reads "not"): then $P(\psi) = 0.5$ as well, but $\varphi \wedge \psi$ is a contradiction, true in no world, so $P(\varphi \wedge \psi) = 0$. The input pair of numbers is $(0.5, 0.5)$ in both cases, yet the output differs, so no function $T$ with $P(\varphi \wedge \psi) = T(P(\varphi), P(\psi))$ can exist.

What the two marginal numbers do pin down is an interval. Every world satisfying $\varphi \wedge \psi$ satisfies $\varphi$, so summing world weights gives $P(\varphi \wedge \psi) \le P(\varphi)$, and symmetrically $P(\varphi \wedge \psi) \le P(\psi)$; hence the conjunction is at most $\min(P(\varphi), P(\psi))$. For the floor, note that each world in a union of two events is counted once on the left of $P(\neg\varphi \vee \neg\psi) \le P(\neg\varphi) + P(\neg\psi)$ (the symbol $\vee$ reads "or": the union of the two events) but once or twice on the right, so the inequality holds. Two rewrites turn it into the bound. First, a world falsifies $\varphi \wedge \psi$ exactly when it falsifies $\varphi$ or falsifies $\psi$, so $\neg\varphi \vee \neg\psi$ names the same set of worlds as $\neg(\varphi \wedge \psi)$. Second, every world is counted exactly once between a formula and its negation, so $P(\chi) + P(\neg\chi) = 1$ for any formula $\chi$. Substituting $P(\neg\varphi) = 1 - P(\varphi)$, $P(\neg\psi) = 1 - P(\psi)$, and $P(\neg\varphi \vee \neg\psi) = 1 - P(\varphi \wedge \psi)$ turns the inequality into $1 - P(\varphi \wedge \psi) \le (1 - P(\varphi)) + (1 - P(\psi)) = 2 - P(\varphi) - P(\psi)$, and rearranging (add $P(\varphi \wedge \psi) - 2 + P(\varphi) + P(\psi)$ to both sides) yields $P(\varphi \wedge \psi) \ge P(\varphi) + P(\psi) - 1$. Where the true value falls inside that interval depends entirely on how the two events overlap in the space of worlds. That word, overlap, is the engine of this chapter: the disjoint-sum exhibit below is exactly what happens when an inference scheme forgets it.

The fork, then, is a trade:

	Part I: fuzzy	Part II: probabilistic
the number lives on	each formula	each world (total choice)
conjunction	computed, $T(a, b)$	not computable from the parts; depends on overlap
logic inside a valuation	many-valued	classical in every world
naive evaluation cost	one bottom-up pass	$2^n$ worlds, one per combination of the $n$ uncertain facts; a counting problem in general
meaning of the number	a degree, t-norm dependent	a probability, coherent by construction

The right column's meaning is exact and its cost is exponential; the left column's cost is linear and its meaning wavers. This Part of the volume is the story of paying the right column's price intelligently, and this chapter establishes what, precisely, is being paid for.

The probabilistic program: eleven coins on the academic world

The companion module distsem.py builds the volume's first probabilistic logic program directly on Volume 1's knowledge base. Its imports refuse to retype anything (distsem.py lines 58–59):

from kb import FACTS, RULES, is_var  # noqa: E402  (the academic world, Vol 1)
from forward_chain import least_fixpoint  # noqa: E402  (⊢ = the least fixpoint)

RULES is the untouched Volume 1 rule set (kb.py lines 73–89): researcher and person from professor and student, grandAdvisor as advises composed with advises, colleague from shared affiliation, and the transitive closure of citation. None of these rules acquires a number. What changes is the status of eleven of the twenty-three base facts (distsem.py lines 71–83):

PROB_FACTS: dict[tuple, float] = {
    ("advises", "alice", "bob"): 0.90,
    ("advises", "bob", "carol"): 0.90,
    ("advises", "bob", "dave"): 0.85,
    ("advises", "carol", "erin"): 0.90,
    ("cites", "p2", "p1"): 0.80,
    ("cites", "p3", "p2"): 0.90,
    ("authored", "alice", "p1"): 0.95,
    ("authored", "bob", "p1"): 0.90,
    ("authored", "carol", "p2"): 0.90,
    ("authored", "dave", "p3"): 0.85,
    ("affiliated", "erin", "cmu"): 0.55,
}

Read the numbers as what they are: noisy evidence. A departmental record saying alice advises bob is strong but not infallible, so the advising edges sit at 0.85 to 0.90. The citation chain carries exactly the confidences Volume 2's annotated reasoner attached to those same edges (0.9 and 0.8). One record is genuinely shaky: erin's affiliation, at 0.55, is barely better than a coin flip. Every other fact of kb.py, all the unary types, the remaining affiliations, the paper topics, stays certain, which the module encodes by leaving it out of PROB_FACTS (the certain remainder is collected at distsem.py line 86).

Two independent research lines arrived at the same reading of such a program. From the logic-programming side, each annotated fact is a random switch and the program defines a distribution over its own groundings [1]; from the agents side, the same object appears as the independent choice logic, where the annotated facts are independent choices made by nature and the crisp rules deterministically unfold each choice's consequences [2]. The notation p :: f is ProbLog's, and the eleven-coin program above is a ProbLog program in miniature [3]; the semantics itself had already been running in earlier systems, Sato and Kameya's PRISM (PRogramming In Statistical Modeling) first among them [4], for a decade before ProbLog named the construct this way.

Here is the whole semantics, decoded before any formula appears. Flip all eleven coins independently: coin $f$ comes up true with its probability $p_f$. The outcome selects a subset of the eleven facts, and that subset, together with the twelve certain facts, is a possible world: one fully classical situation. Inside that world, run the ordinary Volume 1 forward chainer to its least fixpoint; the world derives whatever it derives, crisply. The probability of a query is the total weight of the worlds in which it comes out derivable. That is the entire definition. Everything else in this chapter is bookkeeping done carefully.

The definition, formalized

Now the same definition in symbols, each decoded on arrival. Write $\mathcal{F}$ for the set of probabilistic facts (here the eleven keys of PROB_FACTS), and $n = \lvert\mathcal{F}\rvert$ for their number (the bars $\lvert\cdot\rvert$ denote the size of a set, so $n = 11$). Each fact $f \in \mathcal{F}$ (the symbol $\in$ reads "is an element of") carries a probability $p_f \in [0,1]$. Write $C$ for the certain facts (the twelve remaining kb.py facts) and $R$ for the rules. A total choice is a subset $F \subseteq \mathcal{F}$ (the symbol $\subseteq$ reads "is a subset of"): the set of coins that came up true. Independence makes the probability of a total choice a product, with one factor per coin:

$$P(F) \;=\; \prod_{f \in F} p_f \;\cdot \prod_{f \in \mathcal{F} \setminus F} (1 - p_f),$$

where $\prod$ is the product sign (multiply one factor for each listed element, as $\sum$ adds one term for each) and $\mathcal{F} \setminus F$ is the set difference, the coins not chosen. Each chosen coin contributes its probability $p_f$; each dropped coin contributes the probability $1 - p_f$ of coming up false.

These $2^n$ weights form a genuine probability distribution: they are non-negative, and they sum to one. The proof is a product expansion worth seeing once in full. Take $n = 2$ with coins $f_1, f_2$. The four total choices weigh

$$p_1 p_2 \;+\; p_1(1-p_2) \;+\; (1-p_1)p_2 \;+\; (1-p_1)(1-p_2),$$

and grouping the first pair and the second pair by their common factor gives

$$p_1\big(p_2 + (1-p_2)\big) + (1-p_1)\big(p_2 + (1-p_2)\big) \;=\; p_1 + (1 - p_1) \;=\; 1.$$

The same grouping works for any $n$: expanding the product $\prod_{f \in \mathcal{F}} \big(p_f + (1-p_f)\big)$ distributes into exactly one term per subset $F$, the term that picks $p_f$ for each $f \in F$ and $(1-p_f)$ for each $f \notin F$ (the symbol $\notin$ reads "is not an element of"), which is precisely $P(F)$. Therefore

$$\sum_{F \subseteq \mathcal{F}} P(F) \;=\; \prod_{f \in \mathcal{F}} \big(p_f + (1 - p_f)\big) \;=\; \prod_{f \in \mathcal{F}} 1 \;=\; 1 .$$

Two more symbols and the definition is complete. Write $F \cup C \cup R \vdash q$ for "the query $q$ is derivable from the chosen facts, the certain facts, and the rules": the symbol $\cup$ is the union, pooling those three sets into one fact-and-rule base, and the turnstile $\vdash$ reads "derives". In this volume, derivability is Volume 1's forward chainer: $q$ is derivable exactly when it belongs to the least fixpoint that least_fixpoint computes by firing rules until nothing new appears (forward_chain.py lines 52–63). The success probability of $q$ is then the total weight of the deriving worlds [1]:

$$P(q) \;=\; \sum_{F \subseteq \mathcal{F}\,:\; F \cup C \cup R \,\vdash\, q} P(F) \;=\; \sum_{F \subseteq \mathcal{F}} P(F)\cdot \mathbb{1}\!\left[F \cup C \cup R \vdash q\right],$$

where $\mathbb{1}[\cdot]$ is the indicator: the function that is $1$ when the bracketed statement holds and $0$ when it does not. The second form, probability as the expected value of an indicator over worlds, looks like a rewording; it will do real work in the disjoint-sum derivation below. Note what the definition is not: it is not a rule for combining subformula scores. $P(q)$ is a property of the whole program, computed through the worlds, and no local combination of the parts is guaranteed to reach it. That is the non-truth-functionality of the fork section, now built into a definition.

The load-bearing assumption is independence: the coins are flipped separately, so the probability of any combination of coin outcomes factors into the product above. This is a genuine modeling restriction. The language cannot directly say "these two advising records come from the same faulty database, so they fail together", nor "bob advises carol or dave, but not both": any such coupling is simply not expressible by independent coins alone. The standard escape hatch is the annotated disjunction, a construct that lets several alternative heads share a single choice, so that exactly one of them (or none) fires [5]; it, and the neural predicates that generalize it, belong to the DeepProbLog chapter. For now the program lives honestly inside independence, and the chapter examines what that buys.

The distribution semantics end to end: eleven independent coins over crisp rules, every total choice forward-chained to its fixpoint and weighed, and the disjoint-sum exhibit where naive proof summing overcounts by exactly the shared-coin overlap. Original diagram by the authors, created with AI assistance.

Exact inference as honest brute force

The definition quantifies over every subset of $\mathcal{F}$, and at academic-world scale the honest move is to do exactly that: materialize all $2^{11} = 2048$ total choices, forward-chain each one, and sum. The companion executes the definition literally (distsem.py lines 130–143):

    # Each integer 0 .. 2^n - 1 is one total choice: bit i decides coin i.
    for bits in range(1 << n):
        chosen: list[tuple] = []
        # P(F) = Π_{f ∈ F} p_f · Π_{f ∉ F} (1 − p_f)   (independent coins)
        p_world = 1.0
        for i in range(n):
            if bits >> i & 1:
                chosen.append(atoms[i])
                p_world *= probs[i]
            else:
                p_world *= 1.0 - probs[i]
        # model_F = lfp(T_{F ∪ C ∪ R}) — everything world F derives (Vol 1).
        model = least_fixpoint(certain + chosen, RULES)
        table.append((p_world, frozenset(model)))

Each integer from $0$ to $2^n - 1$ encodes one subset in binary: bit $i$ decides coin $i$, p_world accumulates the product $P(F)$ factor by factor, and least_fixpoint computes what that world derives. The resulting table of (weight, fixpoint) pairs is the distribution semantics written out, and the function guards its own exponential honesty with an assert refusing more than twelve coins (distsem.py line 125). A query's probability is then a filtered sum over the table (distsem.py lines 160–169), using math.fsum so the $2^n$-term addition is exactly rounded and the chapter's 1e-12 comparisons test the semantics, not float noise. One subtlety earns its own function: a query containing a variable, such as grandAdvisor(alice, Z) with the capital Z a logic variable, is an existential query, satisfied in a world when some derived atom unifies with it; holds implements that success criterion (distsem.py lines 149–157).

The committed run opens with the sanity checks the normalization proof promised:

[2] sanity: the 2048 world weights form a distribution
      Σ_F P(F)              = 1.000000000000   (must be exactly 1)
      P(professor(alice))   = 1.000000000000   (a certain fact holds in every world)

A certain fact holds in every world, so its success probability collects the entire unit of weight; an atom no world derives, like advises(erin, alice), collects none, and the module asserts both (distsem.py lines 233–236).

The first substantive theorem is the single-proof case. Suppose a query $q$ has exactly one proof, consuming the coins $f_1, \ldots, f_k$ (certain facts in the proof can be ignored, since they hold everywhere). Then $q$ is derivable in world $F$ exactly when all $k$ coins are in $F$, and both directions deserve a word. If all $k$ coins are in $F$, every fact the proof consumes is present, so each of its rule firings goes through and the fixpoint contains $q$; whatever other coins $F$ happens to contain cannot disable those firings, a special case of the monotonicity proved two sections below. Conversely, a world that derives $q$ supports at least one proof of $q$ built entirely from facts present in that world, and by assumption there is only one proof, so all $k$ of its coins must be in $F$. The success probability therefore splits into the coins the proof fixes and the coins it never mentions. Write $\mathcal{F}'$ for the unmentioned coins; every deriving world is the disjoint union of the fixed part and a free part $F' \subseteq \mathcal{F}'$, and the product $P(F)$ factors accordingly:

$$P(q) \;=\; \sum_{F' \subseteq \mathcal{F}'} \Big( \prod_{i=1}^{k} p_{f_i} \Big) \cdot P(F') \;=\; \Big( \prod_{i=1}^{k} p_{f_i} \Big) \cdot \sum_{F' \subseteq \mathcal{F}'} P(F') \;=\; \prod_{i=1}^{k} p_{f_i},$$

where the last step is the normalization identity applied to the unmentioned coins: their weights sum to $1$, so they marginalize away. Independence makes conjunction multiply, but only because the sum over everything irrelevant collapses. The committed run checks this on three queries whose proofs are unique:

[3] one-proof queries: P(q) = the product of the proof's coin probs
      query                          enumeration      product   |diff|
      grandAdvisor(alice, carol)     0.810000000000 = 0.90 · 0.90   0.0e+00
      citesTransitively(p3, p1)      0.720000000000 = 0.90 · 0.80   0.0e+00
      colleague(carol, erin)         0.550000000000 =        0.55   0.0e+00

Work the first by hand. The only proof of grandAdvisor(alice, carol) is the rule grandAdvisor(X, Z) ← advises(X, Y), advises(Y, Z) instantiated through bob (kb.py line 79), consuming the coins advises(alice, bob) at $0.90$ and advises(bob, carol) at $0.90$; the formula gives $0.90 \times 0.90 = 0.81$, and enumeration over all 2,048 worlds returns 0.810000000000 with zero discrepancy. The third row is quietly instructive: the colleague proof uses affiliated(carol, cmu), which is certain and contributes the factor $1$, and affiliated(erin, cmu), the shaky coin, so the product is just $0.55$.

The disjoint-sum problem

Everything so far suggests a tempting shortcut: find the proofs of a query, multiply each proof's coin probabilities, and add the products. For one proof the previous section proved this exact. For two proofs it is wrong, and the committed exhibit shows it failing as loudly as possible.

The existential query grandAdvisor(alice, Z), "alice is a grand-advisor of someone", has exactly two ground proofs under the program (distsem.py lines 207–209). Both descend through bob:

• Proof A, through carol: coins advises(alice, bob) and advises(bob, carol), product $0.90 \times 0.90 = 0.81$.
• Proof B, through dave: coins advises(alice, bob) and advises(bob, dave), product $0.90 \times 0.85 = 0.765$.

The naive sum of proof products is $0.81 + 0.765 = 1.575$. This exceeds $1$, so it is not merely inaccurate; it is not a probability at all. The diagnosis is the overlap the fork section warned about. Let $A$ be the event "all of proof A's coins came up true" and $B$ the event for proof B. The query succeeds on the union $A \vee B$, but the two events are far from disjoint: they share the coin advises(alice, bob), so the worlds where bob's whole advising record survives, and both proofs go through, are counted once inside $P(A)$ and once again inside $P(B)$.

The exact correction is inclusion-exclusion, and the indicator form of the definition makes its proof a four-row truth check. For any two events, the indicators satisfy

$$\mathbb{1}[A \vee B] \;=\; \mathbb{1}[A] + \mathbb{1}[B] - \mathbb{1}[A]\,\mathbb{1}[B],$$

verified case by case: if neither holds, both sides are $0$; if exactly one holds, both sides are $1 + 0 - 0 = 1$; if both hold, the right side is $1 + 1 - 1 = 1$, matching the left. Multiply both sides by the world weight $P(F)$, sum over all $F \subseteq \mathcal{F}$, and each indicator sum becomes a probability by the definition of $P(\cdot)$:

$$P(A \vee B) \;=\; P(A) + P(B) - P(A \wedge B).$$

Rearranged, $P(A) + P(B) - P(A \vee B) = P(A \wedge B)$: the naive sum overshoots the truth by exactly the probability that both proofs go through, the doubly counted region. Every quantity on that line is computable here. The conjunction $A \wedge B$ holds when every coin in the union of the two proofs' coin sets is true, with the shared coin counted once, so by the single-proof factorization applied to that three-coin set,

$$P(A \wedge B) \;=\; 0.90 \times 0.90 \times 0.85 \;=\; 0.6885,$$

and inclusion-exclusion predicts

$$P(A \vee B) \;=\; 0.81 + 0.765 - 0.6885 \;=\; 0.8865 .$$

The companion computes all three numbers and holds them against exact enumeration (distsem.py lines 248–262):

    p_a = proof_probability(DS_PROOF_A)          # 0.9 · 0.9  = 0.81
    p_b = proof_probability(DS_PROOF_B)          # 0.9 · 0.85 = 0.765
    naive = p_a + p_b                            # sum of proof products
    # P(A ∧ B) = Π over the UNION of the two proofs' coins — the shared coin
    # advises(alice, bob) is counted ONCE: 0.9 · 0.9 · 0.85 = 0.6885.
    p_both = proof_probability(sorted(set(DS_PROOF_A) | set(DS_PROOF_B)))
    # Inclusion–exclusion: P(A ∨ B) = P(A) + P(B) − P(A ∧ B).
    incl_excl = naive - p_both
    p_exact = P_query(DS_QUERY)
    assert naive > 1.0, "the exhibit needs the naive sum to exceed 1"
    assert naive - p_exact > 0.5, "naive sum should overcount by P(A ∧ B)"
    assert abs((naive - p_exact) - p_both) < TOL, (
        "the overcount must be exactly the doubly-counted P(A ∧ B)")
    assert abs(incl_excl - p_exact) < TOL, (
        f"inclusion-exclusion {incl_excl} != enumeration {p_exact}")

The committed output, with the enumeration agreeing far inside the 1e-12 tolerance the asserts demand:

[4] the disjoint-sum problem: grandAdvisor(alice, Z) has two proofs
    that SHARE the coin advises(alice, bob)
      proof A {advises(alice,bob), advises(bob,carol)}  product = 0.8100
      proof B {advises(alice,bob), advises(bob,dave)}   product = 0.7650
      naive sum of proof products   = 1.575000000000   <- exceeds 1: not a probability
      P(A ∧ B), shared coin ONCE    = 0.688500000000   = 0.90 · 0.90 · 0.85
      inclusion-exclusion           = 0.886500000000   = naive − P(A ∧ B)
      exact enumeration             = 0.886500000000   (agrees to 1.1e-16)

The general lesson deserves stating in full, because half of this volume answers to it. Proofs are not disjoint events. Any inference scheme that scores proofs independently and adds the scores silently assumes they are, and must answer for the overlap. With two proofs the repair is one subtracted term; with $m$ overlapping proofs (the letter $m$ counting proofs, leaving $k$ to the per-proof coin count above), inclusion-exclusion expands into $2^m - 1$ signed terms, one per non-empty subset of the $m$ proofs, and the repair itself goes exponential. The systematic resolution is to stop summing over proofs altogether and instead reduce the query to a weighted count over a propositional formula, where each world is counted exactly once no matter how many proofs it supports [6]. That reduction is the next chapter's subject, and this exhibit is the reason it exists.

Monotonicity, made runnable

The semantics inherits a structural theorem from the crisp logic underneath it: adding a probabilistic fact never lowers any success probability. The proof has two layers, one about derivability and one about weights.

The derivability layer is Volume 1's fixpoint, reread. The programs here are definite: every rule has one positive head and a body of positive atoms, with no negation over derived or base facts anywhere. For such programs the immediate-consequence operator is monotone in its fact set: any rule firing available from a smaller set of facts is still available from a larger one, since a body atom satisfied by membership in the smaller set is satisfied in the superset (forward_chain.py lines 42–49). One body atom is not a fact lookup: the colleague rule carries the built-in inequality guard neq(X, Y) (kb.py lines 82–83), and the engine's handling of it (forward_chain.py lines 30–34) succeeds exactly when its two ground arguments differ, a test that never consults the fact set, so its satisfaction is preserved verbatim when facts are added and the argument goes through unchanged. By induction on chaining rounds, every atom the smaller program derives by round $t$ (the round counter, a fresh letter since $k$ already counts a proof's coins above), the larger program also derives by round $t$. So for any two fact sets $F \subseteq G$, where $G$ is the larger set, the least fixpoints satisfy $F \subseteq G \Rightarrow \mathrm{lfp}(F \cup C \cup R) \subseteq \mathrm{lfp}(G \cup C \cup R)$ (the arrow $\Rightarrow$ reads "implies": whenever the left side holds, so does the right). Adding facts can only add conclusions.

The weight layer converts that into probabilities. Add a new coin $f_0$ with probability $p_0$ to the program. Every old total choice $F$ splits into exactly two new ones, $F$ itself with weight $(1 - p_0)\,P(F)$ and $F \cup \{f_0\}$ with weight $p_0\,P(F)$, and these two weights sum back to $P(F)$, so the new distribution refines the old one without moving mass around. Now compute the new success probability of any query $q$ by grouping the new worlds in those pairs:

$$P_{\text{new}}(q) \;=\; \sum_{F} P(F)\Big( (1 - p_0)\, \mathbb{1}[F \vdash q] \;+\; p_0\, \mathbb{1}[F \cup \{f_0\} \vdash q] \Big),$$

writing $F \vdash q$ as shorthand for derivability from $F \cup C \cup R$. By the derivability layer, $\mathbb{1}[F \cup \{f_0\} \vdash q] \ge \mathbb{1}[F \vdash q]$: the enlarged world derives everything the original did. Substituting that inequality termwise,

$$P_{\text{new}}(q) \;\ge\; \sum_{F} P(F)\Big( (1 - p_0) + p_0 \Big)\, \mathbb{1}[F \vdash q] \;=\; \sum_{F} P(F)\, \mathbb{1}[F \vdash q] \;=\; P_{\text{old}}(q).$$

No success probability can drop. The companion runs this theorem rather than trusting it (distsem.py lines 264–284): it adds the coin 0.5 :: cites(p3, p1), the same uncertain direct citation Volume 2's annotated reasoner carries at confidence 0.5, doubling the world count to $2^{12} = 4096$, and re-asks six queries (in the table, the Δ column is the change: after minus before):

query	before	after	Δ
citesTransitively(p3, p1)	0.720000000000	0.860000000000	+0.1400
citesTransitively(p2, p1)	0.800000000000	0.800000000000	+0.0000
grandAdvisor(alice, Z)	0.886500000000	0.886500000000	+0.0000
grandAdvisor(alice, carol)	0.810000000000	0.810000000000	+0.0000
colleague(carol, erin)	0.550000000000	0.550000000000	+0.0000
person(erin)	1.000000000000	1.000000000000	+0.0000

The pattern is exactly what the two proof layers predict. The five queries the new edge cannot reach are unchanged to twelve decimals (the module asserts invariance to the 1e-12 tolerance for one representative, grandAdvisor(alice, Z), at distsem.py lines 282–284, and non-decrease for all six at line 272). The one relevant query rises, and by a computable amount: citesTransitively(p3, p1) now has two proofs, the old chain through p2 consuming the coins at 0.9 and 0.8, and the new direct edge consuming only the fresh coin at 0.5. These two proofs share no coin, so the events "chain succeeds" and "direct edge succeeds" are independent, and independence lets the failure probabilities multiply: the query fails only if both proofs fail, so

$$P(\neg q) \;=\; (1 - 0.72)(1 - 0.5) \;=\; 0.28 \times 0.5 \;=\; 0.14, \qquad P(q) \;=\; 1 - 0.14 \;=\; 0.86 .$$

This is the noisy-or of the two proofs, the disjoint-coin special case where inclusion-exclusion simplifies to a complement product (substituting $P(A \wedge B) = P(A)P(B)$, which holds under independence, gives $P(A \vee B) = P(A) + P(B) - P(A)P(B)$, and that factors as $1 - (1-P(A))(1-P(B))$; expand the product to check). The committed run confirms both digits and structure:

      relevant ct(p3,p1) rises as the noisy-or of its two now-disjoint
      proofs: 1 − (1 − 0.72)(1 − 0.50) = 0.860000000000 = 0.860000000000

Monotonicity is a sanity theorem, but also a preview of a limitation: a definite probabilistic program can only accumulate belief, never retract it, so evidence against a conclusion has no way in. Negation can be added to the language, at the price of a considerably more delicate account of what a world derives; this volume stays with the definite core, where the theorem is clean and the reasoner is Volume 1's unchanged.

What the semantics buys, and what it defers

Tally the trade the fork section promised. On the credit side, the number $P(q)$ has a meaning fixed before any algorithm runs: it is the weight of the worlds that derive $q$, under a distribution the modeler stated fact by fact. It is probabilistically coherent by construction (the weights are non-negative and sum to one, certain conclusions get probability one, impossible ones zero), it is monotone where the logic is, and inside every world the logic is exactly classical, so no t-norm choice can bend the answer. Where Part I had to ask "which fuzzy conjunction, and what does 0.72 even mean?", this chapter's 0.8865 admits one reading: under the stated evidence model, the worlds where alice grand-advises someone carry 88.65% of the weight. The debit side is the wall this chapter kept meeting politely: the definition sums over $2^n$ worlds, each requiring a full forward-chaining pass, and the enumeration that is a 2,048-row table here is beyond all physical computation at real knowledge-base scale. Two deferrals are therefore scheduled. The tractability deferral reduces the query to a weighted count over a propositional formula, so shared structure among proofs is handled once instead of exponentially often [6]; it is the next chapter's subject. The expressiveness deferral, annotated disjunctions and neural predicates that let a network supply the coin probabilities, is the DeepProbLog chapter's.

The unsolved part

The independence assumption is doing enormous, quiet work, and it is a modeling fiction. Two advising records about the same professor are not independent in reality: if bob's departmental records are badly kept, advises(bob, carol) and advises(bob, dave) are suspect together, and confirming one should raise confidence in the other. The distribution semantics cannot say so directly; its coins fail one at a time, by fiat. The standard workaround is to hand-engineer latent structure: introduce an auxiliary probabilistic fact such as reliable(bob) and route both advising edges through rules that consult it, so the correlation flows through shared ancestry in the program. That works, but notice who did the thinking: the modeler chose the latent fact, its probability, and its wiring. The semantics offers no native way to learn that correlation structure from data. The differentiable rule learners later in this volume push on the learning half of this problem, recovering rules and probabilities from examples; even there, choosing what hidden common causes exist remains a modeling act, not an inference. The academic world's eleven coins keep the fiction visible and harmless; at knowledge-base scale, wrongly assumed independence silently miscalibrates every query that touches correlated evidence, and no committed assert in this chapter can catch it.

Why it matters

This chapter is the volume's exactness anchor in a literal, executable sense: distsem.py is the oracle later modules must match. The next chapter's weighted model counter is accepted only because it reproduces these enumerated numbers by circuit evaluation; the gradient semiring that trains DeepProbLog's neural predicates differentiates through the same semantics; Scallop's provenance framework relaxes it knowingly and is judged by how far it drifts. Fix the meaning first, in a form small enough to audit, then let every scalable approximation answer to it. The disjoint-sum exhibit is also the volume's first demonstration that a plausible-looking shortcut can be semantically wrong, not just imprecise: scoring proofs independently and adding is off by 0.6885 here, an error no training data repairs because it misdefines the quantity being computed. And for Volume 5's concerns, the chapter separates two properties its trust and calibration probes must not conflate: coherence (weights summing to one, certain conclusions at probability one) is automatic under this semantics, while calibration in the empirical sense (predicted probabilities matching observed frequencies) holds only insofar as the eleven stated coin probabilities are themselves right, which nothing here checks; Volume 5's probes measure exactly the gap between the two.

Key terms

• Distribution semantics: independent probabilistic facts induce a distribution over total choices; a query's probability is the total weight of the choices that derive it.
• Probabilistic fact ($p :: f$): a fact treated as an independent coin, true with probability $p$; the eleven annotated edges of PROB_FACTS.
• Total choice / possible world: a subset $F \subseteq \mathcal{F}$ of the probabilistic facts, weighted $P(F) = \prod_{f \in F} p_f \prod_{f \notin F} (1 - p_f)$; with the certain facts and rules, one fully classical situation.
• Success probability $P(q)$: $\sum_{F : F \cup C \cup R \vdash q} P(F)$, with derivability decided by Volume 1's forward chainer.
• Truth-functional: a semantics where a compound's value is a fixed function of its parts' values; fuzzy logic is, probability provably is not.
• Disjoint-sum problem: proofs are overlapping events, so summing per-proof products overcounts their conjunction; here 1.575 versus the true 0.8865.
• Inclusion-exclusion: $P(A \vee B) = P(A) + P(B) - P(A \wedge B)$, the exact two-proof repair, exponential in the number of overlapping proofs.
• Monotonicity: for definite programs, adding a probabilistic fact never lowers any success probability.
• Noisy-or: the rule $1 - \prod_i (1 - P_i)$, where $P_i$ is the $i$-th proof's coin product, for proofs with pairwise disjoint coin sets; independence makes the failures multiply.
• Annotated disjunction: the escape from pure independence, letting several alternative heads share one probabilistic choice; deferred to the DeepProbLog chapter.

Where this leads

The definition is now exact, audited, and exponential. Every number in this chapter came from at most a few thousand forward-chaining passes (2,048 worlds, plus 4,096 more for the twelve-coin monotonicity probe) that a laptop finishes in seconds, and none of it survives contact with a knowledge base of ten thousand uncertain edges. The escape route was visible in the disjoint-sum exhibit: stop enumerating worlds and stop summing proofs; instead, compile the query's dependence on the coins into a propositional formula and compute a weighted count of that formula's satisfying assignments, so each world is counted once by construction. That reduction, what it costs, and the precise sense in which counting is harder than deciding, is the subject of the next chapter, Weighted Model Counting: The #P Wall.

---

Companion code: examples/integration/distsem.py executes the distribution semantics literally on the academic world, enumerating all 2,048 worlds with Volume 1's kb.py and forward_chain.py imported unchanged; its asserts guard every identity in this chapter (normalization, the single-proof products, the disjoint-sum inclusion-exclusion to 1e-12, monotonicity, and the noisy-or). Run python3 examples/integration/distsem.py to reproduce every number quoted above.