Propositional Logic: True, False, and What Follows

📍 Where we are: Part I · Logic from Scratch — Chapter 3. Order and Lattices gave us rank, monotone maps, and the least upper bound of a growing set; here we spend that machinery on the smallest logic there is — the first place where "follows from" has an exact meaning — and watch the least fixpoint return as the way a machine actually reasons.

Every argument you trust rests on a claim that some conclusion follows from some premises. Logic's founding move is to make that word precise: to replace "sounds right" with a test a machine can run. The smallest system where the test is fully mechanical is propositional logic, a world of claims that are simply true or false, glued together with a handful of connectives. It is small enough to decide by brute force, and that brute-force procedure (enumerate every possibility and check) is the exact task the last volume of this series learns to approximate.

This chapter builds that system with no gaps. We will define a formula precisely, define its meaning as a computation over a tree, derive the truth table of every connective from the companion code, prove the identity that turns "follows from" into a search for a counterexample, and then run a real reasoner on the running academic world and watch its facts grow in waves to a fixpoint. By the end you will be able to read a small logical engine and see exactly why each number it prints is the number it must print.

The simple version

Imagine a journal's accept/reject stamp, and one house rule everyone agrees on: a paper is accepted exactly when it is both novel and correct. Give each of those three claims a light switch — on or off — and the rule becomes a machine you can check by hand. Flip every combination of switches, and for each pattern ask "does the rule hold?" The full list of patterns where it holds is everything the rule means. Propositional logic is nothing more than that: claims that are true or false, joined by "and", "or", "not", "implies", and "exactly when", and the surprising payoff is that "this follows from that" can be settled by flipping switches until you are certain. Machines reason at scale by flipping switches faster, and by taking shortcuts when the rules have a friendly shape.

What this chapter covers

• Atoms and connectives: the true/false building blocks and the five operators ¬, ∧, ∨, →, ↔, each introduced in plain words, then pinned to its exact truth table as computed by propositional.py.
• Formulas as trees: the inductive definition of a well-formed formula, and how the companion file stores one as an abstract syntax tree of tuples.
• Semantics by structural recursion: a truth assignment as a function, the evaluate walk that reads a formula bottom-up, a derivation of why there are exactly $2^n$ assignments, and the full truth table of "accepted ↔ (novel ∧ correct)" quoted from real output with two rows worked by hand.
• The three questions and one identity: satisfiability, validity, and entailment, the validity/unsatisfiability duality, and a line-by-line proof that premises entail a conclusion exactly when the premises together with the negated conclusion are unsatisfiable, verified against a live enumeration.
• Horn clauses and forward chaining: the restricted clause shape that makes inference branch-free, the immediate-consequence operator $T_P$, a proof that it is monotone and must reach a least fixpoint, and the derivation waves [23, 41, 47, 47] traced atom by atom from forward_chain.py.
• Why neuro-symbolic AI cares: satisfiability and model counting over these formulas are the crisp ground truth Volume 4 makes differentiable.

Atoms, connectives, and formulas as trees

An atomic proposition, or atom, is a claim that can only be true or false, with no internal parts we look inside: this paper is novel, this paper is correct, this paper is accepted. We name them with short variables like novel, correct, accepted. The set of the two truth values we will write $\{\text{T}, \text{F}\}$ (true and false); the curly braces $\{\ \}$ just enclose the members of a set, and later the symbol $\in$ will mean "is an element of", so "$v \in \{\text{T},\text{F}\}$" reads "$v$ is one of true or false".

A connective is an operator that takes one or two truth values and returns a truth value [1]. There are five. Each has a one-line meaning in words before it has a symbol, and each is a small function on $\{\text{T},\text{F}\}$ that the code computes explicitly:

• not (¬): flips true to false and false to true. ¬novel means "not novel". This is the one unary connective (it takes a single argument).
• and (∧): true only when both parts are true. novel ∧ correct.
• or (∨): true when at least one part is true. This is the inclusive or, true also when both parts hold.
• implies (→): writing A and B for any two formulas, A → B is false in exactly one case, when A is true and B is false; think "if A, then B".
• if and only if (↔): A ↔ B is true when both sides have the same truth value; the biconditional, "exactly when".

Because each connective is a finite function, its entire behavior fits in a table. Negation has two input rows; the four binary connectives share the same four input rows $(A,B)$. These tables are not stipulated by decree, they are what the evaluate function in propositional.py returns, and we quote the deciding line of code beside each column:

$A$	$B$	$\neg A$	$A \wedge B$	$A \vee B$	$A \to B$	$A \leftrightarrow B$
F	F	T	F	F	T	T
F	T	T	F	T	T	F
T	F	F	F	T	F	F
T	T	F	T	T	T	T

The ¬A column depends only on $A$ (it repeats down each pair of rows) and comes from return not evaluate(f[1], assignment) at propositional.py:44. The ∧ column is return a and b (line 48), true only in the last row. The ∨ column is return a or b (line 50), false only in the first. The → column is the subtle one: the code computes it as return (not a) or b (line 52), which is false precisely when a is true and b is false, matching the third row and no other. The ↔ column is return a == b (line 54), true on the two rows where $A$ and $B$ agree. We will lean on the fact that → is literally coded as (not a) or b when we reach Horn clauses; hold onto it.

A formula is not a flat string of symbols; it is a tree, and it is defined inductively, which means we say what the simplest formulas are and then how to build bigger ones from smaller ones:

• Base case. Every atom is a formula.
• Inductive step. If $f$ is a formula, then $\neg f$ is a formula. If $f$ and $g$ are formulas, then $f \wedge g$, $f \vee g$, $f \to g$, and $f \leftrightarrow g$ are formulas.
• Nothing else is a formula.

This is a recursive shape: a formula is built from strictly smaller formulas, down to atoms at the leaves. "A paper is accepted exactly when it is novel and correct" has a top connective ↔ whose left branch is the bare atom accepted and whose right branch is itself a smaller formula, novel ∧ correct, whose branches are two more atoms. The companion file makes that tree literal: it stores a formula as a nested tuple whose first slot names the connective and whose remaining slots are its parts, the abstract syntax tree (AST), the parsed skeleton of the sentence. Convenience constructors keep it readable (propositional.py:20):

def V(name):        return ("var", name)
def Not(f):         return ("not", f)
def And(f, g):      return ("and", f, g)
def Or(f, g):       return ("or", f, g)
def Imp(f, g):      return ("imp", f, g)
def Iff(f, g):      return ("iff", f, g)

So our house rule about acceptance is built, and stored, as one tree:

accepted = Iff(V("accepted"), And(V("novel"), V("correct")))
# the same thing as its raw tree:
# ("iff", ("var", "accepted"), ("and", ("var", "novel"), ("var", "correct")))

The outermost tuple is the whole sentence; inside it is the ∧-subtree; inside that, the leaves. The inductive definition above is exactly why every operation in this chapter can be a walk over that tree: each function inspects the head tag, recurses on the child slots, and bottoms out at the "var" leaves.

Semantics: an assignment, and evaluate

Syntax is just shape. Semantics is meaning, and in propositional logic meaning is concrete [2]. A truth assignment is a function $v$ that maps every atom to a truth value, $v : \text{Atoms} \to \{\text{T}, \text{F}\}$; the arrow here just names a rule that takes each atom to one value. It is one setting of all the light switches. In the code an assignment is a Python dict from variable name to True/False, and looking an atom up in it is the base case of evaluation.

Given an assignment, a formula has a single, computable truth value, found by walking the tree from the leaves up: look each atom up in the assignment, then apply each connective's table to the values its children returned. This is structural recursion, recursion that follows the inductive definition of the formula exactly, and it is the evaluate function verbatim (propositional.py:38):

def evaluate(f, assignment: dict) -> bool:
    """Truth value of ``f`` under an assignment of variables to True/False."""
    op = f[0]
    if op == "var":
        return assignment[f[1]]
    if op == "not":
        return not evaluate(f[1], assignment)
    a = evaluate(f[1], assignment)
    b = evaluate(f[2], assignment)
    if op == "and":
        return a and b
    if op == "or":
        return a or b
    if op == "imp":
        return (not a) or b
    if op == "iff":
        return a == b
    raise ValueError(f"unknown connective: {op}")

The "var" branch is the base case (read the switch); each other branch is one line of the inductive step (apply one connective to the already-computed values of its children). Because the recursion always descends to strictly smaller subformulas, it terminates, and it returns exactly the truth value the connective tables above prescribe.

Working the recursion by hand. Take the assignment $v_4$ with accepted false, correct true, novel true, and run evaluate on the acceptance tree bottom-up:

1. Innermost, evaluate(("and", novel, correct), v_4): it sets a = evaluate(novel) = T and b = evaluate(correct) = T, then returns T and T = T.
2. Outer, evaluate(("iff", accepted, ...), v_4): it sets a = evaluate(accepted) = F and b = T (the value just computed), then returns a == b, that is F == T, which is F.

So under $v_4$ the whole rule is false: the paper is novel and correct yet not stamped accepted, a genuine violation of the house rule. Contrast the all-true assignment $v_8$: the ∧-node returns T and T = T, and the ↔-node returns T == T = T, so the rule holds. These two traces are two rows of the table we are about to enumerate.

How many rows? A formula mentions finitely many atoms; call that count $n = |\text{vars}(f)|$, where the bars $|\cdot|$ denote the size of a set. Each atom is independently either true or false, giving two choices, and the choices for distinct atoms are made independently, so the total number of assignments is the product

$$\underbrace{2 \times 2 \times \cdots \times 2}_{n \text{ factors}} \;=\; 2^{n}.$$

The assignments generator produces exactly these, one per tuple from the standard library's itertools.product, imported as the bare name product (line 17) and called as product([False, True], repeat=len(vs)) at propositional.py:61, which is by definition the $2^n$-element set of all length-$n$ true/false tuples. Evaluate the formula on every one of them and you have written out the sentence's entire meaning. That table is the truth table. Our acceptance rule has $n = 3$ atoms, so $2^3 = 8$ rows. Running propositional.py (its atoms sorted alphabetically as accepted, correct, novel) prints:

accepted | correct | novel || f
-------------------------------
F | F | F || T
F | F | T || T
F | T | F || T
F | T | T || F
T | F | F || F
T | F | T || F
T | T | F || F
T | T | T || T
entails accepted -> novel: True

Read the rows against the rule. The last row, accepted, correct, novel all true, makes the two sides agree, so f is T; so does the first row, where nothing is true (both sides false, and false ↔ false is T). The rule breaks in four rows: F | T | T is the $v_4$ we traced (novel and correct yet not accepted); T | F | F is stamped accepted while being neither; and T | F | T and T | T | F are both stamped accepted while the paper is not both novel and correct, the first missing correctness, the second missing novelty. An assignment that makes a formula true is called a model of it, so this table says the rule has four models and four counterexamples.

Meaning made concrete: a formula is a tree whose leaves are true-or-false atoms, its truth table is the enumeration of every switch setting, and forward chaining grows the academic world's facts outward in waves until nothing new appears. Original diagram by the authors, created with AI assistance.

The three questions, and one identity that unites them

Once every formula's meaning is a finite table, three classic questions become mechanical checks over it [3]. A formula is satisfiable if at least one assignment makes it true, that is, it has a model. It is valid, a tautology, if every assignment makes it true, so it can never fail. Each is a one-line loop over the assignments (propositional.py:70 and :74):

def is_satisfiable(f) -> bool:
    return any(evaluate(f, a) for a in assignments(variables(f)))

def is_valid(f) -> bool:
    """Valid = true under *every* assignment (a tautology)."""
    return all(evaluate(f, a) for a in assignments(variables(f)))

Python's any returns true as soon as one assignment satisfies $f$; all returns true only if none fails. Satisfiability and validity are two ends of the same enumeration, and they are joined by a small duality we can prove in one line. A formula $f$ is valid exactly when no assignment makes it false; an assignment makes $f$ false exactly when it makes $\neg f$ true; so "$f$ is valid" is the same statement as "$\neg f$ has no model", that is, "$\neg f$ is unsatisfiable". Reading the chain of equivalences:

$$f \text{ valid} \iff \text{no } v \text{ has } v(f)=\text{F} \iff \text{no } v \text{ has } v(\neg f)=\text{T} \iff \neg f \text{ unsatisfiable}.$$

The symbol $\iff$ here means "is logically the same statement as", each side true in exactly the cases the other is. This duality lets one procedure answer both questions: build a satisfiability checker and you can test validity by negating and checking for no model.

The third question formalizes "follows from". A set of premises entails a conclusion when every model of the premises is also a model of the conclusion: whenever the premises all hold, the conclusion cannot fail. We write this with the double turnstile, $\{\phi_1, \ldots, \phi_k\} \models C$, read "the premises entail $C$". (The double bar $\models$ is semantic entailment, about truth in all models; it is deliberately distinct from the single turnstile $\vdash$, syntactic derivability by proof rules, which the later chapter Inference and Proof develops. That the two coincide for this logic is a theorem, not a definition.)

To check entailment, we hunt for a single counterexample: an assignment that makes every premise true and the conclusion false. If none exists, entailment holds. This is the same as saying the premises together with the negated conclusion have no model at all, that they are unsatisfiable. That equivalence is the load-bearing identity of the whole field, and it deserves a real proof. Let $P$ abbreviate the conjunction of all premises. Then:

$$\begin{aligned} P \models C &\iff \text{every } v \text{ with } v(P)=\text{T} \text{ has } v(C)=\text{T} \\ &\iff \text{no } v \text{ has } v(P)=\text{T} \text{ and } v(C)=\text{F} \\ &\iff \text{no } v \text{ has } v(P)=\text{T} \text{ and } v(\neg C)=\text{T} \\ &\iff \text{no } v \text{ has } v(P \wedge \neg C)=\text{T} \\ &\iff (P \wedge \neg C) \text{ is unsatisfiable}. \end{aligned}$$

Line one is the definition. Line two rewrites "all cases satisfy" as "no case violates" (a universal statement is the denial of an existence). Line three uses $v(C)=\text{F} \iff v(\neg C)=\text{T}$ from the negation table. Line four uses the ∧ table: a conjunction is true exactly when both conjuncts are, so "$v(P)=\text{T}$ and $v(\neg C)=\text{T}$" is precisely "$v(P \wedge \neg C)=\text{T}$". Line five is the definition of unsatisfiability. So: premises entail $C$ if and only if (premises ∧ ¬C) is unsatisfiable. The entails function is exactly that counterexample hunt (propositional.py:79):

def entails(premises: list, conclusion) -> bool:
    """Do the premises logically entail the conclusion? True iff every model of
    all premises is also a model of the conclusion — checked as the
    unsatisfiability of (premises ∧ ¬conclusion)."""
    vs = set(variables(conclusion))
    for p in premises:
        vs |= variables(p)
    for a in assignments(vs):
        if all(evaluate(p, a) for p in premises) and not evaluate(conclusion, a):
            return False
    return True

The function first collects every atom occurring in the conclusion or in any premise into the set vs, folding each premise's atoms in with the augmented assignment vs |= variables(p), which is an in-place set union (it adds those atoms to vs). It then enumerates every assignment over vs. The condition on line 87, all(...premises...) and not evaluate(conclusion, a), is the counterexample test read straight off line two of the proof: premises all true and conclusion false. The first such assignment returns False; if the loop finishes having found none, it returns True.

Working the hunt on the running example. The last line of the run above put it to work: entails accepted -> novel: True. In words: given the acceptance rule $P_1 = (\text{accepted} \leftrightarrow (\text{novel} \wedge \text{correct}))$ and the separate fact $P_2 = \text{accepted}$, does it follow that the paper is novel? The premise set is $\{P_1, P_2\}$ and the conclusion is novel. All three atoms appear, so we enumerate the same eight assignments and check the counterexample condition on each:

#	accepted	correct	novel	$P_1$	$P_2$	both premises?	conclusion novel	counterexample?
1	F	F	F	T	F	no	F	no
2	F	F	T	T	F	no	T	no
3	F	T	F	T	F	no	F	no
4	F	T	T	F	F	no	T	no
5	T	F	F	F	T	no	F	no
6	T	F	T	F	T	no	T	no
7	T	T	F	F	T	no	F	no
8	T	T	T	T	T	yes	T	no

A counterexample would need "both premises = yes" and "conclusion = F" in the same row. Scanning the two columns, the premises hold together in exactly one row, row 8, and there the conclusion novel is true, so it is not a counterexample. No row satisfies both premises while leaving novel false, so the loop finds nothing and entails returns True. The identity checks out too: the only model of the premises (row 8) has novel true, so $\neg\text{novel}$ is false there, so $P_1 \wedge P_2 \wedge \neg\text{novel}$ is false on every row, exactly the unsatisfiability the identity predicts. We have turned a question about valid reasoning into a question about the emptiness of a search, and that reduction, reasoning as (un)satisfiability, is what lets a machine reason without understanding a word of what the atoms mean.

Horn clauses: the shape that makes inference cheap

Enumerating all $2^n$ assignments is correct but hopeless for large formulas. The escape is to restrict the shape of the formulas. A literal is an atom or its negation (for example novel or ¬novel). A clause is an "or" of literals. A Horn clause is a clause with at most one positive literal, at most one un-negated atom, the rest negated.

That definition sounds arcane until we rewrite it, and the rewrite is a derivation we can do with the connective tables already in hand. Take the rule "if professor(x) then researcher(x)", read professor(x) as "x is a professor" with x a placeholder for any individual (first-order notation we unpack next chapter; for now read a filled-in professor(alice) as an ordinary atom). Its natural implication form is $(\text{professor} \to \text{researcher})$. Now unfold it into a clause. Recall the code computes → as (not a) or b, that is, material implication:

$$A \to B \;\equiv\; \neg A \vee B.$$

For a rule with several conditions, say $(b_1 \wedge b_2) \to h$, apply the same equivalence and then De Morgan's law, the identity $\neg(P \wedge Q) \equiv \neg P \vee \neg Q$ ("not both" equals "at least one not"), which itself is just two columns of a truth table agreeing:

$$(b_1 \wedge b_2) \to h \;\equiv\; \neg(b_1 \wedge b_2) \vee h \;\equiv\; (\neg b_1 \vee \neg b_2) \vee h \;\equiv\; \neg b_1 \vee \neg b_2 \vee h.$$

The result is a single clause with exactly one positive literal, the head $h$, and the body conditions appearing negated. That is a Horn clause, and reading it backward, every Horn clause with one positive literal is an implication "conjunction of positive conditions implies one positive head". A plain fact is the special case with an empty body (one positive literal, no negatives). The academic world in kb.py is built entirely from this shape (kb.py:73):

RULES: list[tuple] = [
    # A professor or a student is a researcher; a researcher is a person.
    (("researcher", "X"), [("professor", "X")]),
    (("researcher", "X"), [("student", "X")]),
    (("person", "X"), [("researcher", "X")]),
    # Grand-advising = advising composed with advising (a role chain).
    (("grandAdvisor", "X", "Z"), [("advises", "X", "Y"), ("advises", "Y", "Z")]),
    # ...
    # Transitive closure of citation — the rule that *needs* a fixpoint, because
    # its own head feeds its own body.
    (("citesTransitively", "A", "B"), [("cites", "A", "B")]),
    (("citesTransitively", "A", "C"),
     [("cites", "A", "B"), ("citesTransitively", "B", "C")]),
]

Each pair is (head, body): derive the head whenever every atom in the body already holds. Now the payoff of the restriction. For a general formula, deciding satisfiability may force you to branch, to guess an atom true, explore, backtrack, and guess it false, and that branching is the source of the exponential blow-up. A Horn rule never forces such a guess, though the reason is subtler than "adding facts can never hurt". A set of definite Horn clauses always has a unique least model, and forward chaining reaches a satisfying assignment by only ever adding a forced head $h$ once its body atoms $b_1, b_2$ are all present: it never guesses an atom true or false, and never retracts one. It is not true that any isolated positive addition preserves every clause on its own. The lone rule $\text{rain} \to \text{wet}$, that is the clause $\neg\text{rain} \vee \text{wet}$, is satisfied while both atoms are false (the $\neg\text{rain}$ literal carries it), yet asserting rain by itself flips it to $\neg\text{T} \vee \text{F} = \text{F}$ and breaks it, until wet is added as well. What actually holds is the fixpoint invariant: the least fixpoint, the set forward chaining converges to, satisfies every clause at once. So there is only ever one thing to do, add forced consequences, with no case split anywhere. (These rules carry variables like X, so they are strictly first-order rules, the next chapter's subject, but each ground instance, the rule with every variable replaced by a specific individual so no variables remain, is a propositional Horn clause, and the reasoning principle is identical.)

Forward chaining: reasoning as a least fixpoint

Here the lattice machinery from the previous chapter pays off. Forward chaining computes everything the rules can derive by repeatedly applying the immediate-consequence operator, written $T_P$ (the subscript $P$ names the program, the fixed rule set the operator fires over). In set-builder notation, on a current fact set $I$,

$$T_P(I) \;=\; I \,\cup\, \bigl\{\, \text{head}\cdot\sigma \;:\; (\text{head}, \text{body}) \in P \text{ and every atom of } \text{body}\cdot\sigma \in I \,\bigr\},$$

where $\cup$ is set union (everything in either set), $\sigma$ (sigma) is a substitution that replaces a rule's variables by individuals, and $\text{body}\cdot\sigma$ means the body with that replacement applied. In words: keep everything you already have, and add the head of every rule whose body, under some binding of its variables, is already present. One pass is a few lines (forward_chain.py:42):

def t_p(facts: set, rules: list) -> set:
    """One application of the immediate-consequence operator: the input facts
    plus every head derivable in a single step."""
    out = set(facts)
    for head, body in rules:
        for sub in _match_body(body, facts, {}):
            out.add(apply_sub(head, sub))
    return out

out = set(facts) is the $I$ we keep (the $\cup\, I$); _match_body finds every way the body's atoms line up with the current facts, each returning a substitution sub (the $\sigma$); and apply_sub(head, sub) fills those bindings into the head to produce the derived ground atom, the set-builder's $\text{head}\cdot\sigma$.

Why iterating $T_P$ must halt at a least fixpoint. Two properties do all the work, and both connect straight back to Order and Lattices, where the objects are sets of facts ordered by the subset relation $\subseteq$ ("$I \subseteq J$" means every fact of $I$ is also in $J$).

First, $T_P$ is inflationary: $I \subseteq T_P(I)$, because the operator starts from set(facts) and only ever calls out.add(...), never removes. It can grow the fact set but never shrink it.

Second, $T_P$ is monotone: if $I \subseteq J$ then $T_P(I) \subseteq T_P(J)$. Proof: take any atom $a \in T_P(I)$. Either $a \in I$, and then $a \in J \subseteq T_P(J)$; or $a = \text{head}\cdot\sigma$ for some rule whose body under $\sigma$ lies in $I$, and since $I \subseteq J$ that same body lies in $J$, so the rule fires on $J$ too and $a \in T_P(J)$. Either way $a \in T_P(J)$, which is what $\subseteq$ requires.

Now start from the base facts $I_0$ and iterate, writing $I_{k+1} = T_P(I_k)$. Inflationarity makes the results an increasing chain,

$$I_0 \;\subseteq\; I_1 \;\subseteq\; I_2 \;\subseteq\; \cdots$$

Every $I_k$ is a subset of the finite set of all ground atoms you can form from the finitely many predicates and individuals (the Herbrand base). An increasing chain of subsets of a finite set cannot grow forever; at some step $k$ it must stop adding, giving $I_{k+1} = I_k$. At that point $I_k$ satisfies $T_P(I_k) = I_k$, a set the operator maps to itself: a fixpoint. Because $T_P$ is monotone and we started from the smallest possible set (the given facts) and only added forced consequences, this is the least fixpoint, $\mathrm{lfp}(T_P)$, the least upper bound of the growing chain, exactly the construction the previous chapter set up. Reaching it is a plain loop (forward_chain.py:52):

def least_fixpoint(facts, rules, trace: bool = False):
    """Iterate T_P from ``facts`` until it stops growing. Returns the least
    fixpoint (a ``set`` of ground atoms). With ``trace=True`` also returns the
    per-round size, which shows the derivation "waves" of the chase."""
    current = set(facts)
    sizes = [len(current)]
    while True:
        nxt = t_p(current, rules)
        sizes.append(len(nxt))
        if nxt == current:
            return (current, sizes) if trace else current
        current = nxt

The test nxt == current on line 61 is the fixpoint condition $T_P(I_k) = I_k$ made executable: the moment a pass adds nothing, the loop returns, because by the argument above nothing further can ever be added.

The worked trace, atom by atom. Run forward_chain.py on the academic world and the fixpoint is reached in three rounds:

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.
   ('citesTransitively', 'p2', 'p1')
   ('citesTransitively', 'p3', 'p1')
   ('citesTransitively', 'p3', 'p2')

The size sequence $[23, 41, 47, 47]$ is the chain $|I_0|, |I_1|, |I_2|, |I_3|$ made numeric. We can open up each wave and name every atom it adds, because the run is fully reproducible:

Wave 1 (23 → 41, adds 18 atoms). Every rule whose body is satisfied by the base facts alone fires:

• 5 researcher atoms, from researcher(X) :- professor(X) and researcher(X) :- student(X) (kb.py:75): the two professors alice, bob and the three students carol, dave, erin.
• 3 grandAdvisor atoms, from grandAdvisor(X,Z) :- advises(X,Y), advises(Y,Z) (kb.py:79), one per two-step advising chain: alice→carol (via bob), alice→dave (via bob), bob→erin (via carol).
• 8 colleague atoms, from the shared-institution rule with its X != Y guard (kb.py:82): the mit pair (alice, bob) in both orders is 2, and the three cmu people carol, dave, erin give all 6 ordered distinct pairs, totalling 8.
• 2 citesTransitively atoms, from the base rule citesTransitively(A,B) :- cites(A,B) (kb.py:86): the two direct citations p2→p1 and p3→p2 lifted into the transitive relation.

That is $5 + 3 + 8 + 2 = 18$ new atoms, reaching $23 + 18 = 41$.

Wave 2 (41 → 47, adds 6 atoms). Now the rules whose bodies needed wave-1 output can finally fire:

• 5 person atoms, from person(X) :- researcher(X) (kb.py:77), one per person. These could not appear in wave 1 because researcher did not exist yet; they wait exactly one round for their premise to be derived.
• 1 citesTransitively atom, p3→p1, from the recursive rule citesTransitively(A,C) :- cites(A,B), citesTransitively(B,C) (kb.py:87). It needs citesTransitively(p2,p1), which itself was only derived in wave 1, plus the base fact cites(p3,p2).

That is $5 + 1 = 6$ new atoms, reaching $41 + 6 = 47$.

Wave 3 (47 → 47, adds 0). Every rule body is already satisfied by atoms already present, so t_p returns a set equal to its input, nxt == current fires, and the loop stops. In all, 24 atoms were derived from 23 given (the 47 atoms total, 24 derived line).

The citesTransitively atoms show why a fixpoint is genuinely needed rather than one sweep. citesTransitively p3 p1, paper p3 reaching p1 through p2, is only derivable after citesTransitively p2 p1 exists, because the transitivity rule feeds its own head back into its own body: a rule chasing its own tail until it catches it, with the least fixpoint the place it finally does. Notice too that the whole computation stabilizes in one round more than the deepest rule chain, which is why two waves of change ($I_0 \to I_1 \to I_2$) need a third confirming pass ($I_2 \to I_3$) that adds nothing. This same engine is the shape of a Datalog reasoner and, in Volume 2, of the description-logic completion algorithm that computes what an ontology entails.

The unsolved part

Everything above leans on one quietly expensive fact: our decision procedures enumerate. is_valid, is_satisfiable, and entails all loop over every assignment, and for $n$ atoms there are $2^n$ of them. The growth is merciless: at $n = 60$ atoms the count $2^{60} \approx 1.15 \times 10^{18}$ already exceeds the roughly $4.4 \times 10^{17}$ seconds in the entire age of the universe, so a checker doing one assignment per second would not have finished since the Big Bang. The Horn restriction rescues the special case (Horn satisfiability is decidable in near-linear time by exactly the forward chaining we just traced, no branching), but the general Boolean satisfiability problem (SAT) is NP-complete. NP is nondeterministic polynomial time, the class of problems whose candidate answers are easy to check quickly but seemingly hard to find; NP-complete means SAT is among the hardest in that class, so an efficient method for it would solve them all. Worse for what comes next, counting the models rather than finding one, model counting or #SAT, is #P-hard, at least as hard as the hardest problems in the counting class #P, harder still than merely deciding satisfiability. Whether any method fundamentally beats enumeration on the hardest formulas is the P versus NP question (P being deterministic polynomial time, the problems a machine can actually solve quickly, set against NP's merely-checkable ones), the most famous open problem in computer science, and it is genuinely unsolved. So propositional logic hands us a perfectly crisp notion of truth and a brute-force way to decide it, and, in the same breath, a wall that brute force cannot scale.

Why it matters

That wall is exactly where neuro-symbolic AI enters. The tasks this chapter defined, is this formula satisfiable, and how many of its assignments are models, are the precise operations a learning system needs when it wants its predictions to obey rules. Volume 4 takes model counting and makes it differentiable: instead of counting satisfying assignments by enumeration, it computes a smooth, weighted approximation, weighted model counting (WMC), and turns the logical constraint into a semantic loss a neural network can be trained against, nudging the network toward outputs that a symbolic checker would accept. The crisp SAT/counting answer defined here is the ground truth that relaxation targets: you cannot approximate a quantity you have not first pinned down exactly. Propositional logic is where "what follows" stops being an opinion and becomes a number, and that number is what the neural side later learns to feel its way toward.

Key terms

• Atom / atomic proposition: a claim that is simply true or false, with no internal parts we inspect (novel, accepted).
• Connective: an operator on truth values, each a fixed table: not (¬), and (∧), or (∨), implies (→, coded as (not a) or b), if-and-only-if (↔).
• Formula / abstract syntax tree (AST): a sentence defined inductively from atoms and connectives, stored as a nested tuple whose first slot names the connective.
• Truth assignment / model: a function from atoms to true/false; a model is an assignment that makes the formula true. A formula with $n$ atoms has $2^n$ assignments.
• Satisfiable / valid (tautology): has at least one model / is true under every assignment; $f$ is valid exactly when $\neg f$ is unsatisfiable.
• Entailment ($\models$): premises entail $C$ when every model of the premises is a model of $C$; equivalently, when (premises ∧ ¬C) is unsatisfiable.
• Literal / clause / Horn clause: an atom or its negation; an "or" of literals; a clause with at most one positive literal, equivalent to "conjunction of conditions implies one head", which makes inference branch-free.
• Immediate-consequence operator ($T_P$) / least fixpoint: the inflationary, monotone map firing all applicable rules once; iterating it on a finite domain must reach a smallest self-reproducing fact set, the Horn program's meaning, computed by forward chaining.
• SAT / model counting: Boolean satisfiability (NP-complete) and the harder problem of counting models (#P-hard); the crisp ground truth Volume 4 approximates with weighted model counting.

Where this leads

Propositional logic gave us an exact "follows from", but at a cost we felt immediately: it cannot look inside a claim. It can say alice_advises_bob is true, yet it cannot express "every professor who advises a student is a researcher", because it has no notion of objects, relations, or "every". The next chapter, First-Order Logic: Objects, Relations, and Quantifiers, adds exactly that machinery: variables that range over individuals, relations that hold between them, and the quantifiers ∀ ("for all") and ∃ ("there exists"), turning the flat atoms of this chapter into the structured predicates the academic-world rules (the X, Y, Z we kept meeting) were secretly written in all along.

---

Companion code: examples/logic/propositional.py implements the connectives, evaluate, is_satisfiable, is_valid, and entails as pure enumeration; examples/logic/forward_chain.py implements $T_P$ and least_fixpoint over the Horn rules in examples/logic/kb.py. Run python3 examples/logic/propositional.py to reproduce the truth table and the entailment check, and python3 examples/logic/forward_chain.py to reproduce the [23, 41, 47, 47] derivation waves and the three citesTransitively atoms quoted above.