Inference and Proof: Chaining Facts into Conclusions

📍 Where we are: Part II · Reasoning as Computation — Chapter 5. First-Order Logic told us what it means for a sentence to be true in a world, and checked it by walking every individual with holds(); now we turn from meaning to mechanism and let a machine derive new facts instead of merely testing old ones.

The previous chapter left us with a working but oddly passive picture of truth: hand a reasoner a finished world and a sentence, and it grinds through every individual to report yes or no. That is checking, and it presumes the world is already complete. Real reasoning does the opposite. It grows the world, taking a handful of asserted facts and a set of rules and manufacturing every conclusion those rules force. This chapter makes one claim precise, then proves it: reasoning is mechanical rule-application, and the trail of rule firings that produced a fact is its proof. We will not treat "derive the consequences" as a black box. We will define the one primitive that matches a rule to the facts, define the one operator that does the deriving, watch both move on the running example fact by fact, and prove that what they compute is neither too little (nothing entailed is missed) nor too much (nothing false slips in).

The simple version

Imagine a room full of dominoes, each one labeled with a rule like "if someone is a student, they are a researcher." A domino tips over the moment all the facts it is waiting for are standing. You tip the first few by hand, the facts you were simply told, and then you just watch: each falling domino knocks over the next, wave after wave, until the room goes still and nothing else can fall. Two things come out of this. You have discovered every conclusion the rules allow. And for any fact you like, you can trace backward the exact chain of dominoes that knocked it over, and that chain is a proof.

What this chapter covers

• The inference rule as reasoning's atom: modus ponens, decoded symbol by symbol, and why a proof is nothing more than a finite chain of rule applications.
• Unification, derived and traced: the substitution, the walk that resolves a binding chain, and the argument-by-argument unify that decides whether a rule body matches the facts, run step by step on a real match and a real clash.
• Forward chaining, formalized: the immediate-consequence operator $T_P$ written as a set equation, matched line by line to the real t_p, and its two structural properties (monotone, inflationary) proved from that definition.
• Why the loop must stop: the finite Herbrand base counted exactly for our world (1404 possible atoms), giving a hard bound on the number of sweeps.
• A worked sweep and three proof trees: one full application of $T_P$ traced substitution by substitution, then person(erin), a grand-advisor, and a transitive citation built as genuine derivations.
• The waves are proof depth: rereading the size trace [23, 41, 47, 47] as "one more inference step per wave," with every atom of every wave accounted for.
• Soundness and completeness, proved: an induction shows forward chaining derives only entailed facts; a model-theoretic argument shows it derives all of them, which is exactly why the derived model can be trusted.
• Two directions of proof and a forward pointer to the Fixpoints chapter, where this iterate-to-a-limit engine gets its full mathematical treatment.

The inference rule: reasoning's smallest move

The atom of reasoning is the inference rule: a licensed move from premises you already hold to a conclusion you may now add. The oldest and most important is modus ponens (Latin for "the mode that affirms"): from a fact $P$ and a rule $P \to Q$, you may conclude $Q$ [1]. Two operators appear here and both deserve decoding before we lean on them. The arrow $\to$ is material implication, read "if the left holds, then the right holds"; the sentence $P \to Q$ is a single claim about how $P$ and $Q$ are linked, not an instruction to do anything. Modus ponens is the instruction: it says that once you also possess the left-hand fact $P$ standing on its own, you have earned the right-hand fact $Q$. In one line, with the horizontal bar read as "from the things above, conclude the thing below":

$$\frac{P \qquad P \to Q}{Q}.$$

Our academic world runs on exactly this move. Among its rules in kb.py (lines 76 and 77) is one saying a student is a researcher, and another saying a researcher is a person:

(("researcher", "X"), [("student", "X")]),
(("person", "X"), [("researcher", "X")]),

Here X is a variable (uppercase, by the convention the running example fixes in is_var, kb.py lines 25–28: a term is a variable exactly when it is a non-empty string starting with a capital letter). Each rule is a Horn rule: a single positive head atom on the left and a conjunction of positive body atoms on the right, read "head holds if every body atom holds." The symbol $\land$ that joins body atoms is conjunction, plain "and": $b_1 \land b_2$ is true exactly when both $b_1$ and $b_2$ are true. A fact is just the special case of a Horn rule with an empty body: nothing has to hold first, so it holds unconditionally. To fire a rule we need a substitution: a mapping of its variables to constants that makes the body match facts we already have. We will write a substitution as the Greek letter $\sigma$ (sigma), and write $b\sigma$ for "the atom $b$ with $\sigma$ applied to its variables." Given the base fact student(erin), the substitution $\sigma = \{X \mapsto \text{erin}\}$ (the maplet $\mapsto$ reads "is sent to") turns the first rule's body student(X) into student(erin), which we hold, so modus ponens hands us researcher(erin). Finding that $\sigma$ mechanically is the job of a routine called unify, which we build in full in the next section.

A proof (or derivation) is then a finite sequence of atoms $A_1, A_2, \ldots, A_m$ in which every atom is either a base fact or the head $h\sigma$ of some rule $h \leftarrow b_1, \ldots, b_k$ whose body atoms $b_1\sigma, \ldots, b_k\sigma$ all appear earlier in the sequence. The rule arrow $\leftarrow$ is the same implication written conclusion-first, pointing from the head back to the conditions it rests on. The last atom $A_m$ is the thing proved; the whole sequence is the evidence. Nothing about this is creative. It is bookkeeping a machine can do without judgment, and that mechanical quality is the entire point of the chapter.

Unification: the primitive that matches a rule to the facts

Before a rule can fire we must settle a smaller question: does this rule body match the facts we hold, and if so, under which binding of its variables? That matching is unification, the single primitive both of this volume's reasoning engines share. It is worth deriving on its own, because every firing in the trace to come is a small stack of unifications, and the identical routine reappears, unchanged, in the backward engine of the next chapter.

Recall the vocabulary. A term is either a constant (a lowercase name such as bob or p1, standing for one fixed individual) or a variable (an uppercase name such as X, standing for "some individual, yet to be pinned down"). An atom is a predicate applied to a tuple of terms, stored as the Python tuple (pred, arg1, arg2, ...). A substitution $\sigma$ is a finite map from variables to terms; in code (unify.py, described at the top of the file) it is "a plain dict mapping variable names to terms," so the substitution $\{X \mapsto \text{bob},\, Y \mapsto \text{carol}\}$ is literally the dictionary {'X': 'bob', 'Y': 'carol'}.

To unify two atoms is to find a substitution that makes them identical. The routine unify (unify.py lines 23–43) does it argument by argument:

def unify(a, b, sub=None):
    sub = {} if sub is None else dict(sub)
    if a[0] != b[0] or len(a) != len(b):
        return None
    for x, y in zip(a[1:], b[1:]):
        x, y = walk(x, sub), walk(y, sub)
        if x == y:
            continue
        if is_var(x):
            sub[x] = y
        elif is_var(y):
            sub[y] = x
        else:
            return None
    return sub

Read it in four moves. Line 30 copies the incoming substitution, so a failed attempt never corrupts the caller's bindings. Line 31 is the fast rejection: if the two atoms disagree on their predicate name a[0] or on their arity (the number of arguments, len(a)), they can never be made equal, and the function returns None, read as "no unifier exists." The loop then walks the two argument lists in lockstep. For each pair, walk (lines 16–20) first resolves each term to what it currently stands for, following any chain of bindings already in sub to its end. The while in walk is precisely that chase: as long as the term is a variable that appears as a key in sub, replace it by its bound value and look again, stopping at the first term that is either a constant or an unbound variable. Then three cases decide the pair. If the two resolved terms are already equal, there is nothing to do and we continue. If one side is a variable, bind it to the other side, extending $\sigma$ by one entry. If both sides are distinct constants, they clash and the whole unification fails. Survive every argument and line 43 returns the extended substitution.

Trace it on the exact match the grandAdvisor rule needs, unify(("advises","X","Y"), ("advises","bob","carol"), {}):

step	resolved pair $(x, y)$	case triggered	substitution after
start	—	—	{}
predicate/arity	advises vs advises, both arity 2	passes line 31, continue	{}
arg 1	X vs bob	is_var(x): bind X	{'X': 'bob'}
arg 2	Y vs carol	is_var(x): bind Y	{'X': 'bob', 'Y': 'carol'}

The result $\{X \mapsto \text{bob},\, Y \mapsto \text{carol}\}$ is exactly the binding that turns the body atom advises(X, Y) into the base fact advises(bob, carol). Now watch a clash, which is how the engine prunes dead ends. With those two bindings already in hand, suppose we try to match the rule's second body atom advises(Y, Z) against the fact advises(bob, carol). The first argument pair is (Y, bob); walk resolves Y to carol, the fact supplies the constant bob, and carol and bob are two different constants, so line 42 returns None and this pairing is silently discarded. A binding made by the first atom therefore constrains what the second atom can match, which is the entire mechanism of the join we watch next.

apply_sub (lines 46–48) is the mirror image of unify: given a finished substitution it walks every argument of an atom and replaces each bound variable by its value, turning the rule head ("grandAdvisor","X","Z") under $\{X\mapsto\text{bob},\, Z\mapsto\text{erin}\}$ into the ground atom ("grandAdvisor","bob","erin"). Unify to find the binding; apply it to build the new fact. That pair of steps is the whole of one modus ponens in code, and everything above it is just doing it many times.

Forward chaining, formalized: the immediate-consequence operator

Modus ponens fires one rule once. Forward chaining does it exhaustively: fire every rule whose body is currently satisfied, collect all the new heads, and repeat until no new fact appears [1]. One full sweep, "fire everything applicable right now," is the immediate-consequence operator, written $T_P$, often read as the transformation a program $P$ performs on a set of facts [2]. We can write it as one set equation. Let $S$ be the current set of ground atoms. Then

$$T_P(S) \;=\; S \;\cup\; \bigl\{\, h\sigma \;:\; (h \leftarrow b_1, \ldots, b_k) \in P,\ \sigma \text{ a substitution},\ b_i\sigma \in S \text{ for all } i = 1, \ldots, k \,\bigr\}.$$

Decode the pieces. The union symbol $\cup$ means "throw both collections together into one set." The braces $\{\,\cdot : \cdot\,\}$ are set-builder notation: everything before the colon is the shape of a member, everything after is the condition it must satisfy, and the colon reads "such that." The membership symbol $\in$ reads "is an element of," so $b_i\sigma \in S$ says the substituted body atom is one of the facts we currently hold, and $(h \leftarrow b_1, \ldots, b_k) \in P$ says the rule is one of the program's rules. The quantifier phrase "for all $i = 1, \ldots, k$" ranges over every body atom of the rule; the symbol $\forall$, which we will use shortly, is its shorthand and reads simply "for every." Read the whole line in English: $T_P(S)$ is the facts you already had, plus every head you can produce by finding one substitution that makes an entire rule body true in $S$. Its definition in forward_chain.py (lines 42–49) is almost a transcription of that sentence:

def t_p(facts: set, rules: list) -> set:
    """One application of the immediate-consequence operator: the input facts
    plus every head derivable in a single step."""
    out = set(facts)
    for head, body in rules:
        for sub in _match_body(body, facts, {}):
            out.add(apply_sub(head, sub))
    return out

Line 45, out = set(facts), is the $S \cup \{\cdot\}$ part: the output starts as a copy of everything you had. The double loop is the set-builder made procedural. For every rule, _match_body (lines 19–39) yields every substitution sub that satisfies the whole body against the current facts, matching atoms left to right and extending the running $\sigma$ exactly as unify did above; then out.add(apply_sub(head, sub)) builds the substituted head $h\sigma$ and adds it. Two structural properties of $T_P$ fall straight out of this definition, and both are load-bearing later.

$T_P$ is inflationary: $S \subseteq T_P(S)$ always. The symbol $\subseteq$ reads "is a subset of or equal to," meaning every element of the left set is also in the right set. This holds because line 45 seeds out with all of facts before anything is added, so no input fact is ever lost. Iterating $T_P$ can therefore only grow the set.

$T_P$ is monotone: if $S \subseteq S'$ then $T_P(S) \subseteq T_P(S')$. Here is the proof, straight from the equation. Take any atom $A \in T_P(S)$. There are two cases. If $A \in S$, then since $S \subseteq S'$ we have $A \in S' \subseteq T_P(S')$, done. Otherwise $A = h\sigma$ for some rule whose body atoms all satisfy $b_i\sigma \in S$; because $S \subseteq S'$, those same atoms satisfy $b_i\sigma \in S'$, so the identical firing is available over $S'$ and $A = h\sigma \in T_P(S')$. Either way $A \in T_P(S')$, so $T_P(S) \subseteq T_P(S')$. Adding facts never removes a conclusion; larger inputs give larger outputs.

The driver that iterates $T_P$ to the point where nothing new appears is least_fixpoint (forward_chain.py lines 52–63):

def least_fixpoint(facts, rules, trace: bool = False):
    current = set(facts)
    sizes = [len(current)]
    while True:
        nxt = t_p(current, rules)
        sizes.append(len(nxt))
        if nxt == current:
            return (current, sizes) if trace else current
        current = nxt

The loop builds the chain $S_0, S_1, S_2, \ldots$ with $S_0$ the base facts and $S_{n+1} = T_P(S_n)$. Because $T_P$ is inflationary, this chain ascends, $S_0 \subseteq S_1 \subseteq S_2 \subseteq \cdots$, and it halts the instant a sweep changes nothing, nxt == current. The set where it stops is a fixpoint: a set $S$ with $T_P(S) = S$, meaning one more sweep produces nothing new. The smallest fixpoint reachable from the base facts is the least fixpoint, written $\mathrm{lfp}(T_P)$. For a Horn program it coincides exactly with the program's least Herbrand model, the minimal set of ground atoms that makes every rule true [2], a claim we make precise and use in the soundness-and-completeness section.

Why the loop is guaranteed to stop

The while True never worries a Datalog programmer, and here is the exact reason. Everything the rules can ever produce lives inside the Herbrand base $B$: the set of all ground atoms you can form from the program's predicates and its finitely many constants. Count it for our world. The constants (kb.py lines 32–35) are 5 people, 3 papers, 2 institutions, and 3 topics, so $|C| = 13$ (the bars $|\cdot|$ denote the size, the number of elements, of a set). The predicates are four unary ones (professor, student, researcher, person) and eight binary ones (advises, authored, cites, affiliated, about, grandAdvisor, colleague, citesTransitively). A unary atom is one predicate applied to one constant, giving $4 \times 13 = 52$ possibilities; a binary atom is one predicate applied to an ordered pair of constants, giving $8 \times 13^2 = 8 \times 169 = 1352$. So

$$|B| \;=\; 4 \cdot 13 \;+\; 8 \cdot 13^2 \;=\; 52 + 1352 \;=\; 1404 .$$

Every $S_n$ is a subset of this finite $B$. An ascending chain of subsets of a set of size $N$ can grow strictly at most $N$ times before it runs out of room, because each strict step adds at least one new element and there are only $N$ elements to add. Therefore $T_P$ must reach a fixpoint within at most $|B| = 1404$ sweeps. That is the worst case; the actual academic world exhausts itself in two productive sweeps, as we are about to watch.

A worked sweep, then three proofs

Running the module on the academic world prints the trace we will decode for the rest of the chapter:

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.
   ('citesTransitively', 'p2', 'p1')
   ('citesTransitively', 'p3', 'p1')
   ('citesTransitively', 'p3', 'p2')

From 23 asserted base facts, the seven rules force out 24 more, for a derived model of 47 atoms. (The 23 counts up as $5$ class memberships, $4$ advises, $4$ authored, $2$ cites, $5$ affiliated, and $3$ about, exactly the base facts listed in kb.py lines 39–69.) Before reading proofs off that model, watch a single sweep of $T_P$ actually move, from the 23 base facts $S_0$ to the 41-atom $S_1$. This is the mechanism in motion, one rule and one substitution at a time.

rule fired (kb.py line)	substitutions $\sigma$ that satisfy the body in $S_0$	heads added
researcher(X) ← professor(X) (75)	$X\mapsto$ alice; $X\mapsto$ bob	researcher(alice), researcher(bob)
researcher(X) ← student(X) (76)	$X\mapsto$ carol, dave, erin	researcher(carol), researcher(dave), researcher(erin)
person(X) ← researcher(X) (77)	(no researcher atom is in $S_0$ yet)	none
grandAdvisor(X,Z) ← advises(X,Y) ∧ advises(Y,Z) (79)	$\{X,Y,Z\}\mapsto$ (alice,bob,carol), (alice,bob,dave), (bob,carol,erin)	grandAdvisor(alice,carol), grandAdvisor(alice,dave), grandAdvisor(bob,erin)
colleague(X,Y) ← affiliated(X,I) ∧ affiliated(Y,I) ∧ neq(X,Y) (82)	all ordered same-institution pairs: alice/bob at mit; carol/dave/erin at cmu	8 colleague atoms
citesTransitively(A,B) ← cites(A,B) (86)	$\{A,B\}\mapsto$ (p2,p1), (p3,p2)	citesTransitively(p2,p1), citesTransitively(p3,p2)
citesTransitively(A,C) ← cites(A,B) ∧ citesTransitively(B,C) (87)	(no citesTransitively atom is in $S_0$ yet)	none

Two rows produce nothing, and why is the crux of the whole chapter. person(X) ← researcher(X) cannot fire in this sweep because $S_0$ contains no researcher atom; those are being created in the very same sweep, and $T_P$ reads its body against the old set $S_0$, not the half-built new one (line 47 passes facts, not out). Likewise the recursive citation rule needs a citesTransitively atom in its body, and none exists yet. So both wait for the next sweep. The five rows that do fire add $5 + 3 + 8 + 2 = 18$ new atoms, and $23 + 18 = 41$, exactly the second entry of the trace. The engine has not been told which order to derive things in; the dependency structure of the rules imposes the order by itself.

The join, one binding at a time

The grandAdvisor and colleague rows deserve a closer look, because each joins two atoms through a shared variable, and this is where the running substitution from the previous section earns its keep. _match_body matches body atoms left to right; the first atom advises(X,Y) binds $X$ and $Y$, and the second atom advises(Y,Z) is then matched with $Y$ already fixed, so only advising chains that pivot through the same middle person survive. Here is the entire search the engine runs for the grandAdvisor rule, each row a call to unify extending the substitution or clashing on the pinned $Y$:

$\sigma$ after matching advises(X,Y)	candidate for advises(Y,Z)	outcome	head produced
$\{X\mapsto\text{alice}, Y\mapsto\text{bob}\}$	advises(bob,carol)	$Z\mapsto$ carol	grandAdvisor(alice,carol)
$\{X\mapsto\text{alice}, Y\mapsto\text{bob}\}$	advises(bob,dave)	$Z\mapsto$ dave	grandAdvisor(alice,dave)
$\{X\mapsto\text{bob}, Y\mapsto\text{carol}\}$	advises(carol,erin)	$Z\mapsto$ erin	grandAdvisor(bob,erin)
$\{X\mapsto\text{bob}, Y\mapsto\text{dave}\}$	no fact advises(dave, ·)	clash on $Y$	none
$\{X\mapsto\text{carol}, Y\mapsto\text{erin}\}$	no fact advises(erin, ·)	clash on $Y$	none

Four advises facts give four ways to bind the first body atom; only three of those extend to a second advises fact whose first argument equals the pinned $Y$, so exactly three grand-advisors come out. The colleague rule adds a third body atom, the built-in guard neq(X, Y), handled specially in _match_body (lines 30–35): it is not a stored fact but a test that succeeds only when its two now-ground arguments differ, which is what stops the engine from calling everyone their own colleague. At mit that leaves the ordered pairs (alice, bob) and (bob, alice); at cmu, the six ordered pairs among carol, dave, and erin, namely (carol, dave), (carol, erin), (dave, carol), (dave, erin), (erin, carol), (erin, dave); eight in all, exactly the eight colleague atoms the run prints.

With the mechanism visible, the proofs write themselves. The derived model is not just a bag of 47 atoms; every non-base atom carries an implicit proof, the chain of firings that put it there. Take the simplest ladder, person(erin), reached in two rule applications:

1. student(erin) is a base fact, asserted directly (kb.py line 44).
2. researcher(X) ← student(X) fires with $\sigma = \{X \mapsto \text{erin}\}$, adding researcher(erin).
3. person(X) ← researcher(X) fires with the same $\sigma$, adding person(erin).

Three atoms, two applications of modus ponens, one proof. As a proof tree, read upward from the leaf:

        student(erin)          [base fact]
      ───────────────────      researcher(X) ← student(X),  X↦erin
        researcher(erin)
      ───────────────────      person(X) ← researcher(X),   X↦erin
          person(erin)

erin was never told she is a person; the rules derived it, and the derivation is auditable step by step. The grand-advisor proof is a single application that pins two premises together through the shared middle person, as the join table already showed:

   advises(bob,carol)   advises(carol,erin)     [two base facts]
   ─────────────────────────────────────────    grandAdvisor(X,Z) ← advises(X,Y) ∧ advises(Y,Z)
              grandAdvisor(bob,erin)             X↦bob, Y↦carol, Z↦erin

The deepest proofs in this world are transitive citations, because that rule feeds its own output back into its own input (kb.py lines 86–88). The base facts give a citation chain p3 → p2 → p1. The direct rule turns each cited pair into a transitive one, so citesTransitively(p2, p1) and citesTransitively(p3, p2) appear in the first sweep. But citesTransitively(p3, p1) cannot: its recursive rule needs cites(p3, p2) (a base fact) and citesTransitively(p2, p1) (itself a derived fact). Only after that second fact exists can the recursive rule reach across the whole chain:

   cites(p3,p2)   citesTransitively(p2,p1)        [base fact ; derived in sweep 1]
   ──────────────────────────────────────         citesTransitively(A,C) ← cites(A,B) ∧ citesTransitively(B,C)
           citesTransitively(p3,p1)                A↦p3, B↦p2, C↦p1

That dependence, a fact whose proof requires an already-proved fact, is exactly why this rule needs a fixpoint and cannot be settled in one pass. Its proof tree is genuinely two layers deep, and it is the reason a second productive sweep exists at all.

The waves are proof depth

Reread the size trace [23, 41, 47, 47] and it stops being an implementation detail and becomes a map of proof depth. Each entry is $|S_n|$, the model after $n$ sweeps of $T_P$, and a sweep is one more inference step, so the wave in which a fact first appears is the length of its shortest proof. Here is every atom accounted for.

| wave $n$ | $|S_n|$ | new this wave | what enters, and what it waited on | |---|---|---|---| | 0 | 23 | 23 | the base facts, proof depth 0 (asserted, nothing derived) | | 1 | 41 | 18 | 5 researcher, 8 colleague, 3 grandAdvisor, 2 direct citesTransitively: everything one firing from base facts | | 2 | 47 | 6 | 5 person (each waiting on its wave-1 researcher) and citesTransitively(p3,p1) (waiting on wave-1 citesTransitively(p2,p1)) | | 3 | 47 | 0 | the confirmation sweep: every rule re-fires but produces only atoms already present |

The counts are the run's own output: the 18 new atoms of wave 1 are the five researcher, eight colleague, three grandAdvisor, and two direct citesTransitively facts we enumerated; the 6 new atoms of wave 2 are the five person facts plus the single reach-across citesTransitively(p3,p1); and $5+3+8+2+5+1 = 24$ is the derived total the header line reports. The wave-2 row is the payoff of the recursion. Its six atoms are precisely the ones whose shortest proof is length 2, and the table's "waited on" column names the wave-1 fact each one consumes. The final row, wave 3, adds nothing: firing every rule over the 47-atom set re-derives the same 47 atoms and no more, so nxt == current and the loop returns. That unchanging wave is not wasted work. It is the algorithm proving to itself that it is done, the runtime face of completeness. The deepest facts in this world (person(erin) and citesTransitively(p3, p1)) have proofs of length 2, which is why the model is fully grown after two productive sweeps and the third merely confirms it. In the worst-case bound of the previous section the loop could run 1404 times; the rule dependencies of this program let it finish in 2.

Forward chaining read as proof: each wave adds exactly the facts one inference step deeper than the last, the highlighted chain from student erin to person erin is a proof, and the final empty wave is the algorithm confirming it has reached the least fixpoint. Original diagram by the authors, created with AI assistance.

Soundness and completeness: why you can trust the model

A reasoning procedure is only worth running if you can say precisely what its output means. Two properties pin that down, and forward chaining has both for Horn rules [1]. Stating them needs two more operators. Write $P \vDash A$, read "$P$ entails $A$," to mean that $A$ is true in every model of $P$: every set of ground atoms that contains the base facts and satisfies every rule must also contain $A$. Write $P \vdash A$, read "$P$ derives $A$," to mean that forward chaining actually produces $A$, that $A \in \mathrm{lfp}(T_P)$. The double turnstile $\vDash$ is about truth in all models (semantics); the single turnstile $\vdash$ is about what the machine can produce (syntax). Soundness and completeness say these two coincide.

Soundness is the direction $P \vdash A \implies P \vDash A$ (the arrow $\implies$ here reads "implies," at the level of whole statements): the procedure derives only entailed facts. We prove it by induction on the wave in which $A$ first appears. Fix any model $M$ of $P$, meaning $M$ contains the base facts and satisfies every rule. Base case: an atom in $S_0$ is a base fact, and $M$ contains all base facts, so it is in $M$. Inductive step: suppose every atom of $S_n$ lies in $M$, and let $A$ be new in $S_{n+1}$. By the definition of $T_P$, $A = h\sigma$ for some rule $h \leftarrow b_1, \ldots, b_k$ with every $b_i\sigma \in S_n$. By the inductive hypothesis each $b_i\sigma \in M$; since $M$ satisfies that rule, the body being true in $M$ forces the head $h\sigma \in M$. So every atom of $S_{n+1}$ is in $M$. As $M$ was an arbitrary model, every derived atom is in every model, which is the definition of $P \vDash A$. The single move the engine makes is modus ponens, modus ponens is truth-preserving, and a chain of truth-preserving steps can never manufacture a falsehood. That is why person(erin) in the output is a certainty, not a guess.

Completeness is the reverse direction $P \vDash A \implies P \vdash A$: the procedure derives all entailed facts. The argument turns on one fact about $\mathrm{lfp}(T_P)$: it is itself a model of $P$. It contains the base facts (they are $S_0 \subseteq \mathrm{lfp}(T_P)$), and it satisfies every rule, because if some rule's body were satisfied in $\mathrm{lfp}(T_P)$ by a substitution $\sigma$ but the head $h\sigma$ were missing, then $T_P$ applied once more would add $h\sigma$, contradicting the fact that $\mathrm{lfp}(T_P)$ is a fixpoint where one more sweep changes nothing. So $\mathrm{lfp}(T_P)$ is a model. Now suppose $P \vDash A$. Then $A$ is true in every model, in particular in the model $\mathrm{lfp}(T_P)$, so $A \in \mathrm{lfp}(T_P)$, which is precisely $P \vdash A$. Moreover $\mathrm{lfp}(T_P)$ is the least Herbrand model: because a Horn program's models are closed under intersection (the intersection of any family of models is again a model), the intersection of all models is itself the smallest model, and it equals $\mathrm{lfp}(T_P)$ [2][3]. "Least" is what makes the claim tight in both directions at once. The model adds nothing beyond what the rules force, so it also contains no unentailed atom.

Put the two halves together: $P \vdash A$ if and only if $P \vDash A$. The 47-atom model is exactly the set of entailed ground atoms, no fewer (completeness) and no more (soundness). The moment the size trace repeats, 47, 47, you hold not a set of consequences but the complete one, which is why a downstream system can treat it as ground truth rather than a heuristic sketch.

Two directions of proof, and where the fixpoint goes next

Forward chaining is one of two directions you can run a proof. It is data-driven: start from the facts and push forward, deriving everything, whether or not you asked for it. That is ideal when you want the whole model materialized, as a database view or an ontology's closure. The other direction is goal-driven backward chaining: start from a query and work backward, asking "which rule could conclude this, and what would its body then require?", recursing on those sub-goals until it grounds out in base facts [1]. To answer whether person(erin) holds, backward chaining would match it against the head of person(X) ← researcher(X), reduce the goal to researcher(erin), match that against researcher(X) ← student(X), reduce to student(erin), and find it among the facts, walking the very proof tree we drew above but built top-down from the question rather than bottom-up from the data. Both directions run on the same unify primitive we derived; they differ only in whether unification is aimed at the facts or at the rule heads. Forward chaining computes everything and then looks up the answer; backward chaining computes only what the question demands. They prove the same theorems by opposite routes, and the next chapter builds the backward engine in full.

The forward direction also has a longer future in this series, and it rests entirely on the fixpoint. The same "fire every applicable rule to a fixpoint" loop, specialized to the constructs of a description logic, is the completion algorithm that Volume 2 uses to classify an ontology in the EL family, the decidable fragment the previous chapter flagged as the deliberate retreat from full first-order logic. The rules researcher(X) ← student(X) and person(X) ← researcher(X) are, read in that light, an implicit class hierarchy $\text{student} \sqsubseteq \text{researcher} \sqsubseteq \text{person}$, where the operator $\sqsubseteq$ reads "is subsumed by," meaning "is a subclass of, so every instance of the left is an instance of the right." That is one of several places the same engine reappears, so rather than unpack it here we hand it forward: Fixpoints, Chapter 7, is where this operator and its least fixpoint get their full mathematical treatment, the single idea beneath forward chaining, Datalog, transitive closure, and that description-logic engine alike. Here we needed only enough of the fixpoint to see that a derivation is a proof; there it becomes the whole subject.

The unsolved part

Forward chaining's guarantees are bought with a bill it pays up front: it derives everything, whether or not you need it. On our toy world that is 24 harmless atoms, but the transitive-citation rule is a warning in miniature. Recursive rules over a large, densely connected knowledge graph can make the least fixpoint explode: the transitive closure of a citation graph with $m$ edges can hold up to order $m^2$ derived edges, so the bound $|B|$ that comforted us here (1404 atoms) becomes astronomical at web scale. When only a single fact is in question, materializing the entire model to answer it is enormous wasted work, which is the standing argument for the backward, goal-driven direction. And forward chaining's clean soundness-and-completeness story holds because the rules are Horn: one positive head, no negation, no disjunction. The proofs above used exactly that shape. Soundness used "the body being true forces the head," and completeness used the model-intersection property, both of which are theorems about Horn clauses specifically. Add negation ("a person is inactive if we cannot derive that they published") and the model-intersection property fails: a program may admit several equally-minimal models with no single least one, so $\mathrm{lfp}(T_P)$ and even "the meaning of the program" stop being well defined. Deciding what a rule set even means once negation enters is a genuinely open design space, one that later volumes must confront the moment rules meet the open, incomplete world neural systems live in.

Why it matters

Neuro-symbolic AI keeps returning to one question this chapter answers crisply: what is the target a neural network imitates when we ask it to "reason"? The answer is the least fixpoint, the exact, sound, complete set of consequences the rules force, the 47 atoms our engine both computes and certifies. Because that target is defined by a mechanical procedure with the guarantee $P \vdash A \iff P \vDash A$, we can always state the correct answer and grade a learned reasoner against it: the model is the label. And forward chaining hands us proofs, not just answers: the length-2 tree behind citesTransitively(p3, p1) is an auditable explanation of why the fact holds, and the wave a fact appears in is a readout of how deep that explanation runs. A neural model that predicts the same fact with no such chain is faster and noise-tolerant but unaccountable, and that derivation is the accountability the symbolic side brings to the hybrid. Every later volume that makes reasoning differentiable is, at bottom, approximating this fixpoint while trying to keep some trace of the proof.

Key terms

• Inference rule — a licensed move from premises to a conclusion; the smallest step of reasoning.
• Modus ponens — from $P$ and $P \to Q$, conclude $Q$; the truth-preserving move forward chaining fires over and over.
• Horn rule — a rule with one positive head atom and a conjunction of positive body atoms, read "head holds if the whole body holds"; a fact is the empty-body case.
• Substitution ($\sigma$) — a mapping of a rule's variables to constants that makes its body match known facts; $b\sigma$ is the atom $b$ after applying it.
• Unification — the primitive that finds a substitution making two atoms identical, deciding argument by argument (predicate and arity first, then each term pair) and clashing on two distinct constants; apply_sub then builds the substituted atom.
• Forward chaining — data-driven reasoning: fire every applicable rule and repeat until no new fact appears.
• Immediate-consequence operator ($T_P$) — one sweep, $T_P(S) = S \cup \{h\sigma : \text{some rule's body is satisfied by } \sigma \text{ in } S\}$; it is inflationary ($S \subseteq T_P(S)$) and monotone ($S \subseteq S' \Rightarrow T_P(S) \subseteq T_P(S')$).
• Herbrand base — the finite set of all ground atoms formable from the program's predicates and constants; for our world $|B| = 1404$, which bounds the number of sweeps.
• Fixpoint / least fixpoint (lfp) — a fact set unchanged by $T_P$; the least one reachable from the base facts is the program's meaning, equal to the least Herbrand model.
• Proof / derivation — a finite sequence of atoms, each a base fact or a rule head whose body atoms appear earlier; the trail of firings behind a derived fact.
• Entailment ($\vDash$) versus derivation ($\vdash$) — $P \vDash A$: true in every model; $P \vdash A$: produced by forward chaining. Soundness and completeness make them coincide.
• Soundness — $P \vdash A \Rightarrow P \vDash A$: the procedure derives only entailed facts.
• Completeness — $P \vDash A \Rightarrow P \vdash A$: the procedure derives all entailed facts.
• Backward chaining — goal-driven reasoning: start from a query and reduce it to sub-goals until it grounds out in facts.

Where this leads

We can now grow a world forward and read a proof off the growth. But forward chaining answers a question only by first deriving everything, a poor fit when you have one goal in mind and a large world at your back. The next chapter, Resolution and SLD, turns the arrow around: it starts from a goal, works backward through the rules that could establish it using the same unification primitive we built here, and returns not just a yes-or-no but a proof tree, the auditable, goal-directed reasoning that Prolog is built on and that the rest of the volume leans on when a query, not a closure, is what we want.

---

Companion code: examples/logic/forward_chain.py implements the immediate-consequence operator t_p and the fixpoint driver least_fixpoint in pure Python, over the academic-world facts and rules in examples/logic/kb.py and the unification primitive unify / apply_sub in examples/logic/unify.py. Run python3 examples/logic/forward_chain.py to reproduce every number in this chapter, including the [23, 41, 47, 47] wave trace and the three transitive citations.