A Crash Course in Predicate Logic

Hillel Wayne wrote Logic for Programmers because he couldn't find a good resource on logic written for programmers. Once the book was out, the missing thing was a free one. So on 2026-09-01 he published its second chapter as a blog post, adding the footnotes as editorial comments that are not in the book crash-course-predicate-logic. The chapter covers what the rest of the book leans on: predicates, the implication operator, sets, the two quantifiers, and the rewrite rules that let a formula be simplified the way arithmetic is. It ends by saying that is all the basics of formal logic, and that the hard part is application — knowing division is different from seeing that scaling a five-egg recipe to three eggs is a division problem.

Notation chosen for programmers

Wayne drops symbols that aren't on a keyboard. AND, OR and NOT are &&, || and !, implication is =>, and the quantifiers are spelled all and some instead of ∀ and ∃. Set union, intersection and difference borrow |, & and -. Predicates are TitleCase, ordinary functions snake_case. Set comprehensions use an explicit map-and-filter form, {x^2 for x in set: x > 2}, because beginners tend to confuse which side of the standard {f(x) | P(x)} does the mapping and which the filtering.

The last section defends this. Logic is a language, and inventing new constructs is encouraged as long as they are consistent and explained. He adds ranges, 1..=100 and 1..<100, and pins down the ambiguous case by defining a..=b as empty when a > b. For long requirements he introduces numbered conjunction lists, where numbers and letters mean AND and a || prefix marks alternatives.

Predicates are not functions

A predicate is, to a first approximation, a function that returns a Boolean. The difference is that a predicate only defines what the answer is, while a program function also has to compute it. That lets predicates range from the concrete (Positive(x) = x > 0) to things nobody can compute, such as whether it rained somewhere in Canada on a given date, or whether aliens are real. Wayne wraps abstract bodies in backticks, so a predicate can stay half-informal while a requirement is still being pinned down.

The motivating example is a real requirement he once saw: "The computer must have enough RAM and a fast CPU or a good graphics card." Writing it as RAM(c) && CPU(c) || GPU(c) shows that the English has two readings:

# way 1
CanRunProgram(c) = RAM(c) && (CPU(c) || GPU(c))

# way 2
CanRunProgram(c) = (RAM(c) && CPU(c)) || GPU(c)

A truth table over all eight inputs shows they disagree in two rows, the ones where the machine has a good GPU and not enough RAM. Both readings are ordinary English. The vendor may have meant the first, a buyer reads the second, the program dies for lack of RAM, and the buyer concludes the vendor lied. differential-spec-analysis goes after the same kind of unstated decision at the scale of a whole system, by diffing several implementations built from one spec.

Implication

P => Q is defined as !P || Q: look at Q only when P holds. Wayne arrives at it from a requirement rather than a table. A program with native and web versions needs a capable machine only for the native one, which is !Native(p) || Beefy(c), and that shape is common enough that mathematics gives it an operator. => binds more loosely than && and ||, so A && B => C is (A && B) => C.

Implication also expresses that one statement is stronger than another. Code that crashes on 0 definitely has a bug, while code with a bug need not crash on anything, since an off-by-one error is still a bug:

CrashesOnInput(code, 0) => HasBug(code)

And it is transitive: from CanRenderVideo(c) => CPU(c) && RAM(c) you get CanRenderVideo(c) => CanRunProgram(c) without looking at what the predicates mean.

Sets and quantifiers

Predicates are untyped, so CanRunProgram(poodle) is a legal question, and gluing a good GPU to the poodle makes it return true. Sets fix that: c in Computer, abbreviated to CanRunProgram(c: Computer). Subsets correspond to subtypes. The chapter notes that mathematicians build pairs and then lists out of sets as a foundation, and that programmers can skip that step and use the richer structures directly.

Quantifiers arrive with a merge rule. "A pull request must be reviewed before it can be merged" becomes some d in Developer: ReviewedBy(pr, d). The stricter policy, that everyone who reviews must approve, holds the chapter's best trap. The obvious encoding

EveryoneApproves(pr: PullRequest) =
  all d in Developer: Approved(pr, d)

demands approval from every developer in the company, including those out sick or on parental leave. The fix restricts all to reviewers with implication, all d in Developer: ReviewedBy(pr, d) => Approved(pr, d), and Wayne notes this is the usual way to quantify over a subset. The fix opens a second trap, which an exercise asks the reader to find. If nobody reviewed the pull request, "everyone who reviewed it approved" is true, so SomeoneReviewed still has to be checked on its own. In general all x in {}: P(x) is always true and some x in {}: P(x) always false.

Quantifier order matters as well. "For every PR there is a developer who approved it" and "there is a developer who reviewed every PR" use the same two quantifiers in opposite orders and mean different things. In code, a quantifier is a loop that returns early, and most languages have one built in.

The ability-guarantee tradeoff

With both quantifiers defined, Wayne observes that some is more likely to hold over a large set and all over a small one, so a subset guarantees properties its superset can't. ASCII guarantees one byte per character where Unicode does not. Read-only access guarantees a file is not modified. Formulas built only from Booleans, AND, OR and NOT always have a truth table, which some x in Nat: OddPerfectNumber(x) does not. Yet emoji need Unicode, updates need write access, and interesting predicates need quantifiers. He calls this the ability-guarantee tradeoff and says it shows up in almost every chapter of the book. It has its own page, ability-guarantee-tradeoff.

Rewrite rules and proofs

Logic has simplifications the way arithmetic does, and the three the book says it will use most are De Morgan's laws (!(p && q) is !p || !q), the contrapositive (p => q is !q => !p) and quantifier duality (all x: !P(x) is !(some x: P(x))). Distribution over quantifiers works one way each: some distributes over || and all over &&. The counterexamples for the other pairings use the set of everyone who has ever lived. Someone is alive and someone is dead, but nobody is both. Everyone is alive or dead, but it is false that everyone is alive or that everyone is dead.

Every rewrite rule is a theorem, and a proof is a clear chain of steps from what is known to what is claimed. The contrapositive gets two proofs to make the point that a theorem can be proved more than one way: four rewrite steps through the definition of implication and double negation, or drawing both truth tables and seeing that they match. Wayne adds that even niche rewrite rules are useful for refactoring code.

What the chapter leaves out

The closing notes name the logic: this is first-order logic, where predicates can't be elements of sets or arguments to other predicates. Higher-order logics have more abilities and fewer guarantees. Logic with only Booleans, AND, OR and NOT is propositional logic. For more depth he recommends, in increasing difficulty, Robert S. Wolf's A Tour Through Mathematical Logic, Michael Huth and Mark Ryan's Logic in Computer Science, and Richard Epstein's Classical Mathematical Logic.

Wayne's interviews with engineers who moved into software from other fields are summarized at we-are-not-special.