One. Course Details
This is the second of two lectures on formal logic in Stanford University's CME 296: Diffusion and Large Vision Models. Building on the previous lecture covering propositional logic, this session introduces first-order logic—a significantly more expressive formal language that addresses the critical limitations of propositional logic for representing general knowledge about the world.
The lecture follows a rigorous three-part structure common to all formal logic systems: it first defines the syntax of first-order logic, then establishes its formal semantics, and finally presents sound inference rules for deriving new knowledge from existing facts. It concludes with practical guidance for translating natural language statements into logical expressions, a skill directly applicable to the course assignments. The central thesis is that first-order logic provides a powerful, mathematically precise framework for representing structured knowledge and performing automated reasoning that closely mirrors human deductive thinking.
Two. Key Learning Takeaways
Propositional logic is fundamentally limited because it can only represent atomic facts as monolithic symbols, making it impossible to express general statements about categories of objects or relationships between objects.
First-order logic introduces three critical extensions over propositional logic: terms that represent objects, predicates that express properties and relations, and quantifiers that allow statements about all or some objects in a domain.
A model in first-order logic consists of two components: a domain of objects and an interpretation function that maps constant symbols, function symbols, and predicate symbols to elements and relations over the domain.
Substitution and unification are the foundational operations that enable generalized inference in first-order logic, allowing rules with variables to be applied to specific concrete facts.
Modus ponens extended with unification is a sound inference rule for definite clauses, though it is not complete for the full first-order logic language.
Universal quantifiers (∀) are almost always paired with implication, while existential quantifiers (∃) are almost always paired with conjunction—a rule that holds for over 99% of natural language translations.
First-order logic is still not sufficiently expressive to represent probabilistic statements or higher-order concepts, requiring extensions for many real-world AI applications.
Three. Course Gold Quotes
"Propositional logic is like programming without for loops. You have to write down every single case individually, which clearly doesn't scale."
"Logic is a language for representing knowledge and reasoning with it. It gives us a precise way to say what we mean and derive what follows from what we know."
"Soundness means you only prove true things. Completeness means you can prove all true things. Ideally, you want both: nothing but the truth, and the whole truth."
"The goal of logic is not to replace human reasoning. It is to formalize it, so we can build machines that can reason correctly and consistently."
"Natural language is incredibly powerful because I can say a few words and communicate very complicated ideas. First-order logic gives us that same power in a formal system."
"Unification is generalized equality. It finds the substitution that makes two different terms mean exactly the same thing."
"Most of the time, when you make a mistake translating natural language to logic, it's because you paired the wrong connective with your quantifier."
Four. Layered Learning Notes
Module 1: The Limitations of Propositional Logic
The lecture opens by motivating first-order logic through a demonstration of propositional logic's fundamental limitations. While propositional logic works well for representing simple facts and combinations of facts, it cannot express general statements about categories of objects.
For example, the statement "Alice and Bob know arithmetic" can be easily represented in propositional logic as two separate propositions: AliceKnowsArithmetic ∧ BobKnowsArithmetic. However, the general statement "all students know arithmetic" cannot be expressed compactly. In propositional logic, you would need to write a separate implication for every individual student: StudentAlice → AliceKnowsArithmetic ∧ StudentBob → BobKnowsArithmetic ∧ .... This becomes completely impractical when there are hundreds or thousands of students, and impossible when the set of objects is infinite.
Similarly, mathematical statements like Goldbach's conjecture ("every even integer greater than two is the sum of two primes") cannot be expressed in propositional logic at all, as they require quantifying over an infinite domain of integers.
The core missing elements in propositional logic are:
-
Objects and relations: The ability to break statements into subjects and predicates (e.g., separating "Alice" and "knows arithmetic" into distinct components)
-
Variables and quantifiers: The ability to make statements about all objects or some objects in a domain, rather than enumerating them individually
Module 2: The Syntax of First-Order Logic
First-order logic extends propositional logic with a richer syntax that distinguishes between two types of expressions: terms, which denote objects, and formulas, which denote truth values.
Terms are the basic building blocks that refer to objects in the world. There are three types of terms:
-
Constant symbols: Represent specific individual objects (e.g.,
Alice,Bob,Arithmetic) -
Variables: Represent arbitrary objects (e.g.,
x,y,z) -
Function symbols: Take one or more terms as arguments and return another term (e.g.,
father(Alice),add(x, y))
Terms can be nested arbitrarily to represent complex objects. For example, father(father(Alice)) represents Alice's paternal grandfather.
Formulas are statements that can be true or false. Atomic formulas consist of a predicate symbol applied to one or more terms:
-
Zero-arity predicates (propositions):
Snowing() -
Unary predicates (properties):
Student(Alice),Hot(Phoenix) -
Binary predicates (relations):
Knows(Alice, Arithmetic),From(Alice, Phoenix)
Complex formulas are built from atomic formulas using the same logical connectives as propositional logic: ¬ (not), ∧ (and), ∨ (or), → (implies), and ↔ (if and only if).
Finally, first-order logic adds two quantifiers that bind variables:
-
Universal quantifier (∀): "For all x, P(x) is true"
-
Existential quantifier (∃): "There exists at least one x such that P(x) is true"
A critical syntactic convention is that terms (objects) are written in lowercase, while predicates (truth-valued functions) are written in uppercase. This helps avoid the common mistake of passing a predicate as an argument to another predicate, which is not allowed in first-order logic.
Module 3: The Semantics of First-Order Logic
The semantics of first-order logic define what syntactic expressions mean in terms of a possible world or model. Unlike propositional logic, where a model is simply an assignment of truth values to propositions, a first-order model has a more complex structure:
-
Domain: A non-empty set of objects that the logic is talking about
-
Interpretation function: A mapping that assigns:
-
Each constant symbol to an object in the domain
-
Each function symbol to a function over the domain
-
Each predicate symbol to a relation over the domain
-
This layer of indirection solves the two major problems with a naive propositional-style semantics for first-order logic:
-
It handles infinite domains and functions naturally, without requiring an infinite number of atomic propositions
-
It correctly captures the fact that different terms can refer to the same object (e.g.,
Bobandfather(Alice)might both map to the same object in the domain)
The interpretation function is extended recursively to evaluate complex terms and formulas. To evaluate a quantified formula like ∀x P(x), we check if P(x) is true for every possible assignment of x to an object in the domain. For ∃x P(x), we check if there exists at least one assignment that makes P(x) true.
All the semantic definitions from propositional logic—entailment, contradiction, contingency, satisfiability—carry over directly to first-order logic with this extended model definition.
Module 4: Inference in First-Order Logic
The lecture presents two main approaches to performing inference in first-order logic: propositionalization and generalized modus ponens.
Propositionalization is the simplest approach, applicable when two assumptions hold:
-
Unique names assumption: Each object is referred to by exactly one constant symbol
-
Domain closure assumption: Every object in the domain is referred to by some constant symbol
Under these assumptions, we can convert any first-order knowledge base into an equivalent propositional knowledge base by:
-
Replacing each atomic formula with a propositional symbol (e.g.,
Student(Alice)becomesStudent_Alice) -
Expanding universal quantifiers into conjunctions over all constants
-
Expanding existential quantifiers into disjunctions over all constants
Once propositionalized, we can use any standard propositional inference algorithm. However, this approach fails when there are functions (which generate an infinite number of terms) or when the domain is large or unknown.
Generalized modus ponens is a more powerful inference rule that works directly with first-order formulas. It extends the propositional modus ponens rule with two new operations:
-
Substitution: A search-and-replace operation that replaces variables with terms in a formula
-
Unification: An algorithm that finds the most general substitution that makes two terms identical
The generalized modus ponens rule states:
-
If we have premises
A₁', A₂', ..., Aₖ' -
And we have a definite clause
∀x₁...xₙ (A₁ ∧ A₂ ∧ ... ∧ Aₖ → B) -
And there exists a substitution θ such that
unify(Aᵢ', Aᵢ) = θfor all i -
Then we can conclude
substitute(θ, B)
This rule is sound for definite clauses (universally quantified implications with conjunctions of atomic formulas in the antecedent and a single atomic formula in the consequent). While it is not complete for the full first-order logic language, it is sufficient for many practical AI applications and forms the basis of logic programming languages like Prolog.
Module 5: Translating Natural Language to First-Order Logic
The lecture concludes with practical guidance for translating natural language statements into first-order logic, a skill that will be tested on the course assignments.
The most important rule to remember is the quantifier-connective pairing:
-
Universal quantifiers (∀) almost always go with implication (→)
-
Existential quantifiers (∃) almost always go with conjunction (∧)
This rule holds for over 99% of natural language translations. Common mistakes include:
-
Writing
∀x (Student(x) ∧ Knows(x, Arithmetic)), which incorrectly states that every object in the domain is both a student and knows arithmetic -
Writing
∃x (Student(x) → Knows(x, Arithmetic)), which is trivially true if there exists any object that is not a student
The lecture provides several examples of correct translations:
-
"All students know arithmetic":
∀x (Student(x) → Knows(x, Arithmetic)) -
"Some student knows arithmetic":
∃x (Student(x) ∧ Knows(x, Arithmetic)) -
"There is some course that every student has taken":
∃x (Course(x) ∧ ∀y (Student(y) → Takes(y, x))) -
Goldbach's conjecture:
∀x (Even(x) ∧ GreaterThan(x, 2) → ∃y ∃z (Prime(y) ∧ Prime(z) ∧ Equal(x, Add(y, z))))
Translating natural language to logic is similar to translating informal specifications into code: it requires careful attention to the precise meaning of the original statement and practice with the formal language.
Wishing you clarity and precision as you master the foundations of formal logic. May you develop the ability to translate vague natural language ideas into precise logical statements, and may this skill serve you well in all your future AI work. Whether you go on to build knowledge bases, design reasoning systems, or simply improve your own critical thinking, may you always appreciate the power of clear, rigorous thought. Good luck with your assignments and all your future endeavors!


