First-Order Logic: Objects, Relations, and Quantifiers

📍 Where we are: Part I · Logic from Scratch — Chapter 4. Propositional Logic gave us true, false, and the connectives — but no way to name a single thing or to say "every"; first-order logic cracks that atom open.

Propositional logic could weigh whether "accepted" follows from "novel and correct." What it could never do is name alice, or say one true thing about every professor at once. Each proposition was a solid pebble of truth with no inner parts — you could stack pebbles with ∧ (and), ∨ (or), ¬ (not), → (implies), but you could not look inside one. This chapter cracks the pebble open into the two things a fact is really made of: the objects it talks about, and the relation it claims among them. We will not stop at describing the machinery. We will write down the exact recursive definition of what it means for a sentence to be true in a world, match every line of that definition to the line of committed code that runs it, and then evaluate three real sentences and one real query by hand, sweeping the finite academic world individual by individual exactly as the machine does.

The simple version

Imagine you may only speak in whole statements that are each flatly true or false — "it is raining," "the seminar is at noon" — with no way to say "everyone in the room is tired" except by writing a separate true-or-false statement for every single person. First-order logic hands you three new powers at once: names for individual things (alice, the paper p1), relations that can hold between them (alice advises bob), and the two little quantifying words "every" and "some," so one sentence can speak about a whole crowd. And checking whether such a sentence is true becomes a chore a computer can grind through: to test "every professor is a researcher," it just walks down the list of individuals and checks each one.

What this chapter covers

• The ceiling propositional logic hits — why a logic of true-or-false atoms cannot express "every" or "some," has no notion of an object at all, and would need over a thousand separate atoms just to name the ground facts of our tiny world.
• The pieces of first-order logic — terms (constants and variables), predicates and their arity, the familiar connectives, and the two quantifiers ∀ ("for all") and ∃ ("there exists"), each symbol decoded before it is used.
• Structures and satisfaction, defined exactly — a domain of individuals plus an extension for each predicate, and the full recursive definition of the satisfaction relation ⊨ ("holds in"), matched line by line to how holds() decides a quantified sentence by trying every individual.
• Three sentences, swept by hand — one true universal, one false universal, one true existential, each traced against every individual in the running example, plus the quantifier duality that makes ∀ and ∃ two views of one idea.
• Conjunctive queries — the existential-conjunctive (∃∧) fragment, "who does alice grand-advise?" traced over all thirteen candidates, and why it is exactly the task Volume 4 learns to answer.
• The unsolved part — model checking in one finite world is decidable, but first-order validity over all worlds is not, which is why Volume 2 retreats to a tame, decidable fragment.

The ceiling propositional logic hits

The previous chapter, Propositional Logic, treated each statement as an indivisible truth-bearing atom — accepted, novel — and decided everything (satisfiability, validity, entailment) by enumerating the finitely many true/false assignments. That is powerful, but blind. "alice advises bob" would be one opaque atom, logically unrelated to "bob advises carol." You cannot say advising chains. You cannot say "every professor is a researcher" without hand-writing one separate implication for alice, one for bob, and so on for each professor you happen to have named. And you can never say "some student is advised" at all, because "some" needs a variable — a slot that ranges over the things in the world — and propositional logic has no things and no variables [1]. Propositional logic talks about facts; it cannot talk about the objects the facts are about [2].

It is worth making the ceiling quantitative, because the blow-up is the whole reason quantifiers exist. Our academic world, once fully derived, has 13 individuals and 12 predicates: 4 that take one argument (person, professor, researcher, student) and 8 that take two (about, advises, affiliated, authored, cites, citesTransitively, colleague, grandAdvisor). To speak about this world purely propositionally you would need one distinct atom for every possible ground fact. Counting them:

$$\underbrace{4 \times 13}_{\text{unary}} \;+\; \underbrace{8 \times 13 \times 13}_{\text{binary}} \;=\; 52 \;+\; 1352 \;=\; 1404 .$$

That is 1404 separate propositional letters just to name the atoms of one 13-element world, with no way to say anything general about them. Worse, "every professor is a researcher" would become a finite conjunction of 13 implications, one per individual (professor-of-alice → researcher-of-alice, professor-of-bob → researcher-of-bob, and eleven vacuous others), and the moment a fourteenth individual walked in you would have to hand-write a fourteenth implication. First-order logic replaces all 1404 named atoms with a handful of predicate symbols applied to variables, and replaces that ever-growing conjunction with one sentence, ∀X (professor(X) → researcher(X)), that keeps meaning what it means no matter how many individuals appear.

Terms, predicates, and the two quantifiers

First-order logic adds the missing machinery in layers. First, terms — the names for individuals. A constant names one fixed individual (alice, bob, p1, mit); a variable is a placeholder that ranges over individuals (X, Y). In the running example the only thing that decides which is which is capitalization, and one function in kb.py (lines 25–28) says so:

def is_var(term: str) -> bool:
    """A term is a logic variable iff it is a non-empty string that starts with
    an uppercase letter. Constants (``alice``, ``p1``, ``mit``) start lowercase."""
    return isinstance(term, str) and len(term) > 0 and term[0].isupper()

Next, predicates. A predicate names a property of one thing (professor(x), whose arity — its number of argument slots — is one, a unary predicate) or a relationship among several (advises(x, y), arity two, a binary one). Applied to terms, a predicate forms an atom — the smallest complete claim. The connectives carry over from propositional logic unchanged, and we decode each once here before using it: ¬ ("not," negation) flips a truth value; ∧ ("and," conjunction) is true only when both sides are; ∨ ("or," disjunction) is true when at least one side is; → ("implies," material implication) is false only when a true left side meets a false right side. The symbol ∈ we will lean on shortly reads "is an element of," and ⊆ reads "is a subset of."

The genuinely new power is the pair of quantifiers, and the two symbols deserve slow reading. ∀ (an upside-down A, read "for all") turns a formula about one variable into a claim about the entire domain: ∀X (professor(X) → researcher(X)) asserts the implication holds of every individual. ∃ (a backwards E, read "there exists") asserts a formula holds of at least one individual: ∃X advises(X, bob) says advising-bob is true of somebody. A variable is bound when it sits under a quantifier and free otherwise; a sentence is a formula with no free variables, the kind of thing that has a definite truth value once the world is fixed. Before the symbols do any work, here is the plain-language decoder for how fol.py writes formulas as nested Python tuples: ("all", "X", F) means ∀X F, ("exists", "X", F) means ∃X F, ("imp", F, G) means F → G, and an atom is the predicate name followed by its arguments:

("atom", "professor", "X")
("not", F) / ("and", F, G) / ("or", F, G) / ("imp", F, G)
("all", "X", F) / ("exists", "X", F)

Structures and satisfaction: trying every individual

A sentence has no truth value in a vacuum; it needs a world to be checked against. In first-order logic that world is a structure (also called a model), written here as a pair

$$\mathcal{S} \;=\; (D,\, I),$$

where the calligraphic $\mathcal{S}$ names the whole structure. Its first part, $D$, is the domain: the non-empty set of individuals that exist. Its second part, $I$, is the interpretation: a function that hands every predicate symbol its extension, the exact set of tuples for which the predicate holds. For an $n$-ary predicate $P$ (one taking $n$ arguments) the extension is a subset of $D^n$, the set of all length-$n$ tuples of individuals:

$$I(P) \;\subseteq\; D^n .$$

Read $D^n$ as "$D$ crossed with itself $n$ times," so $D^2$ is every ordered pair of individuals. With $\lvert D\rvert = 13$ (the vertical bars mean "the size of the set"), a binary predicate could in principle hold of $13^2 = 169$ pairs; the extension of advises picks out just 4 of them, which is why extensions are best pictured as sparse tables inside a large grid of possibilities [1]. The Structure class (fol.py, lines 27–34) is exactly this pair: self.domain is $D$ and self.relations is $I$, a dictionary from each predicate name to its set of true tuples.

class Structure:
    def __init__(self, domain, relations: dict):
        self.domain = list(domain)
        # relations: predicate name -> set of tuples of constants
        self.relations = {k: set(v) for k, v in relations.items()}

    def rel(self, pred: str) -> set:
        return self.relations.get(pred, set())

The companion builds one straight from the academic world (fol.py, lines 62–73): it runs the forward-chaining engine to the model (the set of all derivable facts), then reads the domain off as every individual mentioned and each predicate's extension as the set of true argument tuples.

def structure_from_kb() -> Structure:
    facts, rules = program()
    model = least_fixpoint(facts, rules)
    domain, relations = set(), {}
    for atom in model:
        pred, args = atom[0], atom[1:]
        relations.setdefault(pred, set()).add(tuple(args))
        domain.update(args)
    return Structure(sorted(domain), relations)

That least_fixpoint call is the subject of the next chapter; for now take its output as given. It settles in three forward-chaining waves whose cumulative sizes are $[23, 41, 47, 47]$: 23 base facts, then 41 after the first wave of rule firings, then 47, then 47 again with nothing new to add, for a completed model of 47 atoms, 24 of them derived. Reading that model into a structure yields a domain of 13 individuals — the five people, three papers, two institutions, and three topics — and 12 predicates, including the five (researcher, person, grandAdvisor, colleague, citesTransitively) that the Horn rules produced on the way to the fixpoint. That last point matters: the structure is the completed world, so researcher already holds of all five people, not only the two asserted professors. Here are the extensions of the predicates the coming traces touch, exactly as structure_from_kb builds them:

predicate	arity	extension (true tuples)
professor	1	alice, bob
student	1	carol, dave, erin
researcher	1	alice, bob, carol, dave, erin
advises	2	(alice, bob), (bob, carol), (bob, dave), (carol, erin)
grandAdvisor	2	(alice, carol), (alice, dave), (bob, erin)

Now satisfaction — the relation "sentence $F$ holds in structure $\mathcal{S}$," written $\mathcal{S} \models F$, where the turnstile $\models$ reads "satisfies" or "models." It is defined by recursion on the shape of $F$, carrying along an assignment $g$, a partial function mapping each currently-bound variable to the individual it stands for. Writing $\llbracket t\rrbracket_g$ for the individual a term $t$ denotes under $g$ — namely $g(t)$ if $t$ is a variable and $t$ itself if $t$ is a constant, since a constant names itself — the definition is:

$$\begin{aligned} \mathcal{S},\,g \models P(t_1,\dots,t_n) \;&\text{iff}\; (\llbracket t_1\rrbracket_g,\dots,\llbracket t_n\rrbracket_g) \in I(P), \\ \mathcal{S},\,g \models \neg F \;&\text{iff}\; \text{not } \mathcal{S},\,g \models F, \\ \mathcal{S},\,g \models F \wedge G \;&\text{iff}\; \mathcal{S},\,g \models F \text{ and } \mathcal{S},\,g \models G, \\ \mathcal{S},\,g \models F \vee G \;&\text{iff}\; \mathcal{S},\,g \models F \text{ or } \mathcal{S},\,g \models G, \\ \mathcal{S},\,g \models F \to G \;&\text{iff}\; (\text{not } \mathcal{S},\,g \models F) \text{ or } \mathcal{S},\,g \models G, \\ \mathcal{S},\,g \models \forall X\, F \;&\text{iff}\; \text{for every } d \in D,\; \mathcal{S},\,g[X\!\mapsto\! d] \models F, \\ \mathcal{S},\,g \models \exists X\, F \;&\text{iff}\; \text{for some } d \in D,\; \mathcal{S},\,g[X\!\mapsto\! d] \models F, \end{aligned}$$

where $g[X\!\mapsto\! d]$ means "the assignment $g$ updated so that $X$ now points at $d$." This is not a paraphrase of the code; it is the code. The function holds (fol.py, lines 37–59) walks the same seven cases in the same order. The atom clause (lines 41–44) computes each argument as g.get(a, a) — look the term up in the assignment, or, failing that, use the term itself as a constant, which is precisely $\llbracket t\rrbracket_g$ — and tests membership in the extension:

if op == "atom":
    pred, args = f[1], f[2:]
    tup = tuple(g.get(a, a) for a in args)
    return tup in struct.rel(pred)

The connective clauses (lines 45–52) are the Boolean rows of the recursion. The implication line is worth pausing on, because it silently encodes a small theorem: imp is implemented (line 52) as (not holds(f[1], ...)) or holds(f[2], ...), which is the identity

$$F \to G \;\equiv\; \neg F \vee G$$

called material implication. The four connectives share one truth table, and every row of it appears somewhere in our world:

$F$	$G$	$\neg F$	$F\wedge G$	$F\vee G$	$F\to G$	a real witness for the $F\to G$ column
T	T	F	T	T	T	professor(alice) → researcher(alice)
T	F	F	F	T	F	student(carol) → professor(carol)
F	T	T	F	T	T	professor(carol) → researcher(carol) (vacuous)
F	F	T	F	F	T	professor(cmu) → researcher(cmu) (vacuous)

Only the second row makes an implication false: a true antecedent with a false consequent. Every other row, including both rows where the antecedent is false, makes it true — which is exactly why a universal implication passes so easily on individuals the rule does not really talk about.

The two quantifier clauses (lines 53–58) are the whole new idea, and because the domain is finite they become two Python built-ins. "For all" is a literal all(...) demanding every individual pass; "there exists" is a literal any(...) demanding at least one does:

if op == "all":
    var, body = f[1], f[2]
    return all(holds(body, struct, {**g, var: d}) for d in struct.domain)
if op == "exists":
    var, body = f[1], f[2]
    return any(holds(body, struct, {**g, var: d}) for d in struct.domain)

The expression {**g, var: d} is $g[X\!\mapsto\! d]$ made concrete: copy the current assignment and pin var to d. Because struct.domain is finite, both all(...) and any(...) scan a finite list and always terminate — the textbook definition of satisfaction, made runnable [1]. Running the module prints its two headline checks:

all professors are researchers: True
somebody advises bob: True

The academic world as a first-order structure: a domain of thirteen individuals and the predicate extensions over them, with a universal sentence checked by sweeping every individual, an existential satisfied by a single witness, and a conjunctive query answered by walking a two-hop relation chain. Original diagram by the authors, created with AI assistance.

Three sentences about the academic world

With the structure in hand, three sentences show the whole mechanism. Each is built with the constructors the companion provides (All, Exists, Imp, Atom, at fol.py lines 77–82) and decided by holds:

from fol import structure_from_kb, holds, All, Exists, Imp, Atom
s = structure_from_kb()

# ∀x (professor(x) → researcher(x))
print(holds(All("X", Imp(Atom("professor", "X"), Atom("researcher", "X"))), s))
# ∀x (student(x) → professor(x))
print(holds(All("X", Imp(Atom("student", "X"), Atom("professor", "X"))), s))
# ∃x advises(x, bob)
print(holds(Exists("X", Atom("advises", "X", "bob")), s))

True
False
True

Read them one at a time, sweeping the domain in the sorted order holds actually visits it.

∀X (professor(X) → researcher(X)) is true. The all(...) must confirm the implication at all 13 individuals; here is the complete sweep, each row a single call to holds with X pinned to that individual:

individual $d$	professor(d)	researcher(d)	professor(d) → researcher(d)
alice	T	T	T
bob	T	T	T
carol	F	T	T
cmu	F	F	T
dave	F	T	T
erin	F	T	T
logic	F	F	T
mit	F	F	T
ml	F	F	T
nesy	F	F	T
p1	F	F	T
p2	F	F	T
p3	F	F	T

At alice and bob the antecedent is true and, because the rule researcher ← professor (kb.py, line 75) fired during forward chaining, the consequent is true too, so the implication holds. At every other individual the antecedent professor is false, landing in rows three and four of the truth table, so the implication is vacuously true. All 13 pass, so all(...) returns True.

∀X (student(X) → professor(X)) is false, and here the mechanism reveals a shortcut. all(...) stops at the first individual that fails:

individual $d$	student(d)	professor(d)	student(d) → professor(d)	all verdict so far
alice	F	T	T	keep going
bob	F	T	T	keep going
carol	T	F	F	stop, return False

carol is a student but not a professor — the one false row of the implication table — so holds returns False at carol, all(...) short-circuits, and the remaining ten individuals are never examined. A single counterexample sinks a universal.

∃X advises(X, bob) is true, and here the dual shortcut fires immediately. any(...) stops at the first individual that succeeds, and the first individual in sorted order is alice:

individual $d$	advises(d, bob)	any verdict so far
alice	T	stop, return True

Because (alice, bob) sits in the advises extension, holds returns True at alice, any(...) short-circuits, and the other twelve individuals are never tried. A single witness lifts an existential.

The duality: one counterexample, one witness

The two shortcuts above are two faces of one law. A universal collapses on the first counterexample; an existential rises on the first witness. Formally, negating a "for all" turns it into a "there exists" of the negation:

$$\neg\,\forall X\, F \;\equiv\; \exists X\, \neg F .$$

The derivation is one line of unfolding the definitions: $\forall X\,F$ means $F$ holds at every $d \in D$; it is false exactly when $F$ fails at some $d$; and "$F$ fails at some $d$" is precisely "$\neg F$ holds at some $d$," which is $\exists X\,\neg F$. Our false universal is the duality in action. Saying "not every student is a professor" is the same as saying "some student is not a professor," and unfolding the implication ($\text{student} \to \text{professor} \equiv \neg\,\text{student} \vee \text{professor}$, whose negation is $\text{student} \wedge \neg\,\text{professor}$) names the witness outright: carol is a student and not a professor. The counterexample that sank the ∀ is the witness that satisfies the dual ∃. This is why holds needs only the two clauses all and any: negation converts either quantifier into the other, so implementing both is a convenience, not a necessity.

Conjunctive queries: the ∃∧ fragment

Real questions are rarely yes-or-no; we want the individuals that make something true. Those questions live in a small but central corner of first-order logic called the existential-conjunctive fragment (∃∧): a query is an existentially quantified conjunction of atoms, with some variables left free to be the answers. "Who does alice grand-advise?" asks for every individual $Z$ such that

$$\exists Y\;\big(\mathrm{advises}(\text{alice}, Y) \;\wedge\; \mathrm{advises}(Y, Z)\big),$$

the same advising-composed-with-advising chain the grandAdvisor rule captures (kb.py, line 79). We answer it by trying each individual as $Z$ and asking holds whether the inner existential is then satisfied:

from fol import structure_from_kb, holds, Exists, And, Atom
s = structure_from_kb()

# Who does alice grand-advise?  every Z with  ∃Y advises(alice,Y) ∧ advises(Y,Z)
answers = [z for z in s.domain
           if holds(Exists("Y", And(Atom("advises", "alice", "Y"),
                                     Atom("advises", "Y", z))), s)]
print(answers)

['carol', 'dave']

The loop is a double sweep, and tracing it exposes exactly why the answer is what it is. The outer loop fixes a candidate $Z$; the inner ∃Y sweeps every individual for a middle person $Y$. The left conjunct, advises(alice, Y), is true for only one value of $Y$, namely bob, because (alice, bob) is the sole pair in the advises extension whose first slot is alice. So the whole conjunction can succeed only when $Y = \text{bob}$, and it then reduces to asking whether advises(bob, Z) holds. bob advises carol and dave. Here is the outer sweep, with only the meaningful candidates spelled out and the rest collapsed:

candidate $Z$	is advises(bob, Z) true?	inner ∃Y result	in answer set?
alice	no	False	—
bob	no	False	—
carol	yes	True ($Y=$ bob)	✓
cmu	no	False	—
dave	yes	True ($Y=$ bob)	✓
erin	no	False	—
logic, mit, ml, nesy, p1, p2, p3	no	False	—

The answer set is carol and dave, matching the grandAdvisor extension exactly: (alice, carol) and (alice, dave). erin is not in the set, and the trace says precisely why: the only advising chain reaching erin is bob → carol → erin, so erin is two hops from bob (that is the derived fact grandAdvisor(bob, erin)), but three hops from alice. Grand-advising is exactly two hops, and alice is not two advising-hops from erin.

This exact shape — an existentially quantified conjunction returning a set of bindings — is the workhorse of database querying, the ∃∧ core underneath a SQL SELECT ... WHERE [3]. It is also, precisely, the task Volume 4 learns to answer under the name complex query answering over existential positive first-order (EPFO) queries: when the knowledge graph is incomplete, so that the honest holds loop would miss an answer nobody ever wrote down, a neural model predicts the answer set anyway. So this humble double loop over the domain is the symbolic ground truth those neural query answerers are trying to imitate on the facts we have, and to beat on the facts we do not.

The unsolved part

Two questions that sound alike have opposite fates. The first is model checking: given one fixed finite structure $\mathcal{S}$ and a sentence $F$, is $\mathcal{S} \models F$? That is exactly what holds computes, and it is fully decidable — the recursion bottoms out in finitely many membership tests, and each quantifier is a finite all(...) or any(...), so the procedure always halts with a definite yes or no. (Its cost is honest but bounded: a sentence with $k$ nested quantifiers over a domain of size $\lvert D\rvert$ can force on the order of $\lvert D\rvert^{k}$ individual checks, since each quantifier layer sweeps the whole domain inside the last.)

The second question replaces "this world" with "all worlds." A sentence is valid, written $\models F$, when it is true in every structure, of any size, including infinite ones — the first-order analogue of a propositional tautology. Here the wall goes up. First-order validity is undecidable: it was established in 1936 that no algorithm can always answer, with a guaranteed halt, whether an arbitrary first-order sentence is valid [1][2]. The best any procedure can do is semi-decide it. By Gödel's completeness theorem, a sentence is valid if and only if it is provable, $\models F$ iff $\vdash F$ (the single turnstile $\vdash$ reads "is provable"), so a proof search can enumerate every valid sentence and will eventually confirm any $F$ that truly is valid; but on an $F$ that is not valid, that same search may run forever, never able to close the case. Confirm-if-yes, possibly-loop-if-no: that asymmetry is the exact texture of undecidability.

The gap between the two questions is the gap between checking one finite world and quantifying over all conceivable ones, and it is not a defect in our code — it is a wall built into the logic itself. It is also why the series does not linger in full first-order logic. Volume 2 deliberately retreats to a tamer, decidable fragment, description logic in the EL family, trading away some expressive power for the guarantee that reasoning always terminates. Knowing where the wall stands is what turns that retreat from a surrender into a design choice.

Why it matters

Neuro-symbolic AI is largely the project of teaching neural networks to honor the kind of general knowledge only a quantified logic can state — "every professor is a researcher," "advising composes into grand-advising" — while staying robust to the missing facts and noisy inputs that pure symbolic matching handles badly. First-order logic gives that project its precise target: relations over named objects, quantified rules, and conjunctive queries with real answer sets. And the target is not vague. It is a specific, runnable procedure: the satisfaction recursion ⊨, sweeping a finite domain with all and any. Every later volume approximates one of this chapter's exact procedures with something differentiable — Volume 4's learned query answering approximates the conjunctive-query loop we traced over carol and dave. Know the crisp symbolic version first, down to which individual the all(...) stops on and which witness the any(...) seizes, and you can always say what the neural approximation is supposed to return.

Key terms

• Term — a name for an individual: either a constant or a variable.
• Constant — names one fixed individual (alice, p1, mit); lowercase, by the is_var convention.
• Variable — a placeholder that ranges over individuals (X, Y); uppercase. Bound under a quantifier, free otherwise.
• Predicate / arity — a symbol for a property (professor, unary) or a relationship (advises, binary); arity is its number of argument slots. Applied to terms it forms an atom, the smallest complete claim.
• Quantifier — ∀ ("for all") asserts a body of every individual; ∃ ("there exists") asserts it of at least one. Related by the duality ¬∀X F ≡ ∃X ¬F.
• Sentence — a formula with no free variables, so it has a definite truth value once a structure is fixed.
• Structure / model — a pair $(D, I)$: a domain $D$ of individuals plus an interpretation $I$ giving each predicate its extension; the world a sentence is checked against.
• Extension — the exact set of tuples $I(P) \subseteq D^n$ for which an $n$-ary predicate $P$ holds.
• Assignment — the function $g$ mapping each bound variable to the individual it currently stands for; extended by $g[X\!\mapsto\! d]$ under a quantifier.
• Satisfaction (⊨, holds) — whether a sentence is true in a structure; defined by recursion on formula shape, with quantifiers decided by trying every individual in the finite domain (all for ∀, any for ∃).
• Material implication — $F \to G \equiv \neg F \vee G$; false only when a true antecedent meets a false consequent, which is how holds implements imp.
• Model checking vs validity — $\mathcal{S}\models F$ in one finite world is decidable; $\models F$ in every world is undecidable (only semi-decidable via $\vdash$), which is why Volume 2 retreats to decidable description logic.
• Conjunctive query (∃∧) / EPFO — an existentially quantified conjunction of atoms with free answer variables; the core of database querying and Volume 4's complex-query-answering target over incomplete knowledge graphs.

Where this leads

We have said what it means for a sentence to be true in a world, defined the satisfaction relation exactly, and checked it by brute enumeration over a finite domain. But enumeration is not how a reasoner actually proves things, and it says nothing about worlds too large to walk end to end. It also quietly took the completed model as a gift — those $[23, 41, 47, 47]$ waves happened offstage. The next chapter, Inference and Proof: Chaining Facts into Conclusions, turns from meaning to mechanism: how a machine derives new facts by applying the academic world's Horn rules step by step, until nothing new appears — truth-by-checking giving way to truth-by-deriving.

---

Companion code: examples/logic/fol.py implements the Structure class and the satisfaction relation holds in pure standard-library Python, with the seven recursion clauses written out exactly as derived above; examples/logic/kb.py is the shared academic world. Run python3 examples/logic/fol.py to reproduce the two headline checks, and build a structure with structure_from_kb() to re-run every sweep and query traced in this chapter.