Soundness and Completeness: Why the Rules Suffice

📍 Where we are: Part III · The EL Completion Algorithm — Chapter 10. Completion Rules handed us the six firing rules — CR1–CR4, the bottom rule CR⊥, and the role-chain rule CRχ — and watched them grow the two tables $S$ and $R$ to a fixpoint on the academic world. Now we ask the question that turns a clever loop into a reasoner: do those rules derive exactly the subsumptions that genuinely follow, no more and no fewer?

The completion algorithm is built, and it runs. But "it runs and the answers look right" is a hope, not a guarantee — a single passing example proves nothing about the next ontology. This chapter replaces the hope with a proof. We name the three properties a rule set must have before anyone may call it a decision procedure, argue that EL completion has all three, and then do the one thing a paper proof cannot do: run the from-scratch reasoner beside a production one and watch them agree, entry for entry.

The simple version

Imagine hiring an inspector to certify a bridge before it opens. You need three separate promises before you trust the final stamp. First, the inspector never condemns a sound cable — no false alarms that shut a good bridge. Second, the inspector never walks past a frayed one — no misses. Third, the inspection actually finishes, by opening day, instead of pacing the deck forever. Only all three at once make the report worth acting on: an inspector who cries wolf, or overlooks a fault, or never comes back down is useless. A reasoner is that inspector, the class hierarchy is its report, and this chapter is the argument that our inspector has all three virtues — plus a second, independent inspector who checks the first.

What this chapter covers

• Three properties, one decision procedure — soundness (no false positives), completeness (no false negatives), and termination (always halts); only together do they license reading entailment off the table.
• Soundness, worked for CR4 — every rule preserves truth in every model, shown as a single display implication over the description-logic semantics.
• Completeness by canonical model — the saturated $S$ and $R$ are a model of the TBox that falsifies every subsumption the rules did not derive, so anything entailed must have been derived.
• Termination and the polynomial bound — $S$ and $R$ only grow, inside a ceiling fixed by the number of names and pairs, so the fixpoint arrives in polynomially many steps.
• The empirical cross-check — reasoners.py pits classify() against HermiT and both land on 8 subsumptions and the same 2 unsatisfiable concepts.
• Why an independent oracle matters — HermiT is a complete OWL 2 DL reasoner over a strict superset of EL, so its agreement is the strongest external check the from-scratch code can get.

Three properties, one decision procedure

Fix the vocabulary first. A TBox $\mathcal{T}$ is the set of schema axioms (our academic world has 14 of them); a subsumption $A \sqsubseteq B$ reads "every $A$ is a $B$." The question a classifier answers is entailment, written $\mathcal{T} \models A \sqsubseteq B$ and read "the TBox entails $A \sqsubseteq B$": it means the subsumption holds in every interpretation that obeys $\mathcal{T}$ — there is no possible world consistent with the axioms in which some $A$ fails to be a $B$. Completion answers this semantic question by a purely syntactic move: it fires rules until the table $S$ stops growing, then reports $A \sqsubseteq B$ precisely when $B \in S(A)$. That read-off is one line — return sup in S.get(sub, set()) (el_completion.py line 324).

For that syntactic test to mean the semantic entailment, three properties must line up. Naming them precisely is the whole discipline:

Property	Plain meaning	What breaks without it	How EL completion secures it
Soundness	derives only entailed subsumptions — no false positives	the reasoner "proves" falsehoods; every answer is suspect	an invariant every rule preserves in every model [1]
Completeness	derives every entailed subsumption — no false negatives	the reasoner misses real consequences; silence stops meaning "does not follow"	a canonical model satisfying $\mathcal{T}$ that falsifies every non-derived subsumption [2]
Termination	the saturation loop always halts	the answer can never be read off $S$, because "done" never arrives	$S$ and $R$ grow monotonically inside a polynomial ceiling

Only all three together earn the phrase decision procedure: an algorithm that, for every input, halts with the correct yes-or-no answer. Soundness and completeness are the correctness half, and they collapse into one clean biconditional,

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

whose left-to-right direction ($\Longrightarrow$, read "implies") is soundness and whose right-to-left direction ($\Longleftarrow$) is completeness. One caveat keeps this honest: read the biconditional over the satisfiable names $A$, those with $\bot \notin S(A)$. When $A$ is unsatisfiable ($\bot \in S(A)$), the right side is vacuously true — $\mathcal{T} \models A \sqsubseteq B$ holds for every $B$ by ex falso, since an empty concept is a subset of anything — yet the algorithm does not flood $S(A)$ with every name; it reports $A$ apart as unsatisfiable, the separate job of the bottom rule. Termination is the third leg: it guarantees the left side is ever actually computed. The reasoner's own docstring states the target outright — "The algorithm is sound and complete for EL++ subsumption, and runs in time polynomial in the size of the TBox" (el_completion.py lines 38–39). Read that "EL++" against the constructors the academic world actually uses — conjunction, existentials, ⊥, and role chains, the tractable core that the six rules here decide; full EL++ additionally admits nominals and concrete domains, whose own completion rules this ontology never exercises. The rest of this chapter is why that sentence is true.

A decision procedure stands on three columns — soundness, completeness, termination — that together license the biconditional at its crown, while the cross-check against HermiT is the handshake beneath that corroborates the whole structure. Original diagram by the authors, created with AI assistance.

Soundness: every rule preserves truth

Soundness says the rules never lie. The argument is one sturdy idea: keep an invariant that ties every syntactic entry to a semantic fact, and check that each rule preserves it.

First the semantics, decoded before any symbols. An interpretation $\mathcal{I}$ is one possible world: it fixes a domain $\Delta^{\mathcal{I}}$ of individuals, reads each concept name $A$ as a set $A^{\mathcal{I}} \subseteq \Delta^{\mathcal{I}}$ (its extension — the things that are $A$'s in that world), and reads each role $r$ as a set of pairs $r^{\mathcal{I}}$. The constructors get their obvious meanings: conjunction is intersection, $(C \sqcap D)^{\mathcal{I}} = C^{\mathcal{I}} \cap D^{\mathcal{I}}$ ("in both"), and the existential is $(\exists r.C)^{\mathcal{I}} = \{\, x : \exists y,\ (x,y) \in r^{\mathcal{I}} \ \wedge\ y \in C^{\mathcal{I}} \,\}$ ("the $x$ that are $r$-related to some $C$"). The world $\mathcal{I}$ is a model of $\mathcal{T}$ when it satisfies every axiom, each axiom $C \sqsubseteq D$ meaning $C^{\mathcal{I}} \subseteq D^{\mathcal{I}}$.

Now the invariant. Across the whole saturation, for every model $\mathcal{I}$ of $\mathcal{T}$, we maintain:

$$B \in S(A) \ \Rightarrow\ A^{\mathcal{I}} \subseteq B^{\mathcal{I}}, \qquad (A,B) \in R(r) \ \Rightarrow\ A^{\mathcal{I}} \subseteq (\exists r.B)^{\mathcal{I}}.$$

In words: every subsumer the algorithm records is a real subsumption in every model, and every role edge it records is a real "$A$ has an $r$-successor in $B$" in every model. If this survives to the moment saturation stops, then $B \in S(A)$ forces $A^{\mathcal{I}} \subseteq B^{\mathcal{I}}$ in all models — which is exactly $\mathcal{T} \models A \sqsubseteq B$. So proving soundness is proving the invariant survives every rule firing.

It holds at the start: $S(A)$ is seeded with just $A$ and $\top$ (el_completion.py line 187, S = {a: {a, TOP} for a in names}), and $A^{\mathcal{I}} \subseteq A^{\mathcal{I}}$ together with $A^{\mathcal{I}} \subseteq \top^{\mathcal{I}} = \Delta^{\mathcal{I}}$ are both trivially true. The inductive step checks each rule. Take CR4, the subtlest one — four lines of code plus its comment (el_completion.py lines 234–238):

# CR4: (A, B) ∈ R(r), B' ∈ S(B), ∃r.B' ⊑ C  ⟹  C ∈ S(A)
for _, r, b_prime, c in nf4:
    for (A, B) in list(R.get(r, ())):
        if b_prime in S[B] and c not in S[A]:
            S[A].add(c); changed = True

CR4 fires when three facts sit in the tables at once — $(A,B) \in R(r)$, $B' \in S(B)$, and the axiom $\exists r.B' \sqsubseteq C$ belongs to $\mathcal{T}$ — and it concludes $C \in S(A)$. Its soundness is the following implication, true in every model $\mathcal{I}$ of $\mathcal{T}$, with each premise labelled by the table entry that guarantees it:

$$\underbrace{A^{\mathcal{I}} \subseteq (\exists r.B)^{\mathcal{I}}}_{(A,B)\,\in\, R(r)} \ \wedge\ \underbrace{B^{\mathcal{I}} \subseteq (B')^{\mathcal{I}}}_{B'\,\in\, S(B)} \ \wedge\ \underbrace{(\exists r.B')^{\mathcal{I}} \subseteq C^{\mathcal{I}}}_{\exists r.B' \,\sqsubseteq\, C \,\in\, \mathcal{T}} \quad\Longrightarrow\quad A^{\mathcal{I}} \subseteq C^{\mathcal{I}}.$$

Read it pointwise, which is how you check it by hand. Take any individual $x \in A^{\mathcal{I}}$. The first premise puts $x \in (\exists r.B)^{\mathcal{I}}$, so there is some $y$ with $(x,y) \in r^{\mathcal{I}}$ and $y \in B^{\mathcal{I}}$. The second premise, $B^{\mathcal{I}} \subseteq (B')^{\mathcal{I}}$, upgrades that witness to $y \in (B')^{\mathcal{I}}$ — so $x$ is $r$-related to a $B'$, i.e. $x \in (\exists r.B')^{\mathcal{I}}$. The third premise, which is just the axiom holding in $\mathcal{I}$, then delivers $x \in C^{\mathcal{I}}$. Since $x$ was arbitrary, $A^{\mathcal{I}} \subseteq C^{\mathcal{I}}$ — exactly the invariant for the newly written $C \in S(A)$. The same one-model, pointwise check goes through for CR1, CR2, CR3, the bottom rule, and the role-chain rule; each simply chains the semantics of the constructor it touches. Because the invariant holds at the seed and is preserved by every firing, it holds at the fixpoint, and soundness follows [1].

Completeness: a model that falsifies everything else

Completeness is the mirror claim and the harder direction: if $\mathcal{T} \models A \sqsubseteq B$ then the rules really did put $B$ into $S(A)$. By contraposition, whenever $B \notin S(A)$ at the fixpoint, the subsumption genuinely does not follow — there must exist a model of $\mathcal{T}$ in which some $A$ is not a $B$. Completeness is proved by building that countermodel, once, out of the saturated tables themselves.

The construction is the canonical model $\mathcal{I}$, read directly off $S$ and $R$ [2]. Take one domain element $d_A$ for each satisfiable concept name (each $A$ with $\bot \notin S(A)$), and define the extensions by the tables:

$$\Delta^{\mathcal{I}} = \{\, d_A : \bot \notin S(A) \,\}, \qquad A^{\mathcal{I}} = \{\, d_B : A \in S(B) \,\}, \qquad r^{\mathcal{I}} = \{\, (d_A, d_B) : (A,B) \in R(r) \,\}.$$

Two facts make this work, and both are consequences of saturation — the state in which no rule can fire any more. First, the tables are read off honestly: by construction $d_A \in B^{\mathcal{I}}$ iff $B \in S(A)$. Second, $\mathcal{I}$ is a genuine model of $\mathcal{T}$. This is where the completion rules earn their keep in reverse: each closure condition a model must satisfy corresponds to a rule that can no longer fire. Suppose $\mathcal{I}$ violated an axiom $\exists r.B' \sqsubseteq C$ — some $d_A$ with an $r$-edge to a $B'$ but $d_A \notin C^{\mathcal{I}}$. Unfolding the definitions, that says $(A,B) \in R(r)$, $B' \in S(B)$, and $C \notin S(A)$ all hold — so CR4's guard c not in S[A] would be true and the rule would still fire, contradicting that we stopped at a fixpoint. Saturation is exactly the statement that the canonical model has no such gaps; every axiom shape is guarded by the rule that would repair its violation.

The payoff is immediate, for any satisfiable name $A$ — one whose $d_A$ actually sits in $\Delta^{\mathcal{I}}$. Since every $S(A)$ is seeded with $A$ itself, $d_A \in A^{\mathcal{I}}$ always. So if $B \notin S(A)$, then $d_A \in A^{\mathcal{I}}$ yet $d_A \notin B^{\mathcal{I}}$: the canonical model is a witnessing world in which an $A$ is not a $B$, hence $\mathcal{T} \not\models A \sqsubseteq B$. This is exactly why the domain excludes $d_A$ for unsatisfiable names: there $\mathcal{T} \models A \sqsubseteq B$ holds vacuously for every $B$ (the ex-falso subsumptions again), so no countermodel exists or is wanted, and the bottom rule reports those names separately. Contrapositive: for every satisfiable $A$, whatever is entailed was derived. One model, assembled from the saturated tables, simultaneously falsifies every non-derived subsumption between satisfiable names — that is the whole of completeness in a single object.

Termination and the polynomial bound

Correctness is worthless if the loop never stops, so termination is the third pillar — and for EL it arrives with a complexity bound as a bonus. The saturation loop is a plain while changed: that flips changed = False at the top of each pass and back to True only when a rule adds something new (el_completion.py lines 210–213):

    rounds = [sizes()]
    changed = True
    while changed:
        changed = False

Every rule adds to $S$ or $R$ and none ever removes — each is guarded by a not in test (c not in S[A], pair not in R[r]) that sets changed = True only on a genuine addition. So the tables grow monotonically, and they grow inside a fixed ceiling. Let $N$ be the set of concept names and $N_R$ the set of roles. Each $S(A)$ is a subset of $N$, and each $R(r)$ a subset of $N \times N$, so the totals are capped:

$$\sum_{A} |S(A)| \ \le\ |N|^2, \qquad \sum_{r} |R(r)| \ \le\ |N_R| \cdot |N|^2.$$

A quantity that only increases and is bounded above must stabilize. Each productive pass adds at least one element to a total capped by those two ceilings, so after $O(|N_R| \cdot |N|^2)$ passes — polynomially many — nothing new appears, changed stays False, and the loop exits at the least fixpoint. Each pass itself does only polynomial work (scanning the axioms against the names), so the whole classification is polynomial in the size of the TBox — the PTIME result that lets OWL 2 EL reasoners scale to SNOMED CT and the Gene Ontology, ontologies with hundreds of thousands of concepts [1]. Our academic world reaches its fixpoint in just three rounds; the standalone run prints the climb, the sizes of $S$ and $R$ freezing the instant a pass changes nothing (python3 el_completion.py):

saturation reached a fixpoint in 3 rounds
  round : |S| |R|  (derived subsumers, derived role pairs)
      0 :  23   0
      1 :  34   7
      2 :  39   7
      3 :  39   7

The final row repeating the one above it — $|S| = 39$ and $|R| = 7$, both unchanged — is termination made visible: round 3 fires every rule, produces nothing new, and the loop halts. That plateau is the executable form of $T(X) = X$: the moment the monotone operator maps the state to itself, the climb is over.

The empirical cross-check: from-scratch against HermiT

A proof is a meta-argument on paper; it says nothing about whether this Python faithfully implements it. A transcription slip, an off-by-one in a guard, a missing rule case — none of those show up in the mathematics. For that we need an independent witness. The companion reasoners.py rebuilds the identical academic-world ontology with owlready2, runs HermiT over it via sync_reasoner (reasoners.py line 99), calls the from-scratch classify() (line 136), and asserts that the two classifications match "entry for entry" (reasoners.py lines 139–152):

    print("Reasoner (HermiT via owlready2) vs. from-scratch EL completion")
    print(f"  from-scratch subsumptions : {len(el_subs)}")
    print(f"  HermiT subsumptions       : {len(r_subs)}")
    print(f"  from-scratch unsatisfiable: {sorted(el_unsat)}")
    print(f"  HermiT unsatisfiable      : {sorted(r_unsat)}")

    subs_agree = r_subs == el_subs
    unsat_agree = r_unsat == el_unsat
    ...
    assert subs_agree, ("subsumption mismatch", r_subs ^ el_subs)
    assert unsat_agree, ("unsat mismatch", r_unsat ^ el_unsat)
    print("\n  AGREEMENT CONFIRMED — the from-scratch reasoner matches HermiT.")

The ^ in the assertion messages is set symmetric difference — the entries on which the two reasoners disagree — so a failure would print exactly what diverged. It never does. The committed output (python3 reasoners.py) is a clean agreement:

Reasoner (HermiT via owlready2) vs. from-scratch EL completion
  from-scratch subsumptions : 8
  HermiT subsumptions       : 8
  from-scratch unsatisfiable: ['TenuredStudent', 'TenuredStudentAdvisor']
  HermiT unsatisfiable      : ['TenuredStudent', 'TenuredStudentAdvisor']

  subsumptions agree : True
  unsatisfiable agree: True

  AGREEMENT CONFIRMED — the from-scratch reasoner matches HermiT.

Both reasoners find the same 8 subsumptions — Dean ⊑ Person, Professor, Researcher; Professor ⊑ Person, Researcher; Researcher ⊑ Person; Student ⊑ Person, Researcher — and both flag the same 2 unsatisfiable concepts, TenuredStudent and TenuredStudentAdvisor, the deliberately over-constrained classes that make the bottom rule earn its keep. Two independent code paths — one written straight from the textbook completion rules, one a decade-hardened engine — arrive at an identical hierarchy.

Why an independent oracle is the strongest check

Agreement is only as convincing as the witness, and HermiT is the best available. It is a complete OWL 2 DL reasoner [3] — its decision procedure (a hypertableau calculus) is engineered for the full SROIQ description logic behind OWL 2 DL, which is a strict superset of the tiny EL fragment our completion algorithm handles. So HermiT is not a second copy of the same idea that might share the same blind spot; it decides subsumption by a completely different method over a far larger logic, and still lands on the same eight-and-two answer (reasoners.py docstring, lines 12–16: "a strict superset of EL, so agreement here is the strongest possible check"). The owlready2 distribution does not ship the EL-specialised ELK reasoner; driving the heavier, more general HermiT is deliberate, because a superset oracle agreeing is stronger evidence than a same-fragment tool agreeing — the same fragment could hide the same mistake. When a from-scratch implementation and an independent, more powerful reasoner concur on every entry, the residual chance that both are wrong in the same way is about as small as external validation gets. The proof tells us the rules are right; the oracle tells us the code is a faithful copy of the rules.

The unsolved part

Here is the honest boundary. The three-part correctness — soundness, completeness, termination — is a meta-theorem about the algorithm, not a fact the algorithm checks about itself. The reasoner classifies the ontology; it does not, and cannot from the inside, prove that its own rule set is complete for the EL fragment (with ⊥ and role chains) it implements. That proof lives in the mathematics and in our confidence in the code, and the HermiT cross-check corroborates the implementation, not the theorem: agreement on one ontology cannot certify agreement on all of them, and a bug that happens to be shared, or an ontology that quietly slips outside EL, could still fool both. The gap between "the rules are provably right" and "the machine has verified they are right on this input" is exactly the seam a proof-producing or certifying reasoner tries to close, by emitting a checkable justification alongside each answer.

And there is a broader story hiding in plain sight. Look back at how these rules work: our whole method was to derive consequences directly — start from the asserted axioms, fire truth-preserving rules, and saturate — rather than to assume the negation and hunt for a contradiction the way a tableau reasoner does. That forward, contradiction-free style has a name, consequence-based reasoning, and it is precisely what buys EL its polynomial-time guarantee. It is the last stop of this part.

Why it matters

Soundness and completeness are the entire reason the symbolic half of neuro-symbolic AI is worth its brittleness. A learned model answers every query but can be confidently wrong; a sound-and-complete reasoner answers a narrower question, but its "yes" is a guarantee and its "no" means "does not follow," full stop. That certainty is exactly what a neural approximation must be measured against: when a later differentiable or embedding-based reasoner ranks subsumptions by plausibility, the 8 exact subsumptions and 2 exact unsatisfiabilities certified here are the ground truth that says whether the soft model drifted — and the long-range unsatisfiability of TenuredStudentAdvisor, contradiction propagated backward through a role, is precisely the kind of inference soft models tend to miss. A decision procedure is the specification the learning half is trying to approximate, and you cannot tell an approximation is good without an exact answer to hold it to. Knowing the rules suffice, and knowing why, is what makes the completion algorithm usable as that yardstick rather than merely one more heuristic that happened to look right.

Key terms

• Decision procedure — an algorithm that halts on every input with the correct yes-or-no answer; for subsumption it demands soundness, completeness, and termination together.
• Soundness — derives only entailed subsumptions ($B \in S(A) \Rightarrow \mathcal{T} \models A \sqsubseteq B$); proved by an invariant every rule preserves in every model.
• Completeness — derives every entailed subsumption ($\mathcal{T} \models A \sqsubseteq B \Rightarrow B \in S(A)$, for satisfiable $A$); proved by a canonical model that falsifies every non-derived subsumption.
• Termination — the saturation loop always halts, because $S$ and $R$ grow monotonically inside a polynomial ceiling $\le |N_R| \cdot |N|^2$.
• Entailment $\mathcal{T} \models A \sqsubseteq B$ — the subsumption holds in every model of the TBox; the semantic target the syntactic test $B \in S(A)$ must match.
• Canonical model — an interpretation built directly from the saturated $S$ and $R$; it satisfies $\mathcal{T}$ yet witnesses the failure of everything the rules did not derive.
• Oracle (HermiT) — a complete OWL 2 DL reasoner over a strict superset of EL, used as an independent witness that the from-scratch classification is correct.
• Symmetric difference (the Python ^ operator) — the set of entries on which two classifications disagree; empty here, which is why agreement is confirmed.

Where this leads

We have closed the loop on the completion algorithm: rules that are provably sound, complete, and terminating, corroborated by a production reasoner that matches them on every entry. But notice again how they work — they never guess, never assume a negation, never build a tableau and backtrack. They start from what is asserted and grind out consequences until nothing new appears, a monotone fixpoint climb. The next chapter, Consequence-Based Reasoning, gives that style its proper name and shows why deriving consequences directly, rather than searching for contradictions, is exactly what buys EL its polynomial-time classification — the same saturation trace we have been reading, seen now as one instance of a general and powerful reasoning paradigm.