Entailment and Inference

1Entailment: true in every model

A knowledge base entails a query when the query is true in every world where the base holds. Necessity, not likelihood: one consistent counter-world, however contrived, and the entailment claim is dead.

Take the base { if it rained, the ground is wet; it rained }. Any world respecting both claims is a world with wet ground, so wetness is entailed — no surviving world says otherwise.

As a picture, entailment is set containment over worlds: the base's models sit wholly inside the query's models.

And the direction people trip on: a base failing to entail q does not make q false. The base is a partial description of the world, and silence settles nothing.

Figure. Entailment drawn as containment: every world where the knowledge base holds already sits inside the region where q holds. Worlds with q true but the base false are allowed; a KB-world outside the q region is the one thing entailment forbids.

2Model checking by enumeration

The definition of entailment is directly executable for small bases: enumerate every world, discard those where some accepted claim fails, and ask whether the query holds in every survivor. This procedure is sound and complete for propositional logic — it is the semantics, run literally.

Its cost is the 2^n from the previous lesson, which is why it is a definition of correctness first and a practical algorithm second.

The lab below is the procedure in a dozen lines of Python; the heavily-optimised version of the same loop is what an industrial SAT solver is.

Figure. The four worlds from the propositional lesson, filtered by the base: three break an accepted claim and are eliminated. The single survivor has wet true, so wet holds in every world consistent with the base — entailed.

The procedure

1. Enumerate the worldsList every true/false assignment to the atoms — two atoms give four worlds.
2. Keep the KB-worldsDrop any world where some accepted claim comes out false. What survives is every way the world could be, given the base.
3. Check the query in allQuery true in every survivor: entailed. One surviving counter-world: the base does not settle it.

Coding lab. Does the base entail 'wet'? runs in the app, with checks on your output.

3Proofs: reasoning without enumerating

Enumeration checks all worlds; a proof never looks at a world at all. An inference rule is a syntactic pattern — from p and p \to q, conclude q (modus ponens) — and a proof is a chain of rule applications leading from the base to the query.

Syntax standing in for semantics is the trade: each rule application is cheap and local, and a found proof certifies entailment without visiting 2^n worlds. The search for which rules to apply is where the cost went.

A proof also gives you something a green test run does not: a checkable artifact. Every step can be verified independently, which is the property today's formal-verification tools — and proof-checking layers around code generators — are built on.

A three-line proof

1. GivenThe base holds p \to q, q \to r, and p.
2. Modus ponens onceFrom p and p \to q: conclude q.
3. Modus ponens againFrom q and q \to r: conclude r — proved, and not one world inspected.

4Soundness and completeness

Two questions decide whether a proof procedure can be trusted. Soundness: does it prove only entailed sentences? Completeness: does it prove all of them? They fail in opposite directions — an unsound system manufactures falsehoods, an incomplete one leaves true consequences unreachable.

Propositional logic is as good as this ever gets: truth-table checking is sound and complete outright, and resolution is sound and refutation-complete. The price is time, not truth — SAT's exponential worst case again.

The pair is vocabulary you will reuse far from logic. An analyser that flags every real bug but drowns you in false alarms, and one that only speaks when certain but misses cases, are giving up opposite halves of this guarantee — and naming which half was given up is the design decision.

Figure. A sound but incomplete prover: everything provable is entailed — the inner set never escapes the outer — while the ring between them is entailed truths no proof reaches. Soundness forbids the inner set escaping; completeness would shrink the ring to nothing.

5Entailment versus a score

Modern systems make two kinds of claims, and they must not be confused. 'The base entails q' is necessity: true in every KB-world, refuted outright by a single counterexample, never a matter of degree. 'The model outputs 0.99 for q' is plausibility: a degree of belief, calibrated at best, and allowed to be wrong on this very case while remaining a good score.

An LLM's fluent answer is the second kind of claim wearing the grammar of the first. Nothing in the sampling process checks worlds; confidence of tone is not confidence of measure, and neither one is entailment.

Frontier practice buys guarantees where guarantees are cheap: let learned components propose, and route the claims that must hold — schema validity, resource limits, legal constraints — through a checker that deals in necessity. Deciding which layer a claim lives in is a design decision you now have the vocabulary for.

6From brittle truth to degrees of belief

Logic's truth values are all-or-nothing, and noisy evidence fits neither word. A sensor that is right 95% of the time offers a bad bargain: assert its reading as fact and the wrong 5% enter as unqualified truths, poisoning everything later derived from them; refuse to assert and the base learns nothing at all.

Degrees of belief dissolve the dilemma. An agent holding 'wet' at 0.8 can act on it, weigh it against later evidence, and be outvoted without contradiction — which no hard assertion survives.

That is the bridge out of this lesson. The next topic, Bayes, is the arithmetic of exactly those updates — and the base's hard constraints stay on beside it, because probability did not replace logic; it took over the claims logic held badly.

Figure. A sensor right 95% of the time is a bad bargain for all-or-nothing truth. Assert the reading and the wrong 5% poison later inferences; refuse and the base learns nothing. Holding wet at 0.8 is usable now and revisable when the next reading lands.

The bad bargain

1. Assert as factThe 5% wrong readings enter as unqualified truths, and every downstream inference inherits them.
2. Refuse to assertThe base stays consistent and learns nothing; the sensor was bought for nothing.
3. Hold a degree0.8 acts like 0.8 — usable now, revisable the moment the next reading lands.