Stanford CS221 ｜ Autumn 2025 ｜ Lecture 16： Logic II.en_Transcript — Annotated Lecture Notes & Key Takeaways

Course Information

Institution: Stanford

Original Course: Stanford CS221 | Autumn 2025 | Lecture 16: Logic II

Instructor Bio: This lecture is delivered by Percy Liang, Associate Professor of Computer Science at Stanford University and core faculty of the Stanford Institute for Human-Centered Artificial Intelligence (HAI). Percy Liang leads the Stanford Natural Language Processing Group and the Center for Research on Foundation Models (CRFM). His research spans the theoretical foundations and practical systems of artificial intelligence, including machine learning, natural language processing, AI alignment, and rigorous model evaluation. He received his PhD in Computer Science from the University of California, Berkeley and his BA in Mathematics from Harvard University. His work has been recognized with the NSF CAREER Award, Google Faculty Research Award, and multiple best paper awards at top-tier AI conferences. He has taught CS 221 at Stanford for over a decade, shaping foundational AI education for thousands of students.

Course Description: This second logic lecture extends to first-order predicate logic, which enables representation of complex relational knowledge and quantified statements. It covers first-order logic syntax, semantics, and universal/existential quantifiers, then introduces unification and resolution for first-order theorem proving. The lecture also discusses knowledge representation challenges, description logics, and the fundamental tradeoff between expressive power and computational complexity in logical reasoning systems.

This is the second of the two logic lectures in Stanford's CS221 (Autumn 2025), and the topic is first-order logic. I sat with the transcript the way you'd sit with a recording you missed, and what follows is my reconstruction of what the lecturer actually built, in the order he built it, with the spots where I got lost or wanted more. One housekeeping note before anything else: the auto-captioning on this recording is rough. "Knows" repeatedly comes out as "nose," "arity" as "error," and Goldbach's conjecture as "code box conjecture." If a sentence below looks oddly spelled, that's the transcript, not the lecturer.
 

The Snowing-in-Phoenix Puzzle and the Propositional Recap

 

A knowledge base that refuses to answer

 

He opens by refusing to define anything (0:45). Instead he writes a knowledge base on the board one line at a time, each line paired with its formal counterpart, and asks the room to do the reasoning themselves: Alice is a student; Alice is from Phoenix; Phoenix is a hot city; students are people; cities are places; if it's snowing, it's cold. Then the question — is it snowing? The room answers "I don't know," and he agrees, because nothing yet connects snow to anything in the KB.
 

Then he adds the conditional that does the real work: if a person is from a hot place and it is snowing, that person is not happy. Asked again, the KB still says "I don't know." Add one more fact, that Alice is happy, and the answer flips — or at least, that's the strong implication. The room audibly waffles between "I don't know" and "no" (2:51), and the lecturer declines to settle it: he says to ponder it offline and moves on (3:07). That bugged me. As far as I could trace it, Alice is a student, therefore a person; she's from Phoenix, which is a city, therefore a place, and a hot one; so the conditional's antecedent is half-satisfied, and her being happy rules out the snowing half. "No" should be the answer. But he never confirms it on tape, and for a puzzle that's meant to sell the whole apparatus, leaving it dangling felt like a missed beat.
 

The point of the demo, though, lands: a pile of sentences with conjunctions, implications, and quantifier-like English gets you a nontrivial conclusion, and the two questions hovering over the rest of the hour are what sentences this formalism can capture and how you mechanically get answers out of it (3:24). He's candid that first-order logic won't cover every sentence anyone can write, but claims it goes quite far.
 

What the previous lecture already gave us

 

From about 4:03 he rebuilds the propositional machinery, and it's worth having straight because first-order logic reuses every piece of it. A logic is three things: a syntax, a semantics, and inference rules. The mental picture he wants is two territories. In syntax-land you have symbols and rules that churn symbols into more symbols; meaning only arrives through an interpretation function that says what statement a formula makes about the world. Soundness and completeness are then the two properties governing how the symbol-shuffling relates to reality.
 

Then the vocabulary, quickly: primitives are propositional symbols like P, Q, rain, wet; connectives combine them recursively; a model is a truth assignment to those primitives, and a model is also a world — one candidate reality. There are many, and we don't know which one we're actually in, which is the whole reason reasoning is work. Formulas are how you carve down the set of candidate worlds. The interpretation function takes a formula plus a model and returns whether the formula holds there.
 

A knowledge base is the running set of formulas an agent has accumulated, and its models are the intersection of the models of each individual formula — every state of affairs consistent with everything known at once. Drop a new formula in and exactly three things can happen. If the model set doesn't shrink, the new formula was already implicit, and that's entailment. If it shrinks to nothing, you've got a contradiction. Anything else is a contingency: shrunken but non-empty. Those three cases are what implement ask (classify a formula as entailed, contradictory, or contingent) and tell (add a formula, but only if it's contingent — you don't want to store contradictions or redundant facts).
 

He then collapses all of it onto satisfiability. Take satisfiability as your primitive operation; entailment, contradiction, and contingency each reduce to a couple of SAT calls — add the formula and check, then add its negation and check (10:38).
 

Finally, the syntactic side: inference rules like modus ponens let a knowledge base derive or prove a formula, which is a purely syntactic achievement, while entails is a semantic one about models. Two very different-looking notions, bridged by soundness and completeness. His image: think of the set of entailed truths as a glass. Soundness means whatever you pour in stays inside the glass — you never prove something false. Completeness means you can fill the glass — every genuine consequence is reachable. Soundness is "nothing but the truth," completeness is "the whole truth," and you want both (12:51).
 

Why Propositional Logic Runs Out of Room, and What First-Order Logic Adds

 

The two missing ingredients

 

Around 14:00 he turns on the previous lecture. "Alice and Bob both know arithmetic" is fine: two propositional symbols, conjoined. "All students know arithmetic" is where it breaks. You end up writing one implication per student — Alice is a student implies Alice knows arithmetic, same for Bob — and with a thousand students you have a thousand implications. The Goldbach example (15:01) kills it outright: to state "every even integer greater than two is the sum of two primes," you'd need one symbol per integer. Propositional logic has no way to say "all" without enumerating.
 

The diagnosis is that two things are missing. First, objects and predicates — "Alice knows arithmetic" is a single opaque boolean, but it plainly has internal structure, an Alice and an arithmetic inside it, and we want to prise that apart. Second, quantifiers and variables, so that "all" can be said once instead of once per object. His analogy is the one I'd remember from this section: working without quantifiers is like programming without for loops (15:59). You can write everything out by hand, in principle. Nobody does.
 

Terms stay on one side of the line, formulas on the other

 

The formal machinery starts at 16:56, and the single most useful thing in the whole lecture is the split he draws: terms denote objects, formulas denote truth values, and never the twain shall meet.
 

Terms come in three flavors. Constants like Alice or arithmetic name objects — and these are not propositional symbols, because Alice isn't true or false, she's a thing (17:51). Variables like x and y. And functions, which take one or more terms and hand back another term: father-of applied to Alice, or add applied to x and y. Because functions return terms, you can nest them indefinitely, building father-of-father-of-Alice and so on (19:05).
 

Formulas are built from atomic formulas, and an atomic formula is a predicate applied to terms. Predicates are the boolean-returning cousins of functions, and they carry an arity: snowing is nullary, student is unary, knows is binary (20:15). Once you have atomics, the old connectives work exactly as before, and then quantifiers let you bind a variable appearing in a formula, universally or existentially (21:39).
 

The part I'd have benefited from seeing more of is his list of non-formulas (22:48), because it's where the object/truth-value split gets teeth. father(x) is a term, not a formula — a person isn't a boolean. student(knows(Alice, arithmetic)) is nonsense because a predicate returns a boolean and nothing accepts booleans as arguments. His example of the classic blunder is good: asked to formalize "students know arithmetic," the instinct is to slot student in where Alice went, and that's simply wrong (25:04). There's also a notational convention worth memorizing for the homework: lowercase for terms, uppercase for formulas.
 

A student asks whether a function can return another function, and the answer is no — functions return terms (24:02). He uses the moment to make a point that echoes much later in the hour: first-order logic is far more restricted than a language like Python. The restriction is deliberate. Tighter language, easier computation, less you can say.
 

First-Order Logic Semantics: A Failed Attempt, Then Domains and Interpretation

 

Attempt one collapses under functions

 

Semantics begins at 26:03 with an honest attempt to just copy propositional logic: a model is a truth assignment to atomic formulas, so knows(Alice, arithmetic) is true and student(Alice) is true, done. He asks the room what's wrong with it, and there are two fatal problems.
 

With functions in the language, father(Alice), father(father(Alice)), and so on generate infinitely many terms, hence infinitely many atomic formulas, so a single model would need infinitely many truth values (28:23). Worse, truth-assignment-per-atomic-formula has no way to know that two different terms denote the same object. If Bob is Alice's father, nothing stops your model from saying the father-of-Alice knows arithmetic while Bob doesn't — and that's incoherent in a way the formalism can't see (29:26).
 

The domain as a layer of indirection

 

The fix is to insert a layer of indirection (30:33). A model in first-order logic is a pair: a domain, which is just a set of objects, and an interpretation function mapping symbols into that domain. Constants get mapped to objects — Alice to O1, Bob to O2, arithmetic to O3. Functions get mapped to actual object-to-object mappings defined purely over domain elements, never mentioning the constant symbols from syntax-land. Predicates get mapped to functions from tuples of objects to true or false.
 

A student asks whether that mapping is hardcoded, and the answer is nuanced: mathematically it's just an object, and in practice you'd instantiate it lazily and partially rather than write the whole table out (34:20). Then comes the picture I found most clarifying in the entire lecture (35:37): draw the domain as nodes in a graph. Constants become labels or pointers onto nodes — and there need not be a one-to-one relationship, which is why he throws in a "Robert" pointing at the same node as "Bob." Unary predicates attach to a subset of nodes; binary predicates become edges between pairs. If you've heard of knowledge graphs, he says, they have their roots right here.
 

Interpreting a formula, recursively

 

Now the interpretation function itself (36:47). It takes a formula, a world, and a variable-to-object substitution, and recurses over the structure. For an atomic binary predicate like knows(Alice, arithmetic), you look up what the predicate symbol denotes in that world, recursively interpret each argument as a term — Alice resolves to O1, arithmetic to O3 — and feed those objects into the predicate's mapping. Result: true.
 

Quantifiers are handled by brute force over the domain. To evaluate for all x, knows(x, arithmetic), you walk every object in the domain, extend the substitution with variable ↦ object, and check the body each time; one failure sinks the whole thing, and in his running example it fails because O2 doesn't know arithmetic (42:11). A student then asks why and and or are treated differently from ordinary predicates, and the answer is precisely the split from the syntax section: a binary predicate is atomic, its arguments are terms that evaluate to objects, and the boolean only appears when you look that tuple up under the world's interpretation (44:45).
 

Making Inference Go: Propositionalization, Modus Ponens, and Unification

 

The cheap route: pretend it's propositional

 

Inference starts at 45:50 with the demotion-first strategy: can we just turn this into propositional logic and reuse everything from lecture one? Sometimes yes, under two assumptions. Unique names says each object answers to at most one constant; domain closure says each object answers to at least one (46:51). Together they force a one-to-one correspondence between objects and constants, and then you can propositionalize: flatten every atomic formula into one monolithic symbol, expand every universal into a big conjunction over all instantiations, and expand every existential into a big disjunction. At that point first-order logic is, in his phrase, syntactic sugar — same expressive reach, far nicer to read and write (48:55). He's clear this is the easy case and doesn't generalize.
 

Definite clauses and the rule that won't fire

 

The real machinery starts with a restricted formula shape called a definite clause: universally quantified variables, a conjunction of atomic formulas on the left, a single atomic formula on the right (50:13). Anything with disjunction is out, and so is an existentially quantified conclusion — because, as he puts it, for all is compact conjunction and exists is compact disjunction (51:25).
 

Modus ponens over definite clauses should then be trivial, and his example shows why it isn't (52:42). The KB says Alice took 221 and 221 covers logic. The rule says: for all x, y, z, if x takes y and y covers z, then x knows z. Obviously we should conclude Alice knows logic. But the rule engine does string matching. takes(Alice, 221) and takes(x, y) are not the same string, so nothing fires. His aside here is worth remembering: it's kind of dumb, but the rules are just the rules (54:09).
 

The way out is to notice what for all really licenses. A universally quantified clause is a template; you may set x, y, and z to anything you like, including the concrete constants sitting in your KB (55:25).
 

Substitution, unification, and modus ponens take two

 

Two tools get defined. Substitution is recursive search-and-replace on variables inside a formula, and the replacement can itself be a variable, not just a constant (56:48). Unification is generalized equality: given two formulas, find a substitution that makes them identical, and fail if none exists. Only variables can be replaced — you can map x to Alice, but you cannot map Alice to Bob (59:12). His examples: unifying gives {x → Alice, y → Bob}; knows(Alice, y) against knows(x, z) yields {x → Alice, y → z}; knows(Alice, y) against knows(Bob, z) simply fails.
 

Modus ponens is then upgraded (1:01:18). You don't match the premises against the rule head; you unify them, collect the resulting substitution, and apply it to the rule's conclusion. In the running example, unifying takes(Alice, 221) ∧ covers(221, logic) with takes(x, y) ∧ covers(y, z) yields {x → Alice, y → 221, z → logic}, and applying that to knows(x, z) gives knows(Alice, logic). That's the gap between general variables and concrete facts, closed.
 

The cost accounting matters (1:03:43). Every firing produces an atomic formula, so with no functions in the language there's a finite ceiling: the number of constants raised to the maximum predicate arity. Add functions and the space can be infinite — knows(Alice, logic), knows(father(Alice), logic), knows(father(father(Alice)), logic) — and you can write rules that generate forever, like "if x knows logic then father-of-x knows logic."
 

And then the honest caveat: this version of modus ponens is sound but not complete (1:05:10). Anything you derive is true. But there are entailed formulas you can't reach — anything requiring disjunctive conclusions, for instance. Resolution is the rule that buys completeness for first-order logic, and he explicitly skips it, pointing to earlier lectures.
 

Translating English Into First-Order Logic, and Where the Lecture Stops

 

"For all" wants an implication, "there exists" wants an and

 

The last stretch (1:07:27) is the practical one, homeworks facing. "Alice and Bob both know arithmetic" is a conjunction of two atomic formulas. "All students know arithmetic" is for all x, student(x) → knows(x, arithmetic). "Some student knows arithmetic" is exists x, student(x) ∧ knows(x, arithmetic).
 

Then the heuristic I'd write on my hand before an exam: universals almost always pair with an implication, existentials almost always pair with a conjunction (1:08:20). He explains why the wrong pairings are wrong rather than just forbidding them. for all x, student(x) ∧ knows(x, arithmetic) asserts that everything in the domain is a student who knows arithmetic. exists x, student(x) → knows(x, arithmetic) is satisfied by the first non-student you can find, since the implication goes vacuously true. Both are disasters.
 

Two harder examples close it out. "There is some course that every student has taken" becomes exists x, for all y, student(y) → takes(y, x), with his own note that strictly you also want a course(x) conjunct in there (1:10:11). Goldbach becomes for all x, (even(x) ∧ x > 2) → exists y, z, prime(y) ∧ prime(z) ∧ y + z = x. And the student/course/concept sentence is a genuine definite clause, meaning modus ponens will actually do something with it — unlike the Goldbach and "some course" sentences, which aren't (1:12:14). His framing of the skill is fair: it's like turning informal specs into code, just a new language to get used to.
 

The limits he named, and one he half-named

 

He ends by naming the ceiling himself (1:14:29). Try writing "70% of students know machine learning" in first-order logic and you can't — you'd need to quantify over sets of objects, not just objects, and that pushes you into higher-order logics. It loops back neatly to the earlier answer about functions not being able to return functions: first-order logic trades expressiveness for tractability, deliberately, and quantification over sets is part of what it gives up.
 

My one substantive complaint with the lecture is structural rather than mathematical. The unification section is where the class clearly needed the most hand-holding — the recursion, the prime/unprime distinction between the KB facts and the rule's antecedents, the fact that you apply the unifier to the conclusion rather than concluding the conclusion — and it went by fast, on slides, with the recording's captions garbling the notation. The opening snow puzzle got the same treatment: raised, then deferred. Both are the kind of thing I'd want a section or a problem set to sit with.
 

The hour closes with logistics: logic is finished, the last three lectures zoom out to language models and AI in society, and the final session is a fireside-chat-style class with presentations (1:15:22).
 

For all the machinery, the takeaway I'd carry forward is the shape of the thing: a language where objects and truth values are rigorously separated, a semantics built on a domain you interpret symbols into, and inference that only works once you let variables be matched rather than merely compared. Everything else in the lecture is elaboration on those three moves.
 

Content Disclaimer:

This article is for general reference only and does not constitute professional R&D guidance, production process advice or quality certification. All material performance data has specific test premises; readers should verify parameters against actual equipment and working conditions.