The Honest Verdict: What Symbols Guarantee

📍 Where we are: Part VII · The Verdict — Chapter 22. Open-World and Inconsistency showed how a reasoner treats an unknown fact as merely unproven rather than false, and how a single contradiction can poison every entailment; now we close the volume by taking inventory of exactly what all this symbolic machinery does — and does not — buy you.

This chapter adds no new mechanism. It audits the whole volume. Across twenty-one chapters you built ontologies, normalized a TBox (the terminological box, a schema's concept and role axioms), ran the EL completion algorithm, re-expressed it as Datalog, chased existential rules to certain answers, and annotated facts with provenance and confidence. The honest verdict is short, and it has two halves: a column of things symbols genuinely guarantee, and a column of things they cannot. What makes the verdict honest rather than merely asserted is that every number below is a line of committed code you can run — this chapter names the file and line behind each one.

The simple version

Imagine hiring a meticulous auditor to sign off your accounts. They will certify only what the books actually say, show you the exact receipt behind every figure, and refuse to invent a number when a receipt is missing — never "probably fine," only "shown" or "not shown." That refusal to guess is both their great strength and their hard limit: you can trust every stamp they give, but they will hand you a blank where a shrewd guess would have helped. Symbolic reasoning is that auditor. This chapter is the moment we weigh what the stamp is worth.

What this chapter covers

• The verdict, stated plainly — symbols buy you correctness you can trust and explain, on knowledge you must write down and keep consistent.
• What is genuinely solid — sound, complete, polynomial-time EL classification that matches HermiT; certain answers computed over the chase; provenance and confidence that record where a fact came from and how sure it is — each with a companion module behind it.
• What stays out of reach — brittleness to missing or noisy facts, no learning from data, hand-set rather than calibrated confidence, and undecidable termination once existentials enter.
• The four recurring tensions — expressivity vs tractability, open- vs closed-world, complete vs scalable, exact vs robust: the axes Volume 3 and beyond must reconcile.
• The evidence, made runnable — the 13-check ledger in validate.py, one row per claim, whose exit code is the verdict on everything the volume asserts.
• Honest advice — model the crisp symbolic version of a task first, so you always know what a learned approximation is supposed to return.

The verdict, stated plainly

Here is the whole finding in one line: symbols buy you correctness you can trust and explain, on knowledge you must write down and keep consistent [1]. Unpack it into its two clauses and both are load-bearing. Correctness you can trust and explain is the reward: when an EL reasoner says Professor ⊑ Person, it is not a strong hunch but a theorem, true in every model of the ontology, and it can hand you the derivation. Knowledge you must write down and keep consistent is the price: a reasoner reasons only over axioms someone authored, and the instant two of those axioms contradict, classical entailment collapses into deriving everything. Symbols do not read the world; they read your model of it. Everything solid in this volume lives inside that bargain, and everything out of reach lives outside it.

The end-of-volume ledger: a left column of guarantees each certified by a green competency check, a right column of things symbols cannot deliver, four tension sliders beneath, and a dashed arrow handing the open right column to the neural pillar. Original diagram by the authors, created with AI assistance.

What is genuinely solid

Three results in this volume are not rhetoric; they are mechanical, reproducible, and each guarded by a check that either passes or reddens the build.

Classification is sound, complete, and polynomial — and it matches HermiT

The centerpiece guarantee of description logic is classification: computing every subsumption $A \sqsubseteq B$ (read "$A$ is subsumed by $B$," i.e. every $A$ is necessarily a $B$) that the axioms force. For the academic ontology the from-scratch completer in el_completion.py returns a set $\mathrm{cl}(\mathcal{T})$ of subsumption pairs, and the guarantee is an "if and only if":

$$(A, B) \in \mathrm{cl}(\mathcal{T}) \quad\Longleftrightarrow\quad \mathcal{T} \models A \sqsubseteq B.$$

Left-to-right is soundness — every derived subsumption really holds in every model. Right-to-left is completeness — every entailed subsumption is derived, none missed. Check 2 (validate.py lines 51-63) pins the exact answer set, the eight pairs including the headline ("Professor", "Person"), so the day soundness or completeness breaks the assertion fails. And because the classifier is homegrown, the volume corroborates it against an independent oracle: reasoners.py rebuilds the same ontology in owlready2 and runs HermiT (a complete OWL 2 DL reasoner), which agrees on all 8 subsumptions and both unsatisfiable concepts.

The second half of the guarantee is tractability. EL — the lightweight description logic keeping exactly conjunction ⊓ and the existential ∃ — was engineered so classification runs in PTIME (polynomial time) in the size of the ontology [2]. The reason is visible in the completion: the saturated subsumer relation $S$ can hold at most $|N_C|^2$ pairs and the role relation $R$ at most $|N_R| \cdot |N_C|^2$ (with $N_C$ the concept names and $N_R$ the role names), so the monotone climb can only add polynomially many facts before it must halt. Check 5 (validate.py lines 83-90) certifies exactly that shape — monotone growth to a stable round:

    rounds = res["rounds"]
    for (s0, r0), (s1, r1) in zip(rounds, rounds[1:]):
        assert s1 >= s0 and r1 >= r0, rounds       # monotone growth
    assert rounds[-1] == rounds[-2], rounds        # last round added nothing
    assert rounds[0] == (23, 0) and rounds[-1] == (39, 7), rounds

On the academic world that climb settles in three rounds from $(23, 0)$ to $(39, 7)$ — the fixpoint of Chapter 7's Kleene climb, now saturating an ontology instead of a rule base. Soundness, completeness, and a polynomial bound, all three at once: that is the guarantee no purely neural model can currently make about its own outputs.

The chase computes certain answers

Query answering under an open world gets its own guarantee. Given a conjunctive query $Q(\bar x)$, the certain answers are the tuples true in every model of the ontology:

$$\mathrm{cert}(Q, \mathcal{O}) \;=\; \{\, \bar a : \mathcal{O} \models Q(\bar a) \,\} \;=\; \{\, \bar a : \bar a \in Q^{\mathcal{I}} \text{ for every model } \mathcal{I} \,\}.$$

Chapter 20's chase makes this computable: it fires the existential rules (tuple-generating dependencies, TGDs) until saturated, producing a single universal model $U$ that maps by homomorphism into every other model. A tuple $\bar a$ is then a certain answer exactly when there is a homomorphism $h$ from the body of $Q$ into $U$ with $h(\bar x) = \bar a$ that fixes every constant. Crucially, an invented null can never be a certain answer, because a different model could have chosen a different witness. Check 9 (validate.py lines 129-135) states it with no wiggle room:

@check("certain answers are computed by homomorphism over the chase")
def _certain_answers():
    r = chase.chase(chase.CHASE_INSTANCE, chase.TERMINATING_TGDS, restricted=True)
    body, avars = chase.Q_ADVISES_STUDENT
    ca = chase.certain_answers(body, avars, r["instance"])
    assert ca == {("alice",), ("bob",)}, ca      # both professors, only constants
    assert chase.query_holds(body, r["instance"])

For "who advises a student?" the certain answers are alice and bob — both named constants, no invented advisor — and the comment says precisely why: only constants survive the every-model test.

Provenance and annotations track where facts come from and how sure we are

The third solid result is that a symbolic derivation can carry metadata alongside truth. annotated.py recomputes the same reachability fact through different semirings, and check 11 (validate.py lines 147-156) certifies that the fact reach(p3,p1) carries the provenance polynomial t + r·s — meaning it holds either by the single edge $t$ or by the two edges $r$ and $s$ together — with the which-, why-, and Boolean provenance all agreeing. Confidence rides the same rails: on the interval $[0, 1]$, conjunction is meet $= \min$ and disjunction is join $= \max$, so a fact's confidence is the best over derivation paths of the weakest edge on a path. Check 12 (validate.py lines 159-165) pins it:

    # max over paths of min over edges: max(0.5, min(0.9, 0.8)) = 0.8
    assert ann.provenance_of(fact, ann.CONFIDENCE) == 0.8
    assert ann.conf_meet(0.9, 0.8, 0.5) == 0.5    # conjunction ⊓
    assert ann.conf_join(0.9, 0.8, 0.5) == 0.9    # disjunction ⊔

You get an auditable record of where a conclusion came from and a principled combination of how sure each input was — the raw material of trust and traceability.

What stays out of reach

Now the other column, and each gap is the shadow of a strength.

Brittleness to missing and noisy facts. The open-world assumption is not robustness; it is principled abstention. Delete advises(bob, carol) and the reasoner does not degrade gracefully to "probably still advises" — it simply stops entailing anything that needed it, and reports no error. Add one wrong assertion that makes TenuredStudent inhabited and, because Professor ⊓ Student ⊑ ⊥, the model turns inconsistent and classical entailment derives everything. Symbols are exact on the knowledge you wrote and silent — or catastrophic — on the knowledge you got wrong.

No learning. Nothing in this volume induces an axiom from data. Every subsumption, role chain, and disjointness was authored by hand; the completer only unfolds their consequences. A reasoner cannot notice that advisors tend to co-author with advisees and propose the rule — it can only check a rule you already wrote.

Confidence is hand-set, not calibrated. The 0.8 above is real arithmetic over the $[0, 1]$ lattice, but the inputs 0.9, 0.8, 0.5 were typed into the ontology, not fitted to observed frequencies. The combination is principled; the priors are stipulated. A symbolic confidence answers "given these numbers, how do they combine," never "are these the right numbers."

Termination is undecidable in general. Once existentials can feed their own output back into their input, the chase can run forever. Check 10 (validate.py lines 138-143) captures a rule that invents a fresh advisor for every researcher, then a fresh advisor for that advisor, and never stops — the harness only bounds it with a 50-firing cap. Whether an arbitrary set of TGDs has a terminating chase, and whether a query is entailed, is undecidable in general; the decidable fragments (weakly-acyclic, guarded, sticky) buy their guarantee back by giving up expressive power.

The four tensions the whole series returns to

The gaps are not four unrelated complaints; they are four axes, and every method ahead can be located on them [3]. Each is anchored by a number this volume actually prints.

tension	the pole this volume showed	the opposing pole	what pays for the trade
expressivity vs tractability	EL++: ⊓, ∃, ⊥, role chains — PTIME, 3-round fixpoint	SROIQ / OWL 2 DL — worst-case doubly-exponential	the OWL profiles [2]
open-world vs closed-world	certain answers over the chase (alice, bob only)	Datalog least model, waves [23, 41, 47, 47]	which assumption the task actually wants
complete vs scalable	completion reaches the whole model, 39 sco atoms	the closure can explode on real ontologies	EL reasoners (ELK) engineered to stay polynomial
exact vs robust	8 subsumptions, exactly right, or silent	vectors that always answer but only approximate	Volume 3, the neural pillar

No method in this volume wins all four. That is not a defect of the volume; it is the shape of the problem, and the reason the neuro-symbolic field exists.

The evidence, made runnable

Every number quoted across Volume 2 is guarded by validate.py, built on one discipline: requirements are tests. Each claim is a competency check — a plain assertion over the academic ontology, registered by a tiny decorator (validate.py lines 28-33) — and the process's exit code is the verdict. The main loop (lines 189-204) runs every check and returns 0 only if all hold:

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

There are thirteen checks, one per central claim. Here is the whole ledger, each row tied to the file and line that runs it:

#	competency check	where it lives	what it certifies
1	TBox normalizes to the four EL normal forms (+ role chains)	validate.py 36-47	14 axioms become 16 normal-form axioms, 2 fresh names; forms nf1×6, nf2×2, nf3×3, nf4×4, chain×1
2	EL completion classifies the hierarchy correctly	validate.py 51-63	the 8 subsumptions, including Professor ⊑ Person
3	the bottom rule detects the unsatisfiable concepts	validate.py 66-74	TenuredStudent, TenuredStudentAdvisor ⊑ ⊥; the other 8 concepts satisfiable
4	the role-chain rule derives grand-advising	validate.py 77-80	the pair (Dean, Student) is in grandAdvisor
5	saturation is monotone and reaches a stable fixpoint	validate.py 83-90	rounds grow from (23, 0) to (39, 7); the last adds nothing
6	Datalog reproduces the Volume 1 model	validate.py 94-104	waves [23, 41, 47, 47]; 5 researchers, 3 grandAdvisor, 3 citesTransitively, 8 colleagues
7	EL-as-Datalog agrees with the completion	validate.py 107-115	39 sco + 7 rel atoms; same subsumptions as el_completion
8	restricted chase beats the oblivious chase	validate.py 119-126	restricted 3 nulls / 3 steps vs oblivious 5 nulls / 5 steps
9	certain answers by homomorphism over the chase	validate.py 129-135	certain answers are alice and bob — constants only
10	the non-terminating chase diverges	validate.py 138-143	never terminates; 50 nulls at the step cap
11	the provenance polynomial of reach(p3,p1) is t + r·s	validate.py 147-156	polynomial t + r·s; which / why / Boolean agree
12	annotated/fuzzy confidence combines by the [0,1] lattice	validate.py 159-165	max(0.5, min(0.9, 0.8)) = 0.8; meet 0.5, join 0.9
13	Allen's 13 interval relations classify and compose	validate.py 169-186	13 relations; meets ∘ meets yields before; before ∘ before-inverse yields all 13

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

PASS  TBox normalizes to the four EL normal forms (+ role chains)
PASS  EL completion classifies the concept hierarchy correctly
PASS  the bottom rule detects the unsatisfiable concepts
PASS  the role-chain rule derives grand-advising
PASS  saturation is monotone and reaches a stable fixpoint
PASS  Datalog reproduces the Volume 1 academic-world model
PASS  EL-as-Datalog agrees with the from-scratch completion
PASS  restricted chase terminates with fewer nulls than the oblivious chase
PASS  certain answers are computed by homomorphism over the chase
PASS  the non-terminating chase diverges (bounded by a step cap)
PASS  the provenance polynomial of reach(p3,p1) is t + r·s
PASS  annotated/fuzzy confidence combines by the [0,1] lattice
PASS  Allen's 13 interval relations classify and compose correctly

symbolic companion: 13/13 competency checks passed

That last line — symbolic companion: 13/13 competency checks passed — is the volume's real verdict. It means the claims across these twenty-two chapters are not asserted on trust; they are executable, and the day one stops being true, main returns 1 and the build turns red.

Honest advice for building neuro-symbolic systems

If you take one working habit from this volume, take this: model the crisp symbolic version of a task before you reach for a learned one. The reason is practical, not purist. Once you can state what a sound and complete answer is — the exact 8 subsumptions, the two constants alice and bob, the provenance t + r·s — you hold a ground truth to measure a neural approximation against. You can then say precisely what an embedding is supposed to return, see how far it drifts, and tell a lucky guess from a learned truth. Skip that step and a fluent model will hand you confident answers with nothing to check them against. The symbolic model is not the old way that learning replaces; it is the specification the learning is trying to approximate.

The unsolved part

The honest open question is whether the two columns can be merged without a trade. Every partial join the field has tried seems to pay for one property with another: constrain a learner to respect an ontology and you often lose scalability or the smooth gradient that made it trainable; let a reasoner tolerate noise and you often lose the guarantee that made its stamp worth trusting [3]. Volume 2 cannot tell you the trade is unavoidable — and it would be a mistake to declare it so. It establishes only, rigorously and on one shared ontology, that symbolic guarantees are necessary but not sufficient: necessary because a system with no notion of provable, auditable truth cannot be trusted where it matters; insufficient because that same system abstains on missing facts, learns nothing, and cannot always halt. Whether one system can be exact where proof exists, robust where it is not, complete and scalable is genuinely open — the question the remaining volumes exist to attack, not to concede.

Why it matters

The neuro-symbolic bet is that the two columns are complementary rather than competing. This chapter is the honest statement of why the bet is not yet won: you have seen the guarantees earn their green checks on one world, and you have seen the gaps stay open on the same world. Holding that picture clearly — real guarantees on the left, real limits on the right, four tensions that will not vanish — is the most useful thing you can carry forward. 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 genuine neuro-symbolic method must deliver to count as progress: not a higher number on one side, but a system that earns a stamp on both.

Key terms

• The verdict — symbols buy correctness you can trust and explain, on knowledge you must write down and keep consistent; necessary but not sufficient for intelligence.
• Sound and complete classification — the classifier derives all and only the entailed subsumptions, $(A, B) \in \mathrm{cl}(\mathcal{T}) \iff \mathcal{T} \models A \sqsubseteq B$; corroborated here against HermiT.
• PTIME (tractability) — EL classification runs in time polynomial in the ontology size; the academic world saturates in 3 rounds, $(23, 0)$ to $(39, 7)$.
• Certain answers — the tuples true in every model, computed by mapping the query via homomorphism into the universal model built by the chase; only constants qualify (alice, bob).
• Provenance / annotation — metadata riding a derivation: the polynomial t + r·s records why a fact holds; the $[0, 1]$ lattice combines confidence by meet $= \min$, join $= \max$.
• Open-world abstention — a missing fact yields "not entailed," never "false" or "probably" — principled silence, not robustness.
• Undecidable termination — for arbitrary existential rules the chase may run forever and entailment is undecidable; only restricted fragments regain a guarantee.
• The four tensions — expressivity vs tractability, open- vs closed-world, complete vs scalable, exact vs robust: the axes every later method is located on.
• Competency check — one executable assertion over the ontology; the volume's claims equal its tests, and the exit code — 13/13 — is the verdict.

Where this leads

Volume 2 hands you the guarantees, the limits, and one world to weigh them on — and one unanswered question: can exact symbols and robust vectors be made one? The next volume, Volume 3 — Neural Representation, develops the neural pillar: embeddings and the geometric representation of knowledge, where a concept is a region and a relation is a direction, and a query is answered by distance instead of proof. It is the same knowledge base, one knowledge and one question, viewed through the opposite lens — the pillar whose robustness this volume's guarantees need, and whose lack of guarantees this volume's stamp is built to supply.