Fixpoints: Reasoning as Reaching a Limit

📍 Where we are: Part II · Reasoning as Computation — Chapter 7. Resolution and SLD showed how a machine proves one goal by working backward from it; now we turn around and compute everything that follows by climbing forward to a limit a single sweep can never reach.

Backward reasoning asks a question and chases it down. Forward reasoning does the opposite: it takes the facts you have, fires every rule that applies, and repeats, growing the set of known truths until a round adds nothing new. That "until nothing new appears" is not a programming convenience. It is a precise mathematical object, the least fixpoint of an operator, and it turns out to be the same object hiding under four things this series keeps meeting: forward chaining, Datalog query evaluation, transitive closure, and, in Volume 2, the description-logic completion algorithm. This chapter is about that one idea and why recursion is exactly where you cannot avoid it.

This chapter builds the idea from nothing. We will not treat "iterate until nothing changes" as a black box. We will prove that the limit exists (Knaster–Tarski), prove that the climb from the bottom reaches it and halts on a finite world (the Kleene construction), prove that the operator behind forward chaining has the one property those theorems need, and then run the climb by hand on the running example, watching the fact set grow along the exact [23, 41, 47, 47] waves the committed code prints. By the end you will be able to read almost any symbolic reasoner and see one loop staring back.

The simple version

Imagine a rumor spreading through a department. On day one, whoever starts it tells their friends. On day two, those people tell their friends, including some who could never have heard it on day one, because they are two handshakes from the source. Each day the circle grows; eventually a day passes where nobody new learns anything, and the rumor has reached everyone it ever will. That final circle is a fixpoint: apply the "tell your friends" step to it and it does not change. You could not have found it in a single day of telling, because the friend-of-a-friend only hears after the friend does. Reasoning by forward chaining is exactly this, with "facts the rules can derive" in place of "people who know."

What this chapter covers

• The lattice of fact sets — every subset of the possible atoms, ordered by ⊆, with a bottom ⊥ (nothing known) and a top ⊤ (everything), and the two order ideas (monotone maps, ascending chains) the whole chapter runs on.
• Knaster–Tarski, proved — a monotone operator on a complete lattice always has a least fixpoint; we prove it exists as the intersection of all sets the operator maps into themselves.
• The Kleene climb, proved — iterating from ⊥ builds an ascending chain that on a finite domain must halt at that least fixpoint; the proof is the exit test of the real loop.
• The immediate-consequence operator T_P — forward chaining is iterating T_P; we prove it is monotone (because rule bodies are positive), then run it live from forward_chain.py.
• The [23, 41, 47, 47] waves, worked atom by atom — a full trace of which atoms enter in which round, and why person waits one wave behind researcher and the two-hop citation waits one wave behind the one-hop.
• Why recursion demands a fixpoint — a chain of ordinary rules needs a bounded number of passes; recursion makes the count ride on the data, so no fixed unrolling is safe.
• Transitive closure as the same loop — the identical "iterate to a limit" idea on relations, quoted and traced from sets_relations.py.
• The recurring engine, and the frontier — why description-logic completion (Volume 2) and differentiable fixpoint layers (Volume 4) are the same pattern, and how existential rules and the chase can make the climb endless.

The lattice of fact sets: monotone maps and a growing chain

Two ideas from Order and Lattices are the whole toolkit here, so recall them on the objects we actually reason about. Collect every ground atom the academic world could possibly state into one big pool: every ("professor", "alice"), every ("citesTransitively", "p3", "p1"), one atom for every predicate applied to every choice of the five people and three papers. Logicians call this pool the Herbrand base; write it $H$. A snapshot of "what is currently known" is some subset of $H$, and reasoning moves between subsets.

Two symbols carry the argument. The subset relation $A \subseteq B$ (read "$A$ is a subset of $B$") means every atom that is in $A$ is also in $B$, so $B$ knows at least everything $A$ knows. The membership symbol $a \in A$ (read "$a$ is an element of $A$") means the atom $a$ sits inside the set $A$. Ordered by ⊆, the subsets of $H$ form a complete lattice: any family of them, even an infinite family, has a least upper bound and a greatest lower bound. Concretely, for fact sets the least upper bound is the union $\bigcup$ (throw all the atoms together; the smallest set containing them all) and the greatest lower bound is the intersection $\bigcap$ (keep only the atoms common to all; the largest set contained in each). The bottom element ⊥ is the empty set $\varnothing$ (nothing derived yet), the smallest set of all; the top element ⊤ is $H$ itself (everything conceivable), the largest.

A monotone map is a function $F$ on this lattice that never scrambles the order:

$$A \subseteq B \quad\Longrightarrow\quad F(A) \subseteq F(B).$$

The arrow $\Longrightarrow$ reads "implies." In words: feed a monotone operator a bigger set of facts and it can only give back a bigger result, never a smaller one. An ascending chain is a sequence of sets that only grows,

$$X_0 \subseteq X_1 \subseteq X_2 \subseteq \cdots,$$

where the subscript is a plain counter, $X_t$ being the set "after $t$ steps." Reasoning, it turns out, is the act of building one such chain and reading off its limit. Everything below is these two notions applied to one specific operator.

Knaster–Tarski: a monotone operator always settles

Here is the theorem that makes "iterate until nothing changes" legitimate rather than hopeful. A fixpoint of an operator $F$ is a set $X$ that $F$ maps to itself, $F(X) = X$: apply the operator and nothing moves. The Knaster–Tarski theorem says that every monotone operator on a complete lattice has fixpoints, and among them a single smallest one, the least fixpoint, written $\mathrm{lfp}(F)$, contained in every other fixpoint [1].

Most texts state this and move on. We prove the part we depend on, that the least fixpoint exists, because the proof is three short steps and it shows where the limit lives before we compute it.

The least fixpoint exists: a proof

Call a set $X$ closed under $F$ if applying $F$ does not push it any higher, that is $F(X) \subseteq X$. Gather all closed sets into one collection,

$$\mathcal{C} \;=\; \{\, X \subseteq H : F(X) \subseteq X \,\}.$$

(The set-builder braces read "all $X$ such that…"; the colon reads "such that.") This collection is not empty, because the top ⊤ is closed: $F(\top) \subseteq \top$ holds automatically, since every set is a subset of the top. Now form the intersection of everything in $\mathcal{C}$,

$$m \;=\; \bigcap \mathcal{C},$$

the atoms common to every closed set. We claim $m = \mathrm{lfp}(F)$, in three steps.

Step A — $m$ is itself closed. Pick any closed set $X \in \mathcal{C}$. Since $m$ is the intersection of a family that includes $X$, we have $m \subseteq X$. Monotonicity turns that into $F(m) \subseteq F(X)$, and $X$ closed means $F(X) \subseteq X$. Chaining the two inclusions, $F(m) \subseteq X$. This holds for every $X \in \mathcal{C}$, so $F(m)$ sits below every closed set, hence below their intersection: $F(m) \subseteq \bigcap \mathcal{C} = m$. So $m$ is closed.

Step B — $m$ is actually a fixpoint. Apply $F$ to the inclusion just proved. Monotonicity gives $F(F(m)) \subseteq F(m)$, which says $F(m)$ is also closed, so $F(m) \in \mathcal{C}$. But $m$ is a lower bound of $\mathcal{C}$, below every member, so $m \subseteq F(m)$. Now we have both $F(m) \subseteq m$ (Step A) and $m \subseteq F(m)$. The subset order is antisymmetric — from Order and Lattices, $A \subseteq B$ and $B \subseteq A$ together force $A = B$ — so $F(m) = m$. The intersection of all closed sets is a genuine fixpoint.

Step C — $m$ is the least fixpoint. Let $Y$ be any fixpoint, $F(Y) = Y$. Since $F(Y) = Y$, in particular $F(Y) \subseteq Y$, so $Y$ is closed, $Y \in \mathcal{C}$, so $m = \bigcap\mathcal{C} \subseteq Y$. Thus $m$ sits below every fixpoint: it is the least one. $\;\blacksquare$

That is an existence guarantee: it locates the target (the intersection of all closed sets) but does not hand you a procedure that walks to it. For that we need the constructive companion.

The Kleene climb reaches it, and on a finite world it halts

Start at the bottom ⊥ and apply $F$ over and over. Write $F^t$ for "$F$ applied $t$ times," so $F^0(\bot) = \bot$, $F^1(\bot) = F(\bot)$, $F^2(\bot) = F(F(\bot))$, and so on:

$$\bot \;\subseteq\; F(\bot) \;\subseteq\; F(F(\bot)) \;\subseteq\; F(F(F(\bot))) \;\subseteq\; \cdots$$

This is an ascending chain. The first link $\bot \subseteq F(\bot)$ is free, because ⊥ is the empty set and the empty set is a subset of everything. Feed that inclusion through the monotone $F$ and you get $F(\bot) \subseteq F(F(\bot))$; feed that through $F$ and you get the next link; by induction every rung sits at least as high as the one below. Climbing this chain from the bottom and taking its limit is the Kleene fixed-point construction [2].

On a finite domain the climb must stop. Let $|X|$ denote the cardinality of $X$, the plain count of atoms in it. Along the chain $|X_t|$ is a non-decreasing whole number capped by $|H|$, the size of the whole pool. Each strict growth step $X_t \subsetneq X_{t+1}$ (the symbol ⊊ meaning "subset, and not equal") adds at least one atom, so it bumps the count by at least one. A count that starts finite, only rises, and cannot pass $|H|$ can rise only finitely often. Therefore there is a first index $n$ where nothing new arrives, $F^{n+1}(\bot) = F^{n}(\bot)$, and at that index $F$ maps the set to itself: $X_n = F(X_n)$ is a fixpoint.

Is it the least one? Yes, and this is the payoff that ties the two theorems together. Take any fixpoint $Y$ and prove $F^t(\bot) \subseteq Y$ for every $t$ by induction. Base: $F^0(\bot) = \varnothing \subseteq Y$. Step: if $F^t(\bot) \subseteq Y$, then monotonicity gives $F^{t+1}(\bot) = F(F^t(\bot)) \subseteq F(Y) = Y$. So the whole chain lies inside every fixpoint; in particular the fixpoint $X_n$ we reached lies inside every fixpoint, so it is $\mathrm{lfp}(F) = m$ from the previous proof. The climb from the bottom does not merely find a fixpoint; on a finite world it finds the least one, in finitely many steps.

(On an infinite lattice the least fixpoint still exists by Knaster–Tarski, but the climb reaches it only when $F$ is continuous — applying $F$ to the union of the whole chain equals the union of $F$ applied to each rung, $F(X_0 \cup X_1 \cup \cdots) = F(X_0) \cup F(X_1) \cup \cdots$ — and even then the answer may be the least upper bound of the whole infinite chain rather than any finite step. The operator behind forward chaining, and transitive closure, are finitary: each atom they derive reads only finitely many input facts, since one rule firing consults a bounded body. A finitary operator is automatically continuous, because anything it yields from an infinite union of facts already appears from some finite part of that union. So the climb is valid; the frontier section returns to the case where it never halts.)

The immediate-consequence operator T_P

The operator behind forward chaining has a name: the immediate-consequence operator, written $T_P$ (the "P" is for the program of rules). Its job is one sentence: fire every rule whose body is satisfied by the current facts, and add all the resulting heads. Applied to a set of facts, it hands back those facts plus everything derivable in a single step. In forward_chain.py it is a five-line function (eight lines with its docstring), and each clause of that sentence maps onto a line of its body:

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 by line: out = set(facts) copies in the current facts (so $T_P$ never deletes anything); the loop over rules tries each rule; _match_body yields every variable-to-constant substitution that makes the whole body true in the current facts; and out.add(apply_sub(head, sub)) fires the rule by adding the head under that substitution. The output is the input plus the one-step consequences, exactly $T_P(X)$.

T_P is monotone (the one property the theorems need)

Knaster–Tarski and the Kleene climb both require just one thing of $T_P$: monotonicity. Here is the proof, and it rests on a single feature of the rules.

Suppose $A \subseteq B$, and take any atom $h \in T_P(A)$. There are two ways $h$ could have gotten into $T_P(A)$. Either $h$ was already an input fact, $h \in A$; then $h \in B$ because $A \subseteq B$, and since $T_P$ copies its input, $h \in T_P(B)$. Or $h$ is the head of some rule whose body was satisfied by $A$ under a substitution — meaning every atom of that (instantiated) body is an element of $A$. Because $A \subseteq B$, every one of those body atoms is also an element of $B$, so the very same body is satisfied by $B$ under the very same substitution, so the same rule fires on $B$ and produces the same head: $h \in T_P(B)$. Either way $h \in T_P(B)$, so $T_P(A) \subseteq T_P(B)$. $\;\blacksquare$

The load-bearing step is "every body atom in $A$ is also in $B$." It works only because every rule body is a positive conjunction — Horn clauses, no negation. Adding a fact can satisfy more rule bodies, never fewer, so more facts yield more consequences. Had a body contained a negation like "$X$ is not a professor," growing the fact set could switch that condition off and destroy a previously-derivable head, breaking monotonicity and with it every guarantee above. This is why the running example is pure Horn, and why negation is the first thing that makes fixpoint reasoning subtle. In the code, the positivity is visible in _match_body: it satisfies each body atom by finding an actual fact to unify with (for fact in facts: ext = unify(first, fact, sub)), and the only non-fact test, the built-in neq guard, compares two arguments for inequality without ever asking whether some atom is absent.

(Separately, $T_P$ never deletes a fact, so it is also inflationary: $X \subseteq T_P(X)$, from the out = set(facts) copy. Inflation and monotonicity are distinct — inflation compares an input to its own output, monotonicity compares two different inputs — and it is monotonicity, the harder one, that the theorems require.)

With monotonicity in hand, reaching the least fixpoint is the plainest loop imaginable, and it is literally the two theorems made executable:

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

current = set(facts) seeds the climb at the base facts, which is the Kleene climb started one rung up: if we imagined the base facts as rules with empty bodies (bodies that are vacuously satisfied), then $T_P(\bot)$ would already contain them, so seeding with the base facts and seeding with ⊥ reach the same chain. The line nxt = t_p(current, rules) is the single application $X_{t+1} = T_P(X_t)$. And if nxt == current is the exit proof turned into an if: the moment $T_P(X) = X$, the finiteness argument says we have arrived at the least fixpoint, and the loop stops.

The waves, worked atom by atom

Run the module on the academic world and it reports the climb (this is the real printout of python3 forward_chain.py):

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.

Read the trace [23, 41, 47, 47] as the ascending chain $X_0 \subseteq X_1 \subseteq X_2 \subseteq X_3$ itself, with the sizes $|X_t|$ printed rung by rung. The final $47 = 47$ is the round that changes nothing and so proves, by nxt == current, that we are done. Here is exactly which atoms enter on each rung — every number and atom below is captured by instrumenting the real run, not invented:

round $t$	rung $X_t = T_P^{\,t}(\text{base})$	$\lvert X_t\rvert$	atoms added this round	rule(s) that fired
$0$	base facts (the seed)	$23$	the 23 asserted facts	none yet (the seed)
$1$	$T_P(X_0)$	$41$	$+18$: researcher×5, grandAdvisor×3, colleague×8, citesTransitively×2	all rules whose bodies read base facts
$2$	$T_P(X_1)$	$47$	$+6$: person×5, citesTransitively p3→p1 ×1	the two rules that read a derived fact
$3$	$T_P(X_2)$	$47$	$+0$	every firing repeats an atom already present

The whole mechanism is in the last column. Round 1 fires only rules whose bodies are satisfied by the base facts already on the table. The five researcher atoms come from researcher(X) :- professor(X) and researcher(X) :- student(X) (the :- reads "holds if": the head on the left holds whenever the body on the right does). The three grandAdvisor atoms come from composing advises with itself — grandAdvisor(X,Z) :- advises(X,Y), advises(Y,Z) — firing on the chains alice→bob→carol, alice→bob→dave, and bob→carol→erin. The eight colleague atoms are the ordered same-institution pairs (two at mit: alice–bob both ways; six at cmu among carol, dave, erin), with the neq guard blocking a person from being their own colleague. And two citesTransitively atoms, p2→p1 and p3→p2, come from the base case rule citesTransitively(A,B) :- cites(A,B).

Round 2 is where dependence on derived facts shows. Its six new atoms are all conclusions that could not have fired in round 1 because their bodies needed something round 1 had only just produced:

• The five person atoms come from person(X) :- researcher(X). That body reads a researcher atom, which did not exist at round 0 and first appeared at round 1. So person(alice) is exactly one wave behind researcher(alice). Of the six atoms added in round 2, five are person(...); this single rule is most of the second wave.
• The one remaining atom, citesTransitively(p3, p1), comes from the recursive rule and is the crux of the next section.

Round 3 fires every rule again, produces only atoms already in $X_2$, so $X_3 = X_2$: the fixpoint. The limit is 47 atoms, 24 of them derived. This set has a name older than the algorithm: it is the least Herbrand model of the program, the smallest collection of facts that makes every rule true. The classical result of logic programming is that forward chaining and least-model semantics compute the same thing, so $\mathrm{lfp}(T_P)$ simply is the meaning of the program [3]. The procedure and the meaning coincide, and the coincidence is the two proofs above.

Why recursion needs a fixpoint, not one sweep

Two different things push the loop past a single pass, and it pays to keep them apart. The mild one is a chain of ordinary rules: a rule that reads a derived fact must wait for the pass that produces it. We just saw one — person waits for researcher, which waits for professor or student — so person(alice) cannot appear until the wave after researcher(alice). But a rule chain like this always settles in a bounded number of passes, one per layer of the hierarchy, a depth (its derivation depth, the longest chain of predicate dependencies) fixed before you start: professor/student, then researcher, then person, three layers, done. If that were the only complication, you could just unroll the rules a known number of times and never mention fixpoints.

The demanding one is recursion, a rule whose head can re-enter its own body, where the number of passes is not fixed in advance but rides on the data. The academic world has exactly one recursive rule, transitive citation, and kb.py (lines 84–88) flags it as the reason the whole machinery exists:

# Transitive closure of citation — the rule that *needs* a fixpoint, because
# its own head feeds its own body.
(("citesTransitively", "A", "B"), [("cites", "A", "B")]),
(("citesTransitively", "A", "C"),
 [("cites", "A", "B"), ("citesTransitively", "B", "C")]),

The base facts hold a citation chain, p3 cites p2 cites p1. Watch what one sweep can and cannot do. In round 1, the non-recursive first clause turns each direct cites pair into a citesTransitively pair, so p2→p1 and p3→p2 appear. But p3→p1 cannot yet: the recursive second clause needs citesTransitively("p2", "p1") sitting in its body, and that atom did not exist when round 1 began. Only in round 2, with p2→p1 now on the table, does the recursive clause fire to produce p3→p1. Its derivation is a two-level proof tree, and the wave label on each node is exactly the round it entered the model:

citesTransitively(p3, p1)            ← recursive clause, round 2
├── cites(p3, p2)                    ← base fact, round 0
└── citesTransitively(p2, p1)        ← base-case clause, round 1
    └── cites(p2, p1)                ← base fact, round 0

The sorted output of the run confirms the finished closure:

   ('citesTransitively', 'p2', 'p1')
   ('citesTransitively', 'p3', 'p1')
   ('citesTransitively', 'p3', 'p2')

That single delayed atom, p3→p1, is the crux. A conclusion two hops deep is unreachable until the one-hop conclusion beneath it exists, and because a citation chain can be any length, no number of sweeps fixed in advance is safe: a chain of $k$ papers (that is, $k-1$ hops) needs $k-1$ rounds before its longest reachability atom appears. This is the difference from the person/researcher chain, where the depth was a known constant. With recursion the depth rides on the data, so you must iterate until a round is idle. Recursion is precisely the place where reasoning stops being a fixed unrolling and becomes reaching a limit.

Transitive closure: the same idea, one relation at a time

The citation example is a special case of an operation so common it has its own name: the transitive closure of a relation, the smallest relation that contains the original and is closed under "if $a$ reaches $b$ and $b$ reaches $c$, then $a$ reaches $c$." In sets_relations.py it is computed by the very same loop, applied not to a set of logic atoms but to a set of pairs:

def transitive_closure(R: set) -> set:
    closure = set(R)
    while True:
        added = compose(closure, R) - closure
        if not added:
            return closure
        closure |= added

The engine is relational composition, written $R \circ S$ (the ring ∘ reads "composed with"), defined in the file as

$$R \circ S \;=\; \{\, (a, c) : (a, b) \in R \text{ and } (b, c) \in S \,\},$$

which is compose at lines 22–24: pairs that chain through a shared middle element $b$. The shape of transitive_closure is identical to least_fixpoint: start from $R$, apply a monotone step (compose with $R$ and union the new pairs in, closure |= added), and halt when a round adds nothing. The test if not added (line 34) is the same fixpoint test as nxt == current, since added = compose(closure, R) - closure (line 33) is empty exactly when composing produces no pair not already present.

Trace it by hand on the citation relation $R = \{(\text{p2},\text{p1}), (\text{p3},\text{p2})\}$:

iteration	closure at entry	compose(closure, R)	added (new pairs)	action
$1$	$\{(\text{p2},\text{p1}), (\text{p3},\text{p2})\}$	$\{(\text{p3},\text{p1})\}$, from $(\text{p3},\text{p2}) \circ (\text{p2},\text{p1})$	$\{(\text{p3},\text{p1})\}$	add it, loop
$2$	$\{(\text{p2},\text{p1}), (\text{p3},\text{p2}), (\text{p3},\text{p1})\}$	$\{(\text{p3},\text{p1})\}$ (already present)	$\varnothing$	halt

In iteration 1, composition finds one new pair: $(\text{p3},\text{p2})$ in closure chains through p2 into $(\text{p2},\text{p1})$ in $R$, yielding $(\text{p3},\text{p1})$. In iteration 2 the only pair composition can produce is that same $(\text{p3},\text{p1})$, now already present, so added is empty and the loop returns. The real printout matches exactly:

transitive closure of cites: [('p2', 'p1'), ('p3', 'p1'), ('p3', 'p2')]

The pair ('p3', 'p1') is the same derived truth as citesTransitively p3→p1, computed on raw pairs instead of through the rule engine, and it appears at iteration 1 here for the same reason it appeared at round 2 there: it depends on a one-hop fact that had to exist first. This is not a coincidence to admire and forget. It is the foundational-database result that Datalog evaluation is least-fixpoint iteration, and transitive closure is its textbook example of genuine recursion that no fixed set of relational joins can express [4]. Whether you phrase reachability as a Horn rule or as relational composition, you are computing one fixpoint by climbing one ascending chain.

Reasoning as a climb: forward chaining grows the fact set along an ascending chain 23 ⊆ 41 ⊆ 47 ⊆ 47 and halts at the least fixpoint where T_P maps the set to itself, while the two-hop citation p3 → p1 arrives one wave after the one-hop p2 → p1 it is built on. Original diagram by the authors, created with AI assistance.

The engine that keeps returning

Naming the fixpoint pays off because the same engine reappears at every layer of the series, so learning it once is learning all of them.

In Volume 2, a description-logic reasoner decides subsumption by a completion (or saturation) algorithm: it starts with the stated facts and repeatedly applies a fixed set of completion rules — "if an individual is an $R$ and every $R$ is an $S$, mark it an $S$" — adding entailed memberships and edges until a round adds nothing. That is $T_P$ under a different name: a monotone operator whose least fixpoint is the completed model from which every subsumption can be read off, and it is exactly the loop and the two theorems of this chapter. The EL family of description logics is engineered precisely so that this fixpoint stays polynomial in size — for $n$ stated facts the completed model grows to at most on the order of $n$, $n^2$, or $n^3$ facts, never an exponential blow-up — and always terminates, which is why EL reasoners scale to biomedical ontologies with hundreds of thousands of classes.

In Volume 4, differentiable reasoning replaces the crisp "is this atom in the set?" with a soft score in the interval from 0 to 1, and replaces $T_P$ with a smooth, monotone update layer. Running that layer to convergence is a fixpoint layer: it climbs a chain of ever-more-confident fact vectors until the scores stop moving, the continuous analogue of the discrete climb here. The reason such a layer can be trained end to end is that its forward pass is exactly a fixpoint iteration, and a fixpoint can be differentiated through. Symbolic completion and neural fixpoint layers are two implementations of one recipe: iterate a monotone operator from the bottom until it settles.

The unsolved part

The comfort of this chapter rests on one quiet assumption inside the finiteness proof: the domain is finite and fixed. Every atom the academic world can state was drawn from a closed pool of five people and three papers, so $|H|$ was finite, the count $|X_t|$ could not climb past that ceiling, and the chain settled in three waves. Take that assumption away and the guarantee cracks at exactly the step that used it.

The break comes from existential rules, rules whose head asserts that something exists rather than naming a known individual, as in "every researcher has an advisor," which demands an advisor even when none is on record. Firing such a rule invents a fresh individual, and that new individual is itself a researcher who must, in turn, have an advisor, so the same rule fires again on the thing it just made. The forward-chaining process that chases these obligations is called the chase, and its ascending chain need never reach a fixpoint at all: it can climb forever, minting an infinite tower of anonymous advisors' advisors. The finiteness argument fails at its one arithmetic move — $|X_t|$ is no longer capped by a finite $|H|$, so "a rising bounded count must stop" no longer applies. Knaster–Tarski still promises a least fixpoint exists (the operator is monotone, the lattice complete), and because the chase is continuous it is even the limit of that infinite chain, but no terminating loop like least_fixpoint can reach it, and the underlying question — does anything follow? — is undecidable in general.

This is not a flaw to be patched; it is the reason the field is organized the way it is, and here two guarantees must be kept apart. In some fragments the chase is provably finite, so a loop like least_fixpoint computes the answer outright: existential-free Datalog (our case), the EL family of Volume 2, and weakly-acyclic (or acyclic) existential rules — ones where invented individuals cannot feed back to keep spawning fresh individuals forever, so the endless climb just described never gets started — all terminate. In others the chase may run forever, yet query answering stays decidable anyway: guarded (each rule body carries one atom holding all its variables) and sticky (a restriction on how variables propagate as rules fire; Volume 2 makes both precise) existential rules are the classic cases, and they buy that decidability by two genuinely different routes. Guarded rules keep the possibly-infinite chase tree-like, of bounded treewidth, being stitched together from a fixed stock of small, repeating local patterns that decompose into overlapping pieces arranged in a tree, so a query can be answered by exploiting that regular shape without ever building the whole thing. Sticky rules were designed instead to permit the non-guarded joins guardedness forbids, so their chase is not tree-like in general; they earn decidability by being first-order rewritable, meaning the chase can be side-stepped entirely by rewriting the query into an ordinary first-order (SQL-style) query evaluated directly over the given base facts. Either way you pay in expressive power for the guarantee, and Volume 2 is largely the study of where these lines fall. The honest open tension of neuro-symbolic AI lives right here: the expressive logics we would most like to reason in are exactly the ones whose fixpoints we cannot always reach, and buying decidability back is never free.

Why it matters

Almost every symbolic reasoner you will meet in this series is, underneath, the same loop we proved correct and then ran: seed at the bottom, apply a monotone operator, stop when a round changes nothing. Seeing forward chaining, Datalog evaluation, transitive closure, and description-logic completion as one construction — the least fixpoint of a monotone operator — means you learn the pattern once and recognize it everywhere, and you inherit its guarantees (a least, canonical answer exists, by Knaster–Tarski, and the climb reaches it on a finite world, by Kleene) and its dangers (it may be expensive, or endless) as a single package. For the neuro-symbolic program specifically, the fixpoint is the bridge: it is the crisp, provable target that a differentiable reasoning layer is trying to imitate with continuous scores, and the yardstick for whether the neural approximation reached the right limit. When a learned reasoner and a symbolic one climb to the same fixpoint, the hybrid system is coherent; when they do not, the fixpoint is what tells you so.

Key terms

• Herbrand base $H$ — the pool of every ground atom the world can state; its subsets, ordered by ⊆, form the complete lattice reasoning moves through, with bottom ⊥ = ∅ and top ⊤ = $H$.
• Fixpoint — a set $X$ unchanged by an operator, $F(X) = X$; applying the operator moves nothing.
• Least fixpoint ($\mathrm{lfp}$) — the smallest fixpoint of a monotone operator, contained in every other; for forward chaining it is the least model, the meaning of the program.
• Knaster–Tarski theorem — every monotone operator on a complete lattice has a least fixpoint; proved here as the intersection of all sets $F$ maps into themselves. An existence guarantee, silent on how to compute it.
• Kleene fixed-point construction — reaches that least fixpoint by iterating $F$ from ⊥ and taking the limit; the ascending chain must halt on a finite lattice (bounded rising count) and, when it halts, lands exactly on $\mathrm{lfp}(F)$.
• Monotone operator — a map $F$ with $A \subseteq B$ implying $F(A) \subseteq F(B)$: a bigger input yields a bigger output. For $T_P$ this holds because rule bodies are positive; negation would break it. (Distinct from inflationary, $X \subseteq F(X)$, "never removes a fact," which $T_P$ also satisfies.)
• Ascending chain / least upper bound — a sequence that only grows, $X_0 \subseteq X_1 \subseteq \cdots$, and the smallest set above all of it; the fixpoint is the least upper bound of the chain.
• Immediate-consequence operator ($T_P$) — fire every rule whose body holds and add the heads; the monotone operator forward chaining iterates.
• Least Herbrand model — the smallest set of facts satisfying every rule; equal to $\mathrm{lfp}(T_P)$.
• Transitive closure — the smallest transitive relation containing a given one; the textbook recursive fixpoint, computed by the same loop as forward chaining, one relation at a time.
• Completion / saturation (Volume 2) — the description-logic reasoner's fixpoint iteration of entailment rules until nothing new is derived.
• Existential rule / the chase — a rule whose head asserts something exists, invents a fresh individual, and can make the forward-chaining chain climb without ever terminating.
• Terminating-chase fragment — a rule shape (existential-free Datalog, EL, weakly-acyclic or acyclic existential rules) whose chase is finite, so least_fixpoint computes the answer outright.
• Decidable fragment — a rule shape (adding guarded and sticky existential rules) where query answering stays decidable even when the chase can run forever, bought at the cost of expressive power.

Where this leads

We now have the reasoning engine complete, and complete with proof: knowledge encoded as rules, its meaning defined as the least fixpoint of a monotone operator (guaranteed to exist), and that meaning computed by a climb from the bottom that halts the moment a round changes nothing. But every rule so far was given to us — someone wrote "a professor is a researcher," "citation is transitive." The obvious next question is the one that opens the second half of this volume: where do the rules come from when nobody writes them down? The next chapter, What Is Learning: Fitting Functions to Data, turns from deriving consequences of known rules to inferring rules and patterns from examples, the shift from reasoning to learning that the whole neuro-symbolic project is built to reconcile. The fixpoint was how a machine computes with knowledge it has; learning is how it acquires knowledge it lacks.

---

Companion code: examples/logic/forward_chain.py implements t_p (the immediate-consequence operator) and least_fixpoint (the Kleene climb with its nxt == current exit test), and examples/logic/sets_relations.py implements transitive_closure by the identical loop on relations. Run python3 examples/logic/forward_chain.py to reproduce the [23, 41, 47, 47] waves and the citation closure, and python3 examples/logic/sets_relations.py for the transitive closure of cites; both read the running example from kb.py.