Artificial Intelligence · AI Foundations
First-Order Logic and Unification
In AI because 'every student who borrowed this book is a person' is one sentence, not one atom per student — and first-order logic is the language that sentence lives in.
Propositional logic can say 'Priya borrowed Dune' as one atom, and it cannot say 'every borrower is a student' except by writing a new atom for every person the registrar will ever enrol. First-order logic (FOL) adds objects, relations and the words all and some, so one quantified sentence covers the unbounded list. The Knowledge Engineering and Hybrid Systems lesson already named that expressiveness and its semi-decidable bill; this lesson is the language itself — predicates, quantifiers, what an interpretation is, and unification, the matching step every later proof procedure will call. Inference — forward chaining, backward chaining, resolution — is the next lesson.
- Artificial Intelligence
- Medium level
- 5 concepts
1Objects, not just whole sentences
A propositional atom names a whole claim and has no insides. 'PriyaBorrowedDune' does not contain Priya, and it does not contain Dune, so the KB cannot reuse those pieces in another sentence. FOL starts from objects — Priya, Dune, CS201 — and builds claims by relating them.
The campus running example is the library. People and books are objects. Student, Book and Person are properties of one object. Borrowed is a relation on two. One sentence, 'every student is a person', then applies to every object the registrar adds next year, without a new atom. That is the move the propositional language cannot make, and it is the whole reason this lesson exists.
| Want to say | Propositional | First-order |
|---|---|---|
| Priya borrowed Dune | one atom | Borrowed(Priya, Dune) |
| Every student is a person | one atom per student | \forall x\, (Student(x) \rightarrow Person(x)) |
2Predicates, functions, constants
A constant names one object: Priya, Dune. A variable stands in for an object and will be bound by a quantifier: x, y. A function names an object in terms of others: \mathrm{advisor}(\mathrm{Priya}) is whoever advises Priya — still one object, not a yes/no. A predicate is the yes/no: \mathrm{Student}(x), \mathrm{Borrowed}(x,y). Together, \mathrm{Borrowed}(\mathrm{Priya}, \mathrm{Dune}) is an atomic sentence.
Arity is how many objects a symbol takes. Student is arity 1; Borrowed is arity 2; advisor is a function of arity 1. Mixing them — writing Student(Priya, Dune) — is not a sentence of this language. A term is a constant, a variable, or a function applied to terms; only a predicate applied to terms is a sentence you can ask the truth of.
| Symbol | Kind | Arity | Reads as |
|---|---|---|---|
| Priya, Dune | constant | 0 | this person, this book |
| x, y | variable | 0 | some object, not yet named |
| advisor(x) | function | 1 | the advisor of x |
| Student(x) | predicate | 1 | x is a student |
| Borrowed(x, y) | predicate | 2 | x borrowed y |
What expressive elements does First-Order Logic add beyond propositional logic?
- Objects, relations (predicates), functions, and quantifiers (universal and existential)
- Continuous floating-point gradient tensors and neural activations
- Strictly binary boolean variables with no relational structure
- Unsupervised clustering centroids in multi-dimensional space
FOL represents objects, properties, relations, functions, and quantification (orall, \exists), dramatically increasing expressiveness over propositional logic.
3All, and some
\forall x\, P(x) says P holds of every object in the domain. \exists x\, P(x) says P holds of at least one. The library's safety rule is \forall x\, (\mathrm{Student}(x) \rightarrow \mathrm{Person}(x)): if x is a student, x is a person. An existential that matters here is \exists y\, \mathrm{Borrowed}(\mathrm{Priya}, y): Priya borrowed some book, even if the KB does not name which.
The connective under a universal is almost always an implication, not a conjunction. \forall x\, (\mathrm{Student}(x) \wedge \mathrm{Person}(x)) would claim that every object in the domain is both a student and a person, including Dune. The arrow restricts the claim to the students. Under an existential the usual connective is a conjunction: \exists x\, (\mathrm{Student}(x) \wedge \mathrm{Borrowed}(x, \mathrm{Dune})) says some student borrowed Dune, which is what the English means.
| Shape | Reads as | Broken twin |
|---|---|---|
| \forall x\, (S(x) \rightarrow P(x)) | every student is a person | \forall x\, (S(x) \wedge P(x)) — everything is both |
| \exists x\, (S(x) \wedge B(x, d)) | some student borrowed Dune | \exists x\, (S(x) \rightarrow B(x, d)) — true if any non-student exists |
4An interpretation is a world of objects
A propositional world assigned true or false to every atom. An FOL interpretation does more: it names a domain of objects, maps each constant to one of them, maps each function to a function on the domain, and maps each predicate to the set of tuples it holds of. Truth of a sentence is then defined against that interpretation, the same way propositional truth was defined against a world.
A tiny library domain \{p, d\} with Priya \mapsto p, Dune \mapsto d, Student = \{p\}, Book = \{d\}, Borrowed = \{(p, d)\} makes \mathrm{Borrowed}(\mathrm{Priya}, \mathrm{Dune}) true and \mathrm{Student}(\mathrm{Dune}) false. The universal \forall x\, (\mathrm{Student}(x) \rightarrow \mathrm{Person}(x)) is true here only if Person also contains p. Entailment is the same word as before: the KB entails a query when every interpretation that satisfies the KB also satisfies the query. The next lesson is how a machine searches for a proof of that.
Figure. An FOL interpretation names a domain and maps constants, functions and predicates onto it. Domain {p, d}: Priya maps to p, Dune to d. Borrowed = {(p, d)} makes Borrowed(Priya, Dune) true; Student = {p} makes Student(Dune) false.
Truth in a two-object library
Domain {p, d}. Priya maps to p, Dune to d. Student = {p}, Book = {d}, Borrowed = {(p, d)}, Person = {p}.
- Borrowed(Priya, Dune) against {(p, d)}true
- Student(Dune) against {p}false
- Student(x) → Person(x) at x = ptrue → true
- Student(x) → Person(x) at x = dfalse → true
- ∀x (Student(x) → Person(x))true in this interpretation
Pro tip. The implication at Dune is true because the premise is false — the same reading as propositional 'if'. A missing Person(p) would have failed the student case and made the universal false.
5Unification
A proof step will often need two atomic sentences to become the same sentence. Unification is the algorithm that finds a substitution \theta — a list of variable-to-term bindings — such that A\theta and B\theta are identical, or reports that none exists. \mathrm{Borrowed}(\mathrm{Priya}, z) and \mathrm{Borrowed}(x, \mathrm{Dune}) unify with \{x/\mathrm{Priya},\, z/\mathrm{Dune}\}, and both become \mathrm{Borrowed}(\mathrm{Priya}, \mathrm{Dune}).
Two failures are load-bearing. A clash: \mathrm{Borrowed}(\mathrm{Priya}, \mathrm{Dune}) and \mathrm{Borrowed}(\mathrm{Omar}, z) cannot unify, because Priya and Omar are different constants. An occur-check: a variable cannot be bound to a term that already contains it, because no finite term equals a function of itself. The most general unifier (MGU) is a unifier that any other unifier is a further substitution of — \{x/\mathrm{Priya}, z/\mathrm{Dune}\} is an MGU of the first pair; adding an extra unused binding is a unifier too, just a more specific one. The next lesson's proof procedures always keep an MGU, so they do not commit to extra bindings they were not forced into.
Figure. Borrowed(Priya, z) and Borrowed(x, Dune) unify with the MGU {x/Priya, z/Dune}. Borrowed(Priya, Dune) and Borrowed(Omar, z) clash because Priya and Omar are different constants. x with advisor(x) fails the occur-check: a variable cannot be bound to a term that already contains it.
Unify, clash, or occur-check
Three pairs from the library vocabulary.
- Borrowed(Priya, z) with Borrowed(x, Dune)MGU {x/Priya, z/Dune}
- Borrowed(Priya, Dune) with Borrowed(Omar, z)clash — Priya ≠ Omar
- x with advisor(x)occur-check — fail
Pro tip. The third pair is the occur-check in campus clothes: x would have to equal advisor(x). Write the two terms down and see whether a variable is being asked to equal a term that contains it.
Coding lab. First-Order Logic unification runs in the app, with checks on your output.
Can Borrowed(Priya, z) unify with Borrowed(Omar, Dune)?
- No — Priya and Omar clash, and a variable on the other argument cannot repair a constant clash
- Yes, with {z/Dune, Priya/Omar}
- Yes, with {z/Dune} only
- Only after rewriting both as propositions
Unification never rewrites a constant into another constant. z can become Dune, but Priya cannot become Omar. That is a clash, not a missing binding.
Notes
- First-order logic adds objects, relations, functions and quantifiers to the propositional language.
- An interpretation names the objects and says which tuples each predicate holds of.
- Unification finds a substitution that makes two atomic sentences look the same, if one exists.
Formulas
- Universal: \forall x\, P(x) is true when P holds of every object in the domain
- Existential: \exists x\, P(x) is true when P holds of at least one object
- Most general unifier: a substitution \theta such that A\theta = B\theta, and any other unifier is a further substitution of \theta
Exam traps & shortcuts
- A free variable is not a sentence — bind it with \forall or \exists before you ask about truth.
- Unification fails on a clash (two different constants) and on an occur-check (x cannot unify with f(x)).
- The Knowledge Engineering glimpse of FOL named the semi-decidability bill; this lesson owns the language that bill is paid on.
Recap
Next: FOL inference.
- Insides
- Objects, functions and predicates give a sentence reusable parts. One universal covers next year's students.
- Quantifiers
- ∀ with → for 'every S is P'. ∃ with ∧ for 'some S is P'. The swapped connectives mean something else.
- Interpretation
- A domain, plus a mapping for every symbol. Entailment is still 'true in every model of the KB'.
- Unification
- Find an MGU that makes two atoms identical. Clash and occur-check are the two honest failures.
Practise First-Order Logic and Unification
Reading is free and needs no account. Practice, mocks and progress live in the app.
- 2 quick checks with worked explanations
- Timed mocks scored with the real marking scheme
- Readiness tracked per topic, kept on your device