Summary

This post is an adapted chapter from Hillel Wayne's book 'Logic for Programmers,' offering a ground-up introduction to predicate logic using programming-familiar examples. Wayne defines predicates as abstract Boolean functions that can express things beyond computation, then builds up the implication operator, sets, and quantifiers (some/all) through concrete scenarios like system requirements and pull request workflows. A central thread is that formalizing requirements in logic exposes ambiguities invisible in natural language. The chapter culminates in rewrite rules and a unifying principle: the ability-guarantee tradeoff, where more expressive systems offer greater power but fewer provable properties. The notation throughout is deliberately keyboard-typeable, prioritizing accessibility over mathematical convention.

Key Insight

Predicate logic gives programmers a precise, unambiguous tool for specifying system requirements, and the central tension across all logical systems is the ability-guarantee tradeoff: expressive power always comes at the cost of provable properties.

Spicy Quotes (click to share)

• 3

  Predicates act as a bridge between how we talk about systems in a human language and how we encode them in a programming language.

• 4

  This means predicates can be more abstract than programming functions, expressing things that we can't even compute, or at least don't yet know how to.

• 2

  Just like we have an arithmetic of numbers and an arithmetic of Booleans, we also have an arithmetic of sets.

• 6

  The more things a language or format or tool is able to do, the fewer things it guarantees us.

• 2

  Every rewrite rule I listed is a theorem, and we can prove they always work.

• 2

  In logic, too, we can come up with new constructs and ways of writing formulae, as long as 1) it's consistent and 2) we explain the notation clearly.

• 3

  The difficulty, of course, is in the application. It's one thing to know division but quite another to realize that 'scale a recipe with 5 eggs to use only 3 eggs' is a division problem.

• 4

  That's all the basics of formal logic. Really not that much, considering.

Tone

pedagogical, accessible, witty — combines mathematical rigor with programmer-first intuition and self-aware humor about the book's own limitations