A Crash Course in Predicate Logic

I started writing Logic for Programmers because there weren’t any good resources on logic for, uh, programmers. Now that the book’s out, the new problem is that there aren’t any good free resources on logic for programmers.

So, to solve that problem (and maybe hype the book a little), I converted the second chapter of LfP into a blog post. All footnotes are editorial comments not present in the book. Enjoy!

Chapter 2: A Crash Course in Logic

Formal logic is a very powerful tool, but it’s also very simple. Over this chapter, we’ll motivate and explain the basic concepts and syntax. This includes predicates, the implication operator, sets, and set quantifiers. Much of it may already be familiar to you from programming experience!

Predicates

To a first approximation, a predicate is a function that returns a Boolean. You’ve probably written dozens of predicates as a programmer. These are all predicates:

• Positive(x) is true if x is greater than 0.
• IsSum(x, y, z) is true if x plus y equals z.
• RAMAtLeast(c, r) is true if the computer c has at least r bytes of physical RAM.

I say “to a first approximation” because predicates are a mathematical concept, not a programming construct. A program function needs to come with a way of computing the answer, while a predicate simply defines what the answer is. Take RAMAtLeast: the software implementation would depend on the programming language, operating system, and possibly even the physical hardware. But the predicate? True if the computer has the RAM, false if not. That’s it.

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. These are all valid predicates, too:

• CanRunProgram(c) is true if the computer c is capable of running our program, whatever “capable” ends up meaning.
• RainyDayInCa(date) is true if on date, it rained somewhere in Canada.
• NotAlone() is true if aliens are real.

On the other hand, Positive(x) is easy to compute: just check if x > 0. The power of predicates is that they can span the full range of abstraction. So let’s introduce some syntax to distinguish between abstract predicates and concrete predicates. If a predicate is abstract, I’ll wrap the body in `backticks`:

# concrete
Positive(x) = x > 0
IsSum(x, y, z) = x + y == z

# abstract
CanRunProgram(c) = `c can run our program`

This isn’t a common mathematician convention, but it’s clear enough for our purposes. To distinguish predicates from “ordinary” functions like add_two, predicates will always be TitleCase and functions will always be snake_case.

Find some predicates in a program you wrote. Are these abstract predicates or concrete predicates?[^exercises]

Solution

Predicates tend to be functions that don’t change program or world state and return a Boolean. One I recently wrote was document_has_exactly_one_foo. Whatever predicates you find should all be concrete, as it’s impossible to actually code up an “abstract” predicate. You may see an abstract predicate or two in a design document, though.

Since predicates return Booleans, now’s a good time to get some Boolean operations out of the way. Different programming languages have different symbols for AND, inclusive OR, and NOT. Mathematicians use ∧, ∨, and ¬. I’m not going to use these because they’re not found on the keyboard. Instead, I’ll use &&, ||, and ! as our symbols. So X && !Y means “X is true and Y is false”.

On top of the three usual Boolean operators, mathematicians recognize a fourth, =>. But before we get into what that means, let’s try practicing what we just learned.

A Practical Example

Predicates act as a bridge between how we talk about systems in a human language and how we encode them in a programming language. Let’s come back to CanRunProgram. I once saw a program with these requirements:

The computer must have enough RAM and a fast CPU or a good graphics card (GPU).

I find this confusing. The sentence sounds natural enough in English, but we can find a problem by formalizing with logic. We’ll start by first writing predicates for each subrequirement, like so:

RAM(c) = `c has enough RAM`
CPU(c) = `c has a fast CPU`
GPU(c) = `c has a good GPU`

These predicates are abstract because we don’t know the specifics of what these mean. Is 64gb “enough RAM”? Is 32gb? The specifics don’t matter for us, because this is already enough to write CanRunProgram as a concrete mathematical expression.

CanRunProgram(c) = RAM(c) && CPU(c) || GPU(c)

Now the problem is clearer: is a && b || c supposed to be read as (a && b) || c or as a && (b || c)? The predicate is malformed and we have two different ways of making it make sense:

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

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

Both interpretations make sense in English! But they have different outputs for some inputs. We can see this by listing every single possible combination of values for RAM/CPU/GPU, and see what they give for CanRunProgram. This is called a truth table.

There are two combinations of inputs where one interpretation gives “false” and the other gives “true”. It’s possible that the vendor meant the first interpretation when writing the requirements, but I read it as the second interpretation. I’m sure that the program will run on my computer, it fails from insufficient RAM, and I think the vendor lied to me. Much better to express the requirement mathematically!

Expressing properties with formal logic is less ambiguous than with informal English. For the purpose of teaching, we’ll assume the intended predicate is (RAM(c) && CPU(c)) || GPU(c).

We will use truth tables for case analysis in the chapter Decision Tables.

If you ever have trouble generating a truth table, you can try to use a truth table generator. I provided a simple one here. Try p || !q and experiment from there.

Make a truth table for !P && !Q and !(P || Q).

Solution

These are the same. This is called De Morgan’s law.

Conditional Predicates

Let’s now make a variation on our predicate. For our CanRunProgram example: Some programs have a native version and a web version. The native version uses the local computer’s resources, while the web version does most of the processing on some cloud computer somewhere. So the native version requires a beefy computer, but any computer can run the web client.

If a computer is running the native version, it must have enough RAM and a fast CPU or a good graphics card (GPU) to use this program. But if it’s not running the native version, you’re fine.

To model this, we’ll need a new predicate, Native(p). Native is a property of the program, not the computer, so CanRunProgram then depends on both:

CanRunProgram(c, p) = `true unless Native(p),
  in which case (RAM(c) && CPU(c)) || GPU(c)`

I used backticks here because half the predicate is still in informal English. It turns out that we already have the tools we need to make it concrete. Whenever Native(p) is false, CanRunProgram(c, p) should be automatically true: we don’t need to even look at the computer specs.

CanRunProgram(c, p) =
  !Native(p) || ((RAM(c) && CPU(c)) || GPU(c))

How does this work? It’s easier to see if we pull out the right hand side into a new predicate, like Beefy(c), so we have !Native(p) || Beefy(c). Here’s the truth table for that expression (using N(p) for Native(p) and B(c) for Beefy(c)):

When Native(p) is false, !Native(p) || Beefy(c) is true, regardless of the value of Beefy(c). When Native(p) is true, then the expression is equal to the value of Beefy(c). So we’re only checking the computer specs if we’re running the native version, and ignoring it otherwise.

This trick of writing !P || Q to mean “check Q only if P is true” is incredibly common in math. So common that mathematicians use a special operator for it: =>, or the implication operator. P => Q (“P implies Q”) is the same as writing !P || Q. Expressed this way, our predicate is:

CanRunProgram(c, p) =
  Native(p) => (RAM(c) && CPU(c)) || GPU(c)

=> binds less tightly than && and ||: A && B => C is (A && B) => C, not A && (B => C).

The implication operator is incredibly powerful and comes in handy in lots of different places, like writing specifications or making system models. Among other things, we can use it to say that one Boolean statement is “stronger” than another. For example, “this code crashes when passed a 0” is a stronger statement than “this code contains a bug”. If it crashes on some input, it definitely contains a bug! But even if the program doesn’t crash, it can have a bug like an off-by-one error. Or, written mathematically:

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

Implication is also useful because it’s transitive. If P => Q and Q => R, then we know P => R, regardless of what P, Q and R actually are. If CanRenderVideo(c) => CPU(c) && RAM(c), then CanRenderVideo(c) => CanRunProgram(c).

Say we add two more conditions, so that CanRunProgram is instead

CanRunProgram(c, p) =
  `true unless Native(p) and either Q(p) or R(p),
  in which case (RAM(c) && CPU(c)) || GPU(c))`

Write this using =>. Then write this without using =>. Which is easier to read?

Solution

1. Native(p) && (Q(p) || R(p)) => (RAM(c) && CPU(c)) || GPU(c)
2. !(Native(p) && (Q(p) || R(p))) || ((RAM(c) && CPU(c)) || GPU(c))

I personally find (1) easier to read, since we don’t have as many nested expressions.

RAM(c) means that “computer c has sufficient RAM”. Modify it to mean “computer c has enough RAM to run program p”. Make similar changes for our other predicates and write CanRunProgram.

Solution

CanRunProgram(c, p) =
  Native(p) => (RAM(c, p) && CPU(c, p)) || GPU(c, p)

1. Using =>, write the expression “if Native(p) is true then Web(p) is false, and if Web(p) is true then Native(p) is false”.
2. Using &&, write the expression “Native(p) and Web(p) are not both true”.
3. Using ||, write the expression “Native(p) is false or Web(p) is false”.

Solution

1. (Native(p) => !Web(p)) && (Web(p) => !Native(p))
2. !(Web(p) && Native(p))
3. !Native(p) || !Web(p)

Take the predicate:

IfElse(c, x, y) =
  (c => x) && (!c => y)

Assume c, x, and y are all booleans.

1. When is IfElse true? When it is false?
2. What common code construct does this look like?

Solution

1. (c => x) && (!c => y) is equivalent to (!c || x) && (c || y). If you work through the cases, you should find that IfElse is true when c is true and x is true, or when c is false and y is true.
2. As hinted by the name, IfElse is simulating a conditional.

Sets

Predicates have untyped inputs by default. In CanRunProgram(c), c can be a computer, but c can also be a robot, or the number 26, or the string “the number 26”. In programming, we’d want to give it a type to make it clear that we should only pass in computers. Something like:

CanRunProgram(c) = `c is a computer`
    && ((RAM(c) && CPU(c)) || GPU(c))

Now, even if we glue a good GPU to a poodle, CanRunProgram(poodle) will still be false. To make the concept “c is a computer” mathematically representable, mathematicians use sets. A set is an unordered collection of unique values, like “all computers”, “all webpages under 500 kilobytes”, or “all strings that are valid Java programs”. Conventionally, we write the elements of a set like this:

Computer = {my_laptop, your_laptop, your_other_laptop, ... }

Then “c is a computer” is equivalent to saying “c is an element of the set Computer”. We’ll write this as c in Computer.

CanRunProgram(c) = c in Computer && ((RAM(c) && CPU(c)) || GPU(c))

To make our predicate definitions more concise, I’ll borrow a common programming syntax and write CanRunProgram(c: Computer) to mean “c must be an element of Computer”, like this:

CanRunProgram(c: Computer) = (RAM(c) && CPU(c)) || GPU(c)

This will make writing predicates with several constrained parameters easier.

Mathematicians treat sets as a mathematical bedrock they can use to build out more complex concepts. For example, they might define pairs in terms of sets by writing (a, b) as {a, {b}}, and then define the list [a, b, c] to be the set of pairs {(0, a), (1, b), (2, c)}. Then, having a set-based implementation of the list “abstraction”, they can throw away the sets and just work directly with lists.

As programmers, we don’t need to write formal definitions of lists before we use them and prefer to work with that more complex abstraction anyway. Even so, sets are still a useful programming data type. We’ll see this in the next chapter.

Set operations

Just like we have an arithmetic of numbers and an arithmetic of Booleans, we also have an arithmetic of sets. Given sets {A, B} and {B, C}, the basic things we can do are:

1. Union them together, or smush them into one big set: {A, B} | {B, C} == {A, B, C}
2. Intersect them, or find the common elements: {A, B} & {B, C} == {B}
3. Take the set difference, or subtract one set from the other: {A, B} - {B, C} == {A}

We can also test if one set is a subset of another. EvenIntegers is a subset of Integers because every element of EvenIntegers is also an element of Integers. The value 2 is not a subset of Integers, but the set {2} is. Subsets are similar to how programming languages have subtypes. If a language says that “Rectangle is a subtype of Shape”, it means that the set of all rectangles is a subset of the set of all shapes. We’ll look at subtyping in more detail as part of the broader topic of contracts.

1. Use the sets ram, cpu, and gpu to construct the set can_run_program, the set of all computers that pass CanRunProgram(c).
2. Given the sets Child and Adult, express the statements “nobody is both a child and an adult” by saying the sets do not overlap. You can use {} to mean the empty set.
3. The symmetric difference of two sets is the set of all elements in exactly one of the two sets. For example, the symmetric difference of {A, B} and {B, C} is {A, C}. Using just the basic set operations, find the symmetric difference of arbitrary sets S and T.

Solution

1. can_run_program = (ram & cpu) | gpu
2. Child & Adult == {}. Another way would be Child - Adult == Child && Adult - Child == Adult.
3. One way is (S - T) | (T - S); another is (S | T) - (S & T).

It’s also quite useful to map and filter sets. The standard math notation is {f(x) | P(x)}, but I find that beginners get confused about which side is map and which is filter. So for this book, I’ll use a more explicit syntax:

For example, the set of all even numbers is {x in Int: x % 2 == 0} and the set of all square roots of even numbers is {sqrt(x) for x in Int: x % 2 == 0}. This is sometimes called a set comprehension or set builder notation. Later, set comprehensions will form the bedrock of how we understand database queries.

Let Images be a set of images, where each image is a record containing fields for name, height, width, and size in kilobytes. Write set comprehensions for:

1. The set of all image names.
2. The set of all images larger than 10 kb.
3. The set of all heights for images that are squares.

Solution

1. {img.name for img in Images}
2. {img in Images: img.size > 10}
3. {img.height for img in Images: img.height == img.width}

Quantifiers

Let’s move away from software requirements and switch to a different problem. Software development teams often require changes to the main code to be first proposed as part of a pull request, which must be reviewed by another team member. More concisely:

A pull request must be reviewed by a team member before it can be merged.

Let us assume that we have two sets, PullRequest and Developer, that we can use in our predicates. I can start with these abstract predicates to express the rule:

ReviewedBy(pr: PullRequest, d: Developer) =
  `d reviewed pull request pr`

CanMerge(pr: PullRequest) = `someone reviewed pr`

Both of these predicates are abstract, but it seems like we should be able to make CanMerge concrete by defining it in terms of ReviewedBy.

For this we need a quantifier, or a logical expression that acts on a whole set. There are two common quantifiers in predicate logic. The first, the one we’ll use here, is called some.

Some

some x in set: P(x) means that P(x) is true for at least one x in the set set.

CanMerge(pr: PullRequest) =
  some d in Developer: ReviewedBy(pr, d)

I would read this as “CanMerge is true for the Pull Request element pr if there’s at least one element d in the set of Developers where ReviewedBy(pr, d) is true”. Or, as just “there is some developer that reviewed the pull request”.

The value d is called a variable. The token some is quantifying over the set Developer or, alternatively, is scoped to that set. This makes our use of it a scoped quantifier. More rarely, an expression is true for any value we care to name. For example, the statement some x in set: (P(x) && Q) is the same as Q && some x in set: P(x), regardless of what set is. In this case, we can choose to leave out the sets and write:

(some x: (P(x) && Q)) == (Q && some x: P(x))

This use of some is not scoped to a set, so we call it an unscoped quantifier. Almost all quantifiers we use will be scoped.

So as to prevent eldritch math horrors, we can only quantify over sets and values, not predicates.[^function-sets] If you want to know more about eldritch math horrors, check out the appendix Beyond Logic.

All

As it stands, CanMerge is too permissive. What happens if the reviewer found a major security flaw? What if five developers review the pull request and two find flaws? Most companies use a stricter merge requirement:

A pull request must be reviewed by at least one team member, and all reviewers must approve the request, before it can be merged.

As is our habit, we start by writing the requirements as abstract predicates.

ApprovedBy(pr: PullRequest, d: Developer) = `d approved pr`

SomeoneReviewed(pr: PullRequest) =
  some d in Developer: ReviewedBy(pr, d)
EveryoneApproves(pr: PullRequest) =
  `everyone who reviewed pr also approved it`

CanMerge(pr: PullRequest) =
  SomeoneReviewed(pr) && EveryoneApproves(pr)

This gives us an opportunity to introduce the other quantifier: all. all x in set: P(x) says that P(x) is true for every x in our set. With this, it seems like our new predicate can be written like this:

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

But this is wrong: it requires every single developer to approve the pull request, including developers out sick or on parental leave. We only want to require that every developer who reviewed the pull request approved it. We can fix this with implication. Recall that P => Q means !P || Q. Then ReviewedBy(pr, d) => Approved(pr, d) means that either d approved the pull request or did not review it at all.

EverybodyApproves(pr: PullRequest) =
  all d in Developer: ReviewedBy(pr, d) => Approved(pr, d)

We often use => to only an all on a subset of elements.

Most programming languages have built-in quantifier functions, as we’ll discuss in a later chapter. If your language of choice does not, you can usually approximate quantifiers with a loop. For example, you can write SomeoneReviewed like this pseudocode:

fun SomeoneReviewed(pr: PR) {
  for (d in developers) {
    if(ReviewedBy(pr, d)) return true;
  }
  return false;
}

Why do we need SomeoneReviewed at all? Isn’t it true that if everybody who reviewed the PR approved it, then someone must have reviewed it? Find the edge case where EveryoneApproved is true and SomeoneReviewed is false.

Solution

If not a single developer has reviewed the PR, then EveryoneApproved is true (all zero reviewers approved!) while SomeoneReviewed is false (nobody reviewed it).

As a rule, all x in {}: P(x) is always true (regardless of what P is) and some x in {}: P(x) is always false.

Define Nat as the set of natural numbers: 0, 1, 2, etc.

1. Write the logical statement “every natural number is smaller than itself plus 1”.
2. Write the logical statement “0 is less than or equal to every natural number”.

Solution

1. all x in Nat: x < x + 1
2. all x in Nat: 0 <= x

1. Write the logical statement “for every PR, there is a developer that approved it”.
2. Write the logical statement “there is a developer that has reviewed every single pull request”.

In both cases you’ll need to put one quantifier inside a different quantifier.

Solution

1. all pr in PR: some d in Developer: ApprovedBy(pr, d)
2. some d in Developer: all pr in PR: ReviewedBy(pr, d)

The ability-guarantee tradeoff

Now that we’ve seen both all and some I want to point out something important: some x in set: P(x) is more likely to be true for large sets, and all x in set: P(x) is more likely to be true for small sets. If we have two distinct sets and set1 is a subset of set2, we should expect to find some predicate P(x) where all x in set1: P(x) and some x in set2: !P(x). We can say that set1 guarantees P(x). Let’s look at three examples:

1. The set “all ASCII characters” is a subset of the set “all Unicode characters”. ASCII guarantees/assures that every representable character fits in exactly one byte, so I can look at the string ABC and immediately know it’s three bytes. Unicode doesn’t guarantee this, and the string ABC could be six bytes if I use Cyrillic characters.
2. The set “things we can do with read-only access to a file” is a subset of “things we can do with full access to a file”. Read-only access guarantees that a program won’t change the contents of a file. Whereas with full access, any buggy program could overwrite our data.
3. The set “all logical formulae that only use booleans, AND, OR, and NOT” is a subset of “all logical formulae”. The former guarantees that every formula can be turned into a truth table. How do you make a truth table for some x in Nat: OddPerfectNumber(x)? You can’t. Mathematicians still don’t know if it’s true or not!

At the same time, we need Unicode to represent emoji, write access to update our data, and set quantifiers to express most interesting predicates. This is the ability-guarantee tradeoff: the more things a language or format or tool is able to do, the fewer things it guarantees us.

We will see this tradeoff in almost every chapter of this book.

Rewrite Rules

In the beginning of the book, I said that logic is the mathematics of Booleans just as arithmetic is the mathematics of numbers. Knowing arithmetic lets us simplify numerical expressions. For example, here’s how we can simplify the function f(x, y) = -10x + 2(y + 5x):

1. 2(y + 5x) is the same as 2y + 10x.
2. -10x + 2y + 10x is the same as 10x - 10x + 2y.
3. The first two terms are opposites, so they cancel out.
4. So we have just f(x, y) = 2y.

In logic, these simplifications are called rewrite rules. You may have already used one rewrite rule as a kid:

Are you sorry? No? Well are you not not not not sorry?

The rewrite rule here is !!a == a. This means !!(!!Sorry) is the same as Sorry.

Some common rewrite rules we use in logic are:

The implication operator also has rewrite rules. One of them, contrapositive, will be very useful to us.

And there are rewrite rules for quantifiers, too:

Constant extraction works for any quantifier with || or &&. Distribution only works for some/|| and all/&&.

Some rules come up more often than others. We’ll be using De Morgan’s law, contrapositive, and quantifier duality a whole lot going forward. A larger list is in Rewrite Rules. Even niche rules can be quite useful for refactoring code.

Use rewrite rules to simplify !(some x: !P(x)).

Solution

all x: P(x)

Give a real-world example of each distribution rule.

Solution

Here are two I came up with:

1. “All days this week are warm and sunny” is the same as “all days [this week] are warm and all days are sunny”.
2. “Someone has blue eyes or green eyes” is the same as “someone has blue eyes or someone has green eyes”.

some only distributes over || and all only distributes over &&. Find predicates where:

1. (some x: P(x)) && (some x: Q(x)) != some x: P(x) && Q(x)
2. all x: P(x) || Q(x) != (all x: P(x)) || (all x: Q(x))

HINT: In both cases, make the left side true and the right side false.

Solution

There are many answers, here are just two (assuming Person is the set of all people who have ever lived):

1. (some p in Person: Alive(p)) && (some p in Person: Dead(p)) is true, some p in Person: (Alive(p) && Dead(p)) is false.
2. all p in Person: Alive(p) || Dead(p) is true, all p in Person: Alive(p) || all p in Person: Dead(p) is false.

Theorems

You may have heard that mathematicians try to prove theorems. A theorem is just a mathematical statement that is always true, and a proof is just a clear set of steps that gets you from what you already know is true to showing that the theorem is true.

Every rewrite rule I listed is a theorem, and we can prove they always work. Take contrapositive, for example. To show that we can always rewrite !Q => !P into P => Q, we:

1. Start with !Q => !P.
2. Apply the definition of implication to get !!Q || !P.
3. Remove the double negative to get Q || !P.
4. Apply the definition of implication again to get P => Q.

Tada, we just wrote a proof! Try going the other way, starting from P => Q.

Start from P => Q and rewrite it into !Q => !P.

Solution

First rewrite it as !P || Q. Then replace Q with !(!Q) to get !(!Q) || !P. Then rewrite that as !Q => !P.

Most theorems can be proved in more than one way. Here’s a totally different proof of the contrapositive rewrite rule:

1. Draw the truth tables for P => Q and !Q => !P.
2. They are the same.

Theorems are the foundation of mathematics. A theorem is what tells us if a logical tool (like the contrapositive or De Morgan’s law) actually works or not. We can use the machinery of logic without knowing the theorems that support them, just as we know 117*92 == 92*117 without having to write a proof first. That said, we can also prove theorems about code, a specialty topic we’ll cover in its own chapter.

Notation

Mathematicians like to say that logic is a “language”. The point of language is to communicate complex ideas clearly, and sometimes the best way to do that is to come up with new words and grammar.

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. In fact, this is encouraged. For example, the normal way of writing “the set of integers between 1 and 10” takes up a lot of space:

{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}

If I want to be more concise, I can come up with a shorthand:

{1, 2, 3, ... 100}

If I want to be even more concise than that, I can define new syntax:

1..=100 = {1, 2, 3, ... 100}
1..<100 = {1, 2, 3, ... 99}

This isn’t completely unambiguous: what is 10..=9? I’ll define it as the empty set: if a > b, then a..=b is empty. Similarly, a..<b is empty whenever a >= b.

Rewrite that rule (that if a > b, then a..=b is empty) using the all quantifier. Assume both a and b are in the set of integers.

Solution

all a, b in Int: a > b => (a..=b == {})

Write 1..=100 using set filter notation. Filter on the set Int.

Solution

{x in Int: 1 <= x && x <= 100}

Write IsDivisibleBy(num, divisor), which is true if num is evenly divisible by divisor. Use some and ..=.

Solution

IsDivisibleBy(num, divisor) =
  some x in 1..=num:
    x*divisor == num

Another notation I find very useful is conjunction lists. Complicated systems often have complicated requirements:

Rules = A && B && (C || D) && (E || (F && G))

That’s hard to read! To make it easier, let’s instead write it like this:

Rules =
  1. A
  2. B

  3. || C
     || D

  4. || E
     || a. F
        b. G

Numbers like 4. and letters like a. will always mean AND. If I want a list of ORs, I’ll always use ||.

Summary

• A predicate is a Boolean function which can be defined over any input.
• A set is an unordered collection of unique elements. Sets can contain any type of value, except predicates.
• A quantified expression is an expression checked for every (or any) element of a set.
• Math notation is flexible. We can come up with new notation, operators, and grammar, as long as we’re clear and consistent.
• Logical formulae can be rewritten and simplified.

Here are all the symbols and syntax we learned:

• Predicates are always TitleCase(x). Functions are always lowercase and snake_case(x).
• AND, OR, NOT: &&, ||, !
• Implies: =>
• Set union, intersection, difference: |, &, -
• Set map and filter: {x^2 for x in set: x > 2}
• Quantifiers: all x and some x
• Various syntactic sugar.

And that’s it! That’s all the basics of formal logic. Really not that much, considering.

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. The rest of the book is about software situations where logic is useful, and how to make it useful. Let’s use logic to understand the world.

Learn More

By necessity this chapter is only a very broad overview of the basics of mathematical logic. More thorough and comprehensive treatments include (in increasing order of complexity) 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.

The logic we covered is called first-order logic because predicates cannot be values in sets or passed to other predicates. Higher order logics have more abilities and fewer guarantees; see appendix Beyond Logic for more information. Logic without predicates and quantifiers (only booleans, AND, OR, and NOT) is called propositional logic.

The formal names for some and all are the existential and universal quantifiers, respectively. Mathematicians use the symbols ∃ and ∀. There are a few syntactic variants on the quantified expression; see appendix Math Notation for more.

“Ability” in the ability-guarantee tradeoff is sometimes called “power”, as in the rule of least power (prefer the “least powerful” programming language that solves the task). I’ve also seen “guarantees” called “power”. As the “power-power tradeoff” is unclear, we’ll avoid the word “power” in this book.

Logic for Programmers is now available in ebook and tree book formats. Check out the official site to learn more!

1. Just to set expectations up-front: the book is based on first-order classical logical, because that’s all you need to drive a couple hundred pages of applications. There’s no constructive logic, no lambda calculus, no Curry-Howard, etc. The target audience is people who don’t know any math.
2. One really important design decision I had was “all math used in the book should be typeable on standard US keyboard”. Most “official” math symbols are meant to be handwritten, which makes them a lot harder to use on a computer!
3. The blog post uses OR instead of || in tables because || breaks markdown table formatting.
4. Not shown: the book is heavily indexed and interlinked; this and all the other “this will be useful for XYZ” comments have page numbers of other chapters.
5. I first explored this idea in the newsletter Some tests are stronger than others; chapter 4 of the book uses it to motivate property testing.
6. Yeah uh okay in reviewing this post I just realized I got this wrong, the actual mathematical convention of pairs is actually {{a}, {a, b}}. Sorry if this ruined the whole book for you. At least it’s now in the errata.
7. The book uses 0-based indexing for lists (unless discussing a language which does otherwise) and starts the natural numbers at 0. Different branches of math have different conventions and I just stuck to what most programmers are used to.
8. One thing the book does not cover is type theory. There’s a few reasons for this, mainly that I couldn’t find the right balance of simplicity, practicality, and actually-using-logic-ity. It does cover some basic things like Make Illegal States Unrepresentable and Liskov subtyping.
9. Extremely cursed fact I learned while making this figure: The SVG standard defines a “point” as 1 / 72 inches, while TeX defines a “point” as 1 / 72.27 inches. I wrote more about the history here.
10. Coming up with the dang name for this took forever. I used to call it the capability-tractability tradeoff but the book was pretentious enough as-is. Thanks to Chelsea Troy for finally coming up with something workable.
11. This is the best idea in the book. I love conjunction lists.