The Honest Verdict: What Foundations Buy You

📍 Where we are: Part V · The Verdict — Chapter 15. The previous chapter, The Running Example, showed one tiny academic world — alice, bob, carol, the papers p1 through p3, the advises and cites edges — carrying every method in this book at once. Now we step back from the machinery and ask the only question that matters at the end of a foundations volume: what did all of it actually buy us?

You have built a great deal from scratch: a forward-chaining engine, a proof-searching prover, a line-fitter, a neural network that cracks XOR, a translating embedding. This chapter adds no new tool; it takes inventory. The honest verdict is short, and it has three parts — two things you now hold, and one thing you do not. What makes the verdict honest rather than merely stated is that every claim in it is a line of committed code you can run: this chapter names the file and line behind each number, so nothing below is asserted on trust.

The simple version

Imagine you have spent a term learning two languages. One is a language of proof: every sentence is either provably true, provably false, or honestly unknown, and when it says "true" it can show you exactly why. The other is a language of resemblance: it never says "unknown," it always offers a best guess, and its guesses get eerily good — but it can never show its work, only its confidence. You are now fluent in both. What you cannot yet do is hold a single conversation that speaks both at once: proving when proof is possible and guessing when it is not, in the same breath. That missing bilingual sentence is neuro-symbolic AI, and everything after this volume is the attempt to write it.

What this chapter covers

• The verdict, stated plainly — you leave Volume 1 holding both halves of neuro-symbolic AI and a yardstick to judge them, but not the bridge that joins them.
• What is genuinely solid — a crisp, mechanical notion of proof run forward and backward, traced wave by wave to the exact 47-atom fixpoint; and learning that provably fits: a recovered line, a network that beats XOR, an embedding that ranks true facts as more plausible than false ones, each with real numbers tied line by line to the code.
• What stays wide open — joining an exact prover's guarantees to a learner's robustness without losing either.
• The three recurring tensions — exact versus robust, explainable versus opaque, complete versus scalable: the axes the whole series returns to, each grounded on a number the code prints.
• The evidence, made runnable — the twelve-check ledger in validate.py, mapped one row per claim to its file and line, whose exit code is the verdict on every claim this volume makes.
• Where to start — honest advice for a beginner: learn the crisp symbolic version of a task first, so you can always say what the neural approximation is supposed to return.

The verdict, stated plainly

Here is the whole finding in three clauses. First, you now hold both halves of neuro-symbolic AI — the term names the program of joining neural learning with symbolic reasoning [1]. One half is exact but brittle: logic derives only what genuinely follows and can prove each step, but it falls silent the instant a question steps outside its rules. The other half is robust but opaque: a learned model answers any question you can pose and generalizes past its data, but it can be confidently wrong and cannot show why. Second, you hold the yardstick to judge them — a shared vocabulary (proofs, fixpoints, gradients, embeddings) and a single shared world (the academic knowledge base, 23 asserted facts closed under 7 rules into a 47-atom model) on which both halves were run head to head. Third — and this is the honest part — you do not yet hold the bridge. Nothing in Volume 1 joins the guarantees of the prover to the robustness of the learner. That the two halves fit the same world is what makes the gap between them visible; closing it is what the remaining four volumes are for [2].

The end-of-volume balance: an exact-but-brittle symbolic half and a robust-but-opaque neural half, weighed on one shared academic world, with the bridge between them still a dashed gap — and a twelve-check ledger certifying that everything on both pans really runs. Original diagram by the authors, created with AI assistance.

What is genuinely solid

Two results in this volume are not hand-waving; they are mechanical, reproducible, and guarded by code. We take them one at a time and, this time, watch the mechanism actually move.

The first solid result: proof, run both directions

The symbolic pan of the balance rests on a crisp notion of proof, and it runs both ways. Run forward, reasoning is repeated application of the immediate-consequence operator $T_P$ — read "T-sub-P," the map that takes a set of facts, fires every rule whose body is currently satisfied, and returns the input plus every head those rules conclude in one step. Written out, for a set $S$ of atoms (an atom is one ground fact such as advises(alice, bob)),

$$T_P(S) \;=\; S \,\cup\, \{\, \text{head} \;:\; \text{rule (head} \leftarrow \text{body) fires with its body true in } S \,\}.$$

The symbol $\cup$ is set union ("everything in either set"), the colon inside the braces reads "such that," and the whole expression is exactly the function t_p in forward_chain.py (lines 42–49): out = set(facts) seeds $S$, then each rule head that matches gets added. A fixpoint of $T_P$ is a set the operator maps to itself, $T_P(S) = S$: applying the rules produces nothing you did not already have. The least fixpoint, written $\mathrm{lfp}(T_P)$ ("lfp" = least fixpoint, the smallest such set), is the meaning of the program, and the loop in least_fixpoint (lines 52–63) reaches it by iterating $T_P$ from the base facts until two successive rounds are identical (if nxt == current: return).

Here is that climb, wave by wave, on the running example. Starting from the 23 asserted facts, each row is one application of $T_P$. Two symbols appear in the table below: ⟹ reads "therefore / implies," and ∧ reads "and."

wave	operator	new atoms this wave, and why	cumulative size
0	— (asserted)	the 23 base facts (5 class memberships, 4 advises, 4 authored, 2 cites, 5 affiliated, 3 about)	23
1	$T_P$ on 23	+5 researcher (professor or student ⟹ researcher), +3 grandAdvisor (advises composed with advises), +8 colleague (share an institution), +2 citesTransitively (base case, one per cites edge)	41
2	$T_P$ on 41	+5 person (researcher ⟹ person), +1 citesTransitively(p3, p1) (recursive step: cites(p3, p2) ∧ citesTransitively(p2, p1))	47
3	$T_P$ on 47	nothing new: $T_P(S) = S$, so the fixpoint is confirmed	47

Those cumulative sizes are exactly what forward_chain.py prints: sizes per round: [23, 41, 47, 47], then 47 atoms total, 24 derived. The 24 derived atoms decompose with no remainder as 5 researcher + 5 person + 3 grandAdvisor + 8 colleague + 3 citesTransitively, and $23 + 24 = 47$.

Two features of that trace are the whole reason a fixpoint is needed rather than a single pass. First, person(alice) cannot appear until wave 2, because the rule person(X) ← researcher(X) needs researcher(alice), which is itself only derived in wave 1: consequences feed further consequences. Second, citesTransitively(p3, p1) also waits for wave 2, because the recursive rule citesTransitively(A, C) ← cites(A, B), citesTransitively(B, C) feeds its own head back into its own body — the closure of the citation chain p3 → p2 → p1 is genuine recursion, not a lookup. The fourth pass adding nothing (sizes[-1] == sizes[-2], i.e. 47 == 47) is the engine proving to itself that it is finished, and the check _fc_stable (validate.py, lines 52–57) pins exactly that: it asserts model == fc.t_p(model, rules), the literal statement $T_P(S) = S$.

Run the other direction and the same facts fall out goal-first. The SLD prover in sld.py starts from a query, asks "which rule could conclude this, and what would its body then require," and returns an auditable proof tree rather than a bare yes. Asking it for grandAdvisor(alice, carol) (sld.py, prove, lines 63–75; rendered by Proof.render, lines 29–34) prints:

grandAdvisor(alice, carol)
  advises(alice, bob)
  advises(bob, carol)

Read it as a derivation you can check by eye: the goal grandAdvisor(alice, carol) is established by the single rule grandAdvisor(X, Z) ← advises(X, Y), advises(Y, Z) with X = alice, Y = bob, Z = carol, and each leaf, advises(alice, bob) and advises(bob, carol), is a base fact needing no further proof. The deep fact linking the two directions is that they agree: everything the forward engine derives, the backward prover can also prove. The check _fc_sld_agree (validate.py, lines 77–82) states it with no wiggle room — it walks every one of the 47 atoms in the model and asserts sld.provable(atom) for each:

@check("forward and backward chaining agree on membership")
def _fc_sld_agree():
    facts, rules = program()
    model = fc.least_fixpoint(facts, rules)
    for atom in model:
        assert sld.provable(atom), f"SLD failed to prove derived atom {atom}"

This makes completeness concrete and executable: every atom the forward engine derives, the backward prover can also prove (the whole model is a subset of what SLD can prove), and the exit code turns red the day that stops being true. The mirror half, soundness — the prover proves only atoms that are in the model, nothing spurious — is not what this loop iterates; it follows from the fact that SLD resolution is sound for definite Horn clauses, and the chapter spot-checks it with the single negative assert not sld.provable(("advises", "alice", "carol")) at line 74, a non-fact the prover correctly refuses to derive.

The second solid result: learning that provably fits

The neural pan rests on learning that provably fits. This is not "the model looked good"; it is an assertion that either holds or fails the build. Three faces of "fit a function to data," each demonstrated on the one world we can inspect by eye.

The first is linear regression. Gradient descent — nudging parameters downhill along the gradient, the vector of partial slopes that points in the direction of steepest increase of the error, so its negative points downhill — recovers the slope of a line. Running fit_line (learning.py, lines 22–37) on the five points in the file prints line: y = 1.990 x + 0.050 (loss 44.182 -> 0.0214): the true slope near 2.0 recovered, and the mean-squared-error loss driven down from 44.182 to 0.0214, a fall of more than a hundredfold. The check _learning (validate.py, lines 133–141) guards both facts at once, assert l1 < l0 / 100 and assert abs(w - 2.0) < 0.1.

The second is a logistic classifier grounded directly in the running example. Its two features are read straight off the advises relation by advise_features (learning.py, lines 49–64): for each person, the out-degree (how many people they advise) and the in-degree (how many advise them). Professors are labeled 1, students 0. Here is the exact table the code builds:

person	out-degree	in-degree	label
alice	1	0	prof (1)
bob	2	1	prof (1)
carol	1	1	student (0)
dave	0	1	student (0)
erin	0	1	student (0)

Neither column alone separates the groups: carol (a student) and alice (a professor) share an out-degree of 1, and bob (a professor) and the students all have in-degree 1. The classifier must lean on both, and fit_logistic (lines 67–85) finds the combination by gradient descent on the cross-entropy loss, printing logistic: weights=[7.75, -8.59] bias=-2.76 loss=0.010 with all five people labeled correctly. The signs are exactly the qualitative rule you would hope for: the out-degree weight is large and positive (advising people is evidence of being a professor), the in-degree weight is large and negative (being advised is evidence of being a student). The same check _learning asserts preds == y.

The third is XOR, the exclusive-or pattern (output 1 when the two inputs differ, 0 when they match) that no straight line can separate. A linear classifier provably cannot get more than three of the four cases right, and neural.py confirms it: linear classifier on XOR: [1, 1, 1, 1] ... correct: 2 / 4. Add one hidden layer — a 2-4-1 multi-layer perceptron trained by backpropagation in train_mlp (neural.py, lines 31–67) — and all four cases come out right: 2-4-1 MLP on XOR: [0, 1, 1, 0] ... correct: 4 / 4 (loss 0.0003). The check _neural (validate.py, lines 145–154) states both halves: assert lin_correct < 4 for the line and assert mlp == [int(v) for v in neural.XOR_Y] for the network.

    params, loss = neural.train_mlp(neural.XOR_X, neural.XOR_Y)
    mlp = [neural.predict_mlp(params, x) for x in neural.XOR_X]
    assert mlp == [int(v) for v in neural.XOR_Y], mlp   # MLP gets all four

The third solid result: meaning as geometry

The same downhill trick, applied to symbols, gives a from-scratch TransE embedding in which a relation is a translation: a true triple (head $h$, relation $r$, tail $t$) should satisfy $\mathbf{h} + \mathbf{r} \approx \mathbf{t}$, where the bold letters are the two-coordinate vectors placed for each entity and relation, and $\approx$ reads "is approximately equal to." The plausibility of a triple is measured by how badly that approximation fails, namely the distance (embeddings.py, score, lines 79–82):

$$\text{score}(h, r, t) \;=\; \big\lVert\, \mathbf{h} + \mathbf{r} - \mathbf{t} \,\big\rVert \;=\; \sqrt{\textstyle\sum_{i} (h_i + r_i - t_i)^2}.$$

Here $\lVert \cdot \rVert$ is the Euclidean length of a vector (the square root of the sum of its squared coordinates), $\sum_i$ sums over the coordinates $i = 1, 2$, and $\sqrt{\cdot}$ is the ordinary square root. Lower means the translation fits better, so a good embedding puts true triples below false ones. After training (seeded, so reproducible), embeddings.py prints exactly that ordering:

triples scored	mean / value	reading
true triples (all binary facts)	1.609	fit the $\mathbf{h} + \mathbf{r} \approx \mathbf{t}$ pattern well
corrupted triples (tail replaced)	2.737	fit it worse — a clean gap of about 1.13
advises(alice, bob) (a real edge)	0.399	scores low: geometry believes it
advises(alice, erin) (a non-edge)	0.929	scores higher: geometry doubts it

The check _embeddings (validate.py, lines 158–165) asserts both the aggregate gap, assert true_s < corr_s (1.609 below 2.737), and the single-edge ordering, assert s_true < s_false (0.399 below 0.929). Regression, a network, and a knowledge-graph embedding — three faces of "fit a function to data," each demonstrated on the one world we can inspect by eye, and each guarded by an assertion that either passes or reddens the build.

What stays wide open

Now the gap. Each half is excellent at exactly what the other cannot do. The prover is sound and complete for its logic — it derives all and only what follows — but it is silent about everything else. Ask it whether advises(alice, erin) and it simply refuses: that edge is neither asserted nor derivable by any rule, so the prover falls silent. The check _sld_answers spot-checks the analogous non-fact advises(alice, carol) in one line, assert not sld.provable(("advises", "alice", "carol")) (validate.py, line 74): for either edge the prover answers "not derivable," never "unlikely." It has no notion of degree. The embedding is the mirror image — never silent, handing back a number for any triple you can name, but never certain, because any single number can be wrong. It scores the non-edge advises(alice, erin) at 0.929: higher than the real edge's 0.399, so the ranking is right, but 0.929 is a hint, not a verdict, and nothing in the geometry promises it. The unsolved engineering problem of the entire field is to fuse the two: to keep the prover's guarantees where a proof exists and fall back on the learner's robust guess where it does not, in one system, without the fusion quietly destroying either property. Volume 1 shows the two poles with unusual clarity precisely because it never pretends to have joined them.

The three tensions the whole series returns to

The gap is not one disagreement but three, and naming them is half of thinking clearly about neuro-symbolic AI. Every method in the volumes ahead can be located by where it sits on these three axes [3], and each axis is anchored by a number this volume actually prints.

Exact versus robust. Forward chaining is exact — the 47 atoms are provably right and provably complete for the rules, and the trace [23, 41, 47, 47] shows the closure reached and certified stable — but brittle: one fact outside the rule set and it says nothing. TransE is robust — it degrades gracefully to a plausibility (0.929 for the non-edge) instead of a refusal — but inexact: that distance is a hint, not a verdict. You can have the guarantee or the graceful failure; this volume never had both at once.

Explainable versus opaque. The SLD proof tree is the explanation — the two-line derivation of grandAdvisor(alice, carol) from advises(alice, bob) and advises(bob, carol) is a chain a human can read and check, and the check _sld_proof (validate.py, lines 61–66) asserts both leaves appear in it. The weights [7.75, -8.59] that let the classifier separate professors from students, or the hidden-layer parameters that solve XOR, explain nothing on their face; they are a working answer with no readable reason. Symbolic reasoning is transparent by construction; learned models are opaque by default.

Complete versus scalable. Fixpoint iteration is complete — it reaches the whole least model, all 47 atoms, and the concept hierarchy it induces is a genuine order: the check _orders confirms professor ⊑ researcher ⊑ person (where ⊑ reads "is subsumed by," i.e. "is a subclass of"), with join("professor", "student") == "researcher" (their least common superclass) and meet("professor", "student") is None (no common subclass). That completeness is exactly what can explode on a real knowledge base, where the closure may be astronomically larger than the input. Embeddings scale to graphs with millions of edges precisely because they never try to be complete; they approximate, trading the guarantee for the graceful number. Coverage and cost pull against each other.

No single method in this book wins all three axes. That is not a failure of the book — it is the shape of the problem, and the reason the field exists.

The evidence, made runnable

Every number quoted in this volume is guarded by a companion program, validate.py, built on one discipline: requirements are tests. Each claim the book makes is one competency check — a plain assertion over the running example, registered by the tiny check decorator (validate.py, lines 29–33) — and the process's exit code is the verdict. The main loop (lines 168–183) runs every check, counts the passes, and returns 0 only if all of them hold:

    total = len(CHECKS)
    print(f"\nlogic companion: {passed}/{total} competency checks passed")
    return 0 if passed == total else 1

There are twelve checks, and they map one-to-one onto the volume's central claims. Here is the whole ledger, each row tied to the file and line that runs it and the number or fact it certifies:

#	competency check	where it lives	what it certifies
1	forward chaining reaches the least fixpoint	validate.py 37–49	5 researchers, 3 grandAdvisor pairs, 3 citesTransitively, 8 colleagues — the 24 derived atoms
2	forward chaining terminates (fixpoint is stable)	validate.py 52–57	[23, 41, 47, 47]; T_P(model) == model
3	SLD proves a role-chain goal with a proof tree	validate.py 61–66	the grandAdvisor(alice, carol) tree contains both advising leaves
4	SLD query answering matches the bindings	validate.py 69–74	colleague(alice, Who) = [bob]; advises(alice, carol) not provable
5	forward and backward chaining agree	validate.py 77–82	every one of the 47 atoms is SLD-provable
6	propositional truth tables, validity, SAT, entailment	validate.py 86–93	a tautology is valid, a contradiction unsatisfiable, entailment holds
7	FOL satisfaction over the structure	validate.py 97–106	every professor is a researcher; not every student is a professor
8	relation composition and transitive closure	validate.py 110–119	advises ∘ advises (advising composed with advising) = 3 grand-pairs; cites⁺ (the transitive closure of cites) = 3 pairs; affiliated is functional
9	the concept hierarchy is a partial order	validate.py 123–129	professor ⊑ researcher ⊑ person, correct joins and meets
10	linear and logistic regression fit	validate.py 133–141	loss falls over 100×, slope within 0.1 of 2.0, all 5 people correct
11	a hidden layer learns XOR where a line fails	validate.py 145–154	linear under 4 of 4; the 2-4-1 MLP gets 4 of 4
12	TransE scores true triples above corrupted	validate.py 158–165	1.609 below 2.737; 0.399 below 0.929

Running the harness prints the full ledger and its bottom line:

PASS  forward chaining reaches the least fixpoint (derived facts)
PASS  forward chaining terminates (fixpoint is stable)
PASS  SLD proves a role-chain goal with a proof tree
PASS  SLD query answering matches the intended bindings
PASS  forward and backward chaining agree on membership
PASS  propositional truth tables, validity, satisfiability, entailment
PASS  FOL satisfaction over the running example structure
PASS  relation composition and transitive closure
PASS  the concept hierarchy is a partial order with correct joins/meets
PASS  linear and logistic regression fit the data by gradient descent
PASS  a hidden layer learns XOR where a linear model fails
PASS  TransE embeddings score true triples above corrupted ones

logic companion: 12/12 competency checks passed

That last line — logic companion: 12/12 competency checks passed — is the volume's real verdict, and it is the same "requirements equal tests" discipline the later volumes reuse. It means the claims across the fourteen chapters this verdict summarizes are not asserted on trust; they are executable, and the day one of them stops being true, main returns 1 and the build turns red.

Advice for starting neuro-symbolic AI

If you take one working habit from this volume, take this: learn the crisp symbolic version of a task before you reach for the neural one. The reason is practical, not purist. Once you can state what a sound and complete answer would be — the exact 47 atoms, the specific two-leaf proof tree, the true set of advising edges — you have a ground truth to hold the neural approximation against. You can then say precisely what the learner is supposed to return, measure how far it drifts, and know whether a wrong guess is a tolerable one. The TransE run makes the point concretely: because we already know advises(alice, erin) is not an edge, the score 0.929 becomes meaningful — we can see it is correctly ranked above the real edge's 0.399, and we can also see that 0.929 alone would tell us nothing without the symbolic truth to compare it to. Skip that step and a fluent model will hand you confident answers with nothing to check them against, and you will have no way to tell a lucky guess from a learned truth. The symbolic half is not the old way that learning replaced; it is the specification the learning half is trying to approximate.

The unsolved part

The honest open question is whether the bridge can be built without a trade. Every partial join the field has tried so far seems to pay for one property with another: make the learner respect a logical rule and you often lose scalability; make the reasoner tolerate noise and you often lose the guarantee that made it worth trusting [3]. Volume 1 cannot tell you the trade is unavoidable — and it would be a mistake to declare it so. It only establishes, rigorously and on one shared world, that the two halves have complementary strengths and that no free lunch is yet in hand: the prover is complete but silent outside its rules, the embedding is fluent but never certain, and the twelve checks that certify each of them are green precisely because each half is measured on the task it is built for, not the other's. Whether a single system can be exact where proof is possible, robust where it is not, explainable, complete and scalable all at once is genuinely open — and it is the question the next four volumes exist to attack, not to concede.

Why it matters

The whole neuro-symbolic program rests on a bet that the two traditions in this volume are complementary rather than competing — that logic's guarantees and learning's reach can be combined into something neither achieves alone. This chapter is the honest statement of why the bet is not yet won: you have seen both halves work, on the same world, with the same yardstick, and you have seen the seam between them stay open. Holding that picture clearly — two solid halves, one unbuilt bridge, three tensions that will not vanish — is the single most useful thing a beginner can carry into the rest of the series. It keeps you from mistaking a robust guess for a proof, or a proof for a robust system, and it tells you exactly what a real neuro-symbolic method must deliver to count as progress: not a higher number on one pan, but a system that earns a green check on both.

Key terms

• Neuro-symbolic AI — the program of joining neural learning with symbolic reasoning so a system can both generalize and prove; the subject of the whole series.
• Both halves — the exact-but-brittle symbolic half (proofs, fixpoints) and the robust-but-opaque neural half (gradients, embeddings), shown in this volume on one shared world.
• Immediate-consequence operator $T_P$ — the map that fires every rule whose body is currently true and adds the heads; forward chaining is repeated application of it.
• Fixpoint / least fixpoint — a set the rules map to itself, $T_P(S) = S$; the forward engine reaches the least one (47 atoms via [23, 41, 47, 47]) and knows it is done when a pass adds nothing.
• Proof tree — the auditable, human-readable chain of steps a backward prover returns, e.g. deriving grandAdvisor(alice, carol) from advises(alice, bob) and advises(bob, carol).
• Sound and complete — derives all and only what follows; the property the symbolic half has and the neural half does not.
• TransE score — the distance $\lVert \mathbf{h} + \mathbf{r} - \mathbf{t} \rVert$; lower means a more plausible triple, so true triples (mean 1.609) rank below corrupted ones (2.737).
• Never silent, never certain — the embedding's mirror-image trade: it scores every triple you can name but any score can be wrong.
• The three tensions — exact versus robust, explainable versus opaque, complete versus scalable: the axes on which every later method can be located.
• Competency check — one executable assertion over the running example; the volume's claims equal its tests, and the exit code is the verdict.
• The bridge — the still-unbuilt join that would keep the prover's guarantees where proof exists and the learner's robustness where it does not.

Where this leads

Volume 1 hands you the two halves, the vocabulary, and the world to compare them on — and one unanswered question: can the two cultures be made one? The next volume, Volume 2 — Symbolic Reasoning, develops the symbolic pillar in full depth: ontologies that give the academic world a principled vocabulary, description logic that lets you say far more than Horn rules could, and the reasoners that decide it. It is the same knowledge base, examined through a sharper lens — the first of four volumes that, one at a time, try to turn this chapter's open verdict into a built bridge.