Last updated: 2026-09-18
Predicate Logic
Set Theory for Computing uses a predicate — P(x), true or false depending on x — informally, to describe a set by a rule rather than a listing. Predicate logic is what happens when that informal use is made precise: a small formal language for stating exactly what a predicate can say, how predicates combine, and — crucially, beyond plain propositional logic — how to talk about every or some member of a domain without naming them one at a time. Frege's original formulation, the first system complete enough to handle both plain propositions and quantified statements about "all" and "some" in one framework, is the historical starting point for everything below1; Enderton's textbook is the standard modern route to the rigorous version of the same material2.
From Propositions to Predicates
Propositional logic combines whole statements with connectives — ∧ (and), ∨ (or), ¬ (not), → (implies) — and can already say things like "it is raining ∧ ¬(I have an umbrella) → I get wet." What it can't do is reach inside a statement: "every book in the library has an author" isn't one proposition, it's a claim about every member of a whole collection, and propositional logic has no machinery for "every member of a collection." Predicate logic adds exactly that machinery: a predicate like HasAuthor(b) is true or false depending on what b is substituted in for, and two quantifiers state how many members of a domain a predicate has to hold for:
| Symbol | Reads as | Example |
|---|---|---|
| ∀x | for all x (universal quantifier) | ∀b ∈ Books, HasAuthor(b) — every book has an author |
| ∃x | there exists an x (existential quantifier) | ∃b ∈ Books, Overdue(b) — at least one book is overdue |
Order matters, and swapping two quantifiers can change a statement's meaning entirely: ∀m ∈ Members, ∃b ∈ Books, Borrowed(m, b) says every member has borrowed at least one book (possibly a different book per member), while ∃b ∈ Books, ∀m ∈ Members, Borrowed(m, b) says there's one specific book every single member has borrowed — a much stronger, and for a real library, almost certainly false, claim built from the exact same three symbols in a different order.
Free and Bound Variables
In ∀b ∈ Books, HasAuthor(b), the variable b is bound by the quantifier — it has no meaning outside the formula, and renaming it (∀x ∈ Books, HasAuthor(x)) changes nothing at all. A variable not captured by any quantifier is free, and a formula with a free variable isn't true or false on its own — HasAuthor(b) alone is only a claim once something concrete is substituted for b, exactly the same distinction a function's parameter (bound to whatever's passed in when it's called) has against a global variable referenced from outside.
Predicate Logic in a Query Language
SQL is predicate logic with the quantifiers spelled out as keywords rather than symbols. A plain WHERE clause, as the set theory companion page covers, is a quantifier-free predicate applied to one row at a time. EXISTS and NOT EXISTS are the existential and (negated) universal quantifiers directly: WHERE EXISTS (SELECT 1 FROM loans WHERE loans.book_id = books.book_id) is literally ∃l ∈ Loans, book_id(l) = book_id(this row) — "there exists a loan referencing this book." A join's ON condition is a predicate with two free variables, one bound to each table's row, made concrete exactly the way a two-argument predicate like Borrowed(m, b) above is made concrete once m and b are both supplied. None of this is analogy for teaching purposes — a query planner's job is precisely to decide, mechanically, an efficient order in which to check a predicate logic formula against however many rows a table holds.
Predicate Logic as a Programming Language
Predicate logic doesn't have to stay a language for describing things — it can be executed directly. Paradigms & Polyglot Programming covers how Prolog, and logic programming generally, turns a restricted fragment of predicate logic (Horn clauses — facts and rules of the form "if these things are true, so is this") into a program a resolution engine can run: declare what's true, and let the engine search for values that satisfy a query, rather than writing the search by hand.
Toward Formal Methods
One more use of predicate logic matters enough to have its own page: attaching a predicate to a specific point in a program — "when execution reaches here, this must be true" — is the entire logical basis for reasoning formally about what a program does, before or instead of just running it and checking the output. Formal Methods: Specifying Before You Build picks this up directly.