37 min read

> "For all x, there exists a bug, such that the test suite does not catch it."

Prerequisites

  • 1

Learning Objectives

  • Translate English statements that talk about objects and their properties into predicate logic, identifying the predicate and its domain.
  • Use the universal quantifier and the existential quantifier correctly, and read a quantified statement back into precise English.
  • Interpret and write nested (multiply-quantified) statements, and explain how reordering quantifiers changes their meaning.
  • Negate any quantified statement by mechanically pushing the negation inward, and produce a counterexample to disprove a universal claim.
  • Map quantifiers onto loops and onto Python's all() and any(), and use quantified statements to specify a function's preconditions and postconditions.

Chapter 2: Predicate Logic and Quantifiers

"For all x, there exists a bug, such that the test suite does not catch it." — the universally quantified anxiety of every programmer

Overview

In Chapter 1 you learned to reason about whole statements — "the cache is warm," "the user is an admin" — and to combine them with $\land$, $\lor$, $\neg$, $\rightarrow$, and $\leftrightarrow$. That toolkit is powerful, but it has a ceiling, and you hit the ceiling the moment you try to say something about every element of a collection or some element of one.

Consider three claims a programmer makes constantly:

  • "Every item in this list is non-negative."
  • "There is at least one user with admin rights."
  • "For every request, there is a server that handles it."

Propositional logic cannot express any of these. To propositional logic, "every item in this list is non-negative" is a single opaque letter $p$ — true or false, with no internal structure. You cannot reach inside it to talk about the individual items, and you certainly cannot relate it to "the third item is non-negative." Yet that internal structure is exactly what you reason about when you write a loop, an assertion, or a function contract. The gap between "a statement is true" and "a statement is true for every element" is the gap this chapter closes.

The fix is predicate logic: logic that can talk about objects, the properties those objects have, and — crucially — how many objects have a property. It is the language in which every loop invariant, every API contract, every database query, and every formal specification is ultimately written. Once you can read for all and there exists as precisely as you read if and and, you can state exactly what your code is supposed to do — and that precision is the difference between a test that passes and a program that is correct.

In this chapter you will learn to:

  • Break a statement into a predicate (the property) and the objects it talks about, and pin down the domain those objects come from.
  • Quantify a predicate with $\forall$ ("for all") and $\exists$ ("there exists"), and translate fluently between English and symbols in both directions.
  • Read and write nested quantifiers, and explain precisely why $\forall x\, \exists y$ and $\exists y\, \forall x$ usually say different things.
  • Negate any quantified statement by pushing $\neg$ through the quantifiers, and disprove a universal claim with a single counterexample.
  • See that $\forall$ is a loop with an early-exit on False, that $\exists$ is a loop with an early-exit on True, and that Python's all() and any() are these quantifiers in code.
  • Specify a function with preconditions and postconditions written as quantified statements — the bridge from "what the code does" to "what the code is supposed to do."

Learning Paths

🏃 Fast Track: If you already read quantified statements comfortably, skim 2.1–2.2, then spend your time on 2.3 (nested quantifiers — the part everyone gets wrong) and 2.6 (specifications). Do the ⭐⭐ and ⭐⭐⭐ exercises, especially the translation and negation problems.

📖 Standard Path: Read in order. Work every 🔄 Check Your Understanding before moving on. When a translation problem appears, write your answer down before reading ours — quantifier translation is a skill you build by doing, not by watching.

🔬 Deep Dive: After the chapter, restate the negation rules as a single recursive procedure ("to negate a formula, ..."), prove it correct on the structure of formulas, and connect it to the way a SAT/SMT solver or a property-based testing library (like Hypothesis) actually searches for counterexamples. The exercise set's Part E points the way.


2.1 From propositions to predicates

Start with a sentence that propositional logic cannot handle, and watch why it fails.

"$x > 5$."

Is this true or false? You cannot say — it depends on $x$. If $x = 7$ it is true; if $x = 2$ it is false; if $x$ is unspecified the sentence has no truth value at all. A proposition, by the definition from Chapter 1, must be definitely true or definitely false. So "$x > 5$" is not a proposition. It is something new: a statement with a hole in it, a statement that becomes a proposition only once you fill the hole with a specific value.

That "statement with a hole" is the central object of this chapter.

Definition (predicate). A predicate is a statement that contains one or more variables and becomes a proposition — definitely true or definitely false — once each variable is assigned a specific value from a fixed collection. We write a predicate as a function of its variable(s), for example $P(x)$, $Q(x, y)$, or $\text{Prime}(n)$. The result $P(x)$ is read "$P$ of $x$" or "$x$ satisfies $P$."

So if we name our example $P(x)$, meaning "$x > 5$," then:

  • $P(7)$ is the proposition "$7 > 5$," which is true.
  • $P(2)$ is the proposition "$2 > 5$," which is false.
  • $P(x)$ on its own is a predicate, with no truth value until $x$ is fixed.

A predicate is, quite literally, a boolean-valued function. You have written hundreds of them:

def is_positive(x):
    return x > 0

print(is_positive(7))   # the proposition "7 > 0", which is True
print(is_positive(-3))  # the proposition "-3 > 0", which is False
# Expected output:
# True
# False

is_positive is the predicate $P(x)$ = "$x > 0$" rendered in Python. Calling it with an argument "plugs the hole" and yields a definite True or False — a proposition. This correspondence is not a loose analogy; it is exact, and it is the reason predicate logic feels natural to programmers. A predicate is a function from objects to truth values.

💡 Intuition: A proposition is a value (True or False); a predicate is a function that returns a value once you give it an argument. Chapter 1 reasoned about the values. This chapter reasons about the functions — and, in the next sections, about what is true across all their possible arguments at once.

The domain: which objects are we talking about?

Notice that "$P(7)$ is true" and "$P(x)$ for an unspecified $x$" are not the only options. There is a third, more interesting question: for which values of $x$ is $P(x)$ true? — and to even ask it, you must say which values of $x$ are on the table in the first place. "$x > 5$" ranges over what: integers? real numbers? the elements of a particular list? The answer changes everything.

Definition (domain). The domain (or domain of discourse, or universe) of a predicate is the collection of values that its variables are allowed to take. Every quantified statement is made relative to a domain; the same predicate can be true over one domain and false over another.

The domain is not optional decoration — it is part of the statement's meaning. Consider the predicate $Q(x)$ = "$x^2 = 2$":

  • Over the domain of real numbers $\mathbb{R}$, there is a value satisfying $Q$ (namely $x = \sqrt{2}$).
  • Over the domain of rational numbers $\mathbb{Q}$, there is no such value (a fact you'll prove by contradiction in Chapter 5).
  • Over the domain of integers $\mathbb{Z}$, again no such value.

Same predicate, three different domains, two different answers to "does anything satisfy it?" In code, the domain is usually explicit and finite — it's the list you're looping over, the set of users in the database, the keys of a dictionary. When a programmer says "every item in the list is non-negative," the list is the domain. We will lean on that fact heavily in 2.5.

Predicates of several variables

A predicate can have more than one hole. $\text{Greater}(x, y)$ = "$x > y$" needs two values before it becomes a proposition: $\text{Greater}(7, 3)$ is true, $\text{Greater}(3, 7)$ is false. The number of variables is the predicate's arity — $P(x)$ is unary, $Q(x, y)$ is binary, and so on. Multi-place predicates are how we express relationships ("$x$ divides $y$", "$u$ follows $v$", "$a$ is the parent of $b$"), and they become the heart of the action in 2.3 when we quantify each variable separately.

Here is a worked translation to fix the vocabulary before we add quantifiers.

Worked example. Let the domain be all employees of a company. Define the predicates $M(x)$ = "$x$ is a manager," $E(x, y)$ = "$x$ earns more than $y$," and $D(x, y)$ = "$x$ and $y$ work in the same department." Translate into a single combined statement: "Alice is a manager who earns more than Bob, and they are in the same department."

Letting $a$ = Alice and $b$ = Bob (specific elements of the domain), this is

$$M(a) \land E(a, b) \land D(a, b).$$

Each piece is now a proposition (Alice and Bob are specific people), so the connectives from Chapter 1 combine them exactly as before. Predicate logic doesn't replace propositional logic — it extends it, adding the ability to name objects and properties beneath the connectives you already know.

🔄 Check Your Understanding 1. Is "$n$ is a prime number" a proposition or a predicate? What about "$17$ is a prime number"? 2. Let the domain be the integers and $R(x)$ = "$x^2 \ge 0$." For how many values of $x$ in the domain is $R(x)$ true? 3. Why is it impossible to assign a truth value to the predicate $E(x, y)$ = "$x > y$" without more information?

Answers

  1. "$n$ is a prime number" is a predicate (it has a variable $n$ with no value). "$17$ is a prime number" is a proposition (the hole is filled; it is definitely true). 2. All of them — every integer squared is non-negative, so $R(x)$ holds for every $x$ in the domain. (In 2.2 we'll write this as a single statement: $\forall x\, R(x)$.) 3. $E(x, y)$ has two unfilled holes; until both $x$ and $y$ are given specific values, there is nothing definite to be true or false about.

2.2 Universal and existential quantifiers

A predicate by itself has no truth value. But the interesting claims a programmer makes are not about one filled-in value — they are about how the predicate behaves across the whole domain. "Is every item non-negative?" "Is there any duplicate?" These two questions — every and some — are so central that logic gives each its own symbol. They are called quantifiers, because they say something about the quantity of domain elements that satisfy a predicate.

The universal quantifier: $\forall$

Definition (universal quantifier). For a predicate $P(x)$ over a domain $D$, the statement $\forall x\, P(x)$ — read "for all $x$, $P(x)$" — is the proposition that is true exactly when $P(x)$ is true for every element $x$ of $D$, and false otherwise. The symbol $\forall$ is the universal quantifier.

Unlike a bare predicate, $\forall x\, P(x)$ is a proposition: it is definitely true or definitely false (relative to the domain). The variable $x$ is no longer a hole you fill from outside — the quantifier "uses it up," ranging over the whole domain internally. We make this precise in a moment when we discuss bound and free variables.

A universal statement is, in effect, a giant conjunction. If the domain is the finite set $D = \{d_1, d_2, \dots, d_n\}$, then

$$\forall x\, P(x) \quad\text{means exactly}\quad P(d_1) \land P(d_2) \land \dots \land P(d_n).$$

It takes only one false conjunct to make the whole thing false — which is why a single bad element sinks a universal claim. Hold that thought; it is the basis of the counterexample (2.4) and of short-circuit evaluation (2.5).

Worked example. Domain: the integers $\mathbb{Z}$ (recall $\mathbb{N}$ includes 0, but here we use all of $\mathbb{Z}$). Let $P(x)$ = "$x^2 \ge 0$." Then $\forall x\, P(x)$ says "every integer has a non-negative square," which is true. Now let $Q(x)$ = "$x > 0$." Then $\forall x\, Q(x)$ says "every integer is positive," which is false — the integer $0$ (or any negative integer) violates it.

The existential quantifier: $\exists$

Definition (existential quantifier). For a predicate $P(x)$ over a domain $D$, the statement $\exists x\, P(x)$ — read "there exists $x$ such that $P(x)$" — is the proposition that is true exactly when $P(x)$ is true for at least one element $x$ of $D$, and false otherwise. The symbol $\exists$ is the existential quantifier.

Where $\forall$ is a giant and, $\exists$ is a giant or. Over a finite domain $D = \{d_1, \dots, d_n\}$,

$$\exists x\, P(x) \quad\text{means exactly}\quad P(d_1) \lor P(d_2) \lor \dots \lor P(d_n).$$

It takes only one true disjunct to make the whole thing true — so finding a single witness settles an existential claim, just as finding a single offender settles (refutes) a universal one.

💡 Intuition: $\forall$ is a demand on everyone — every element must comply, and the doubter wins by naming one rebel. $\exists$ is a search for one — the claimant wins by exhibiting a single example, and the doubter must rule out the entire domain. This asymmetry (one example refutes a "for all"; one example proves a "there exists") drives almost everything in the rest of the chapter.

A related, stronger claim is "there is exactly one." Logic writes this $\exists! x\, P(x)$ (read "there exists a unique $x$"). It means $P$ holds for one element and no others; you'll meet it formally when we prove uniqueness in Chapter 5, but it is worth recognizing the symbol now.

Worked example. Domain: positive integers. Let $C(x)$ = "$x$ is composite (not prime and greater than 1)." Then $\exists x\, C(x)$ is true — for instance $x = 4$ works ($4 = 2 \times 2$). A single witness, $4$, makes the existential statement true; we do not need to find them all.

Restricting the domain inside the quantifier

In practice we constantly want to quantify over part of a domain: "every positive integer ...," "some prime ...." There is a standard idiom for each quantifier, and getting the connective right is a classic stumbling block.

  • Universal with a restriction uses $\rightarrow$: "every positive integer is $\ge 1$" is $$\forall x\, \big( x > 0 \rightarrow x \ge 1 \big).$$ Read it as: for all $x$, if $x$ qualifies (is positive), then it has the property. When $x$ does not qualify, the implication is vacuously true (Chapter 1's $F \rightarrow \text{anything} = T$), so non-qualifying elements are harmlessly ignored.
  • Existential with a restriction uses $\land$: "some integer is both prime and even" is $$\exists x\, \big( \text{Prime}(x) \land \text{Even}(x) \big).$$ Read it as: there exists an $x$ that qualifies AND has the property. (Here $x = 2$ is the witness.)

⚠️ Common Pitfall: don't swap $\rightarrow$ and $\land$ between the quantifiers. Writing $\exists x\,(\text{Prime}(x) \rightarrow \text{Even}(x))$ does not say "some prime is even." An implication is true whenever its hypothesis is false, so that statement is satisfied by any witness that isn't prime at all (e.g. $x = 9$ makes $\text{Prime}(9)$ false, so the implication is true) — it's trivially true and says almost nothing. Symmetrically, $\forall x\,(x > 0 \land x \ge 1)$ does not say "every positive integer is $\ge 1$"; it claims every element of the domain is positive and $\ge 1$, which is false the moment the domain contains $0$ or a negative number. The rule: $\forall$ pairs with $\rightarrow$, $\exists$ pairs with $\land$.

🔄 Check Your Understanding 1. Over the domain $\{1, 2, 3, 4\}$, write $\forall x\, (x < 5)$ as an explicit conjunction, and say whether it's true. 2. Translate "some student passed the exam" using $S(x)$ = "$x$ is a student" and $P(x)$ = "$x$ passed," over a domain of all people. Which connective goes inside? 3. True or false, and why: over the domain of integers, $\exists x\, (x^2 = -1)$.

Answers

  1. $(1 < 5) \land (2 < 5) \land (3 < 5) \land (4 < 5)$, which is true (all four conjuncts hold).
  2. $\exists x\, (S(x) \land P(x))$ — existential restriction uses and ("there is someone who is a student and passed"). 3. False: no integer has square $-1$ (squares of integers are $\ge 0$), so the domain contains no witness.

2.3 Nested quantifiers and the order that matters

Here is where predicate logic earns its keep — and where careful reading separates a correct specification from a subtly wrong one. Real statements quantify more than one variable, and when you do, the order of the quantifiers can change the meaning entirely.

Begin with the predicate everyone has an intuition for. Let the domain be people, and let $L(x, y)$ = "$x$ loves $y$." Consider two statements that look almost identical:

$$\forall x\, \exists y\, L(x, y) \qquad\text{versus}\qquad \exists y\, \forall x\, L(x, y).$$

Read them slowly, left to right, in the order the quantifiers appear:

  • $\forall x\, \exists y\, L(x, y)$: "for every person $x$, there exists a person $y$ such that $x$ loves $y$." In plain English: everybody loves somebody — but each person may love a different somebody. The choice of $y$ is allowed to depend on $x$.
  • $\exists y\, \forall x\, L(x, y)$: "there exists a person $y$ such that, for every person $x$, $x$ loves $y$." In plain English: somebody is loved by everybody — there is one specific person $y$ whom every $x$ loves. The same $y$ must work for all $x$.

These are wildly different claims. The second is far stronger: it asserts a single universal sweetheart; the first merely asserts nobody is entirely loveless. The second implies the first (if one person is loved by all, then certainly everyone loves someone), but the first does not imply the second.

💡 Intuition: read quantifiers as a game with a move order. $\forall x\, \exists y\, P(x,y)$ is a game where an adversary picks $x$ first, then you must produce a $y$ that works — so your $y$ can react to their $x$. $\exists y\, \forall x\, P(x,y)$ reverses the order: you must commit to a single $y$ first, and only then does the adversary pick the $x$ that must satisfy $P(x,y)$ — your $y$ has to handle every challenge they could throw. Committing first is harder. An inner existential may depend on an outer universal; an outer existential must be chosen once and for all.

A concrete, checkable example

Abstract people-loving examples are vivid but unfalsifiable. Let's use arithmetic, where you can verify the truth values yourself. Domain: the integers $\mathbb{Z}$. Predicate: $S(x, y)$ = "$x + y = 0$."

  • $\forall x\, \exists y\, S(x, y)$: "for every integer $x$, there is an integer $y$ with $x + y = 0$." True — given any $x$, choose $y = -x$, and indeed $x + (-x) = 0$. The witness $y$ depends on $x$, which is allowed because $\exists y$ is inside $\forall x$.
  • $\exists y\, \forall x\, S(x, y)$: "there is a single integer $y$ such that, for every integer $x$, $x + y = 0$." False — no fixed $y$ can satisfy $x + y = 0$ for all $x$ at once. If $y$ worked for $x = 1$ (so $y = -1$), it fails for $x = 2$ (since $2 + (-1) = 1 \ne 0$). One $y$ cannot cancel every $x$.

Same predicate, same domain — swapping the quantifier order flips the statement from true to false. This is the lesson: with mixed quantifiers, order is meaning.

When order does not matter

Two quantifiers of the same kind commute freely. $\forall x\, \forall y\, P(x, y)$ and $\forall y\, \forall x\, P(x, y)$ say the same thing ("$P$ holds for every pair"), and likewise $\exists x\, \exists y\, P(x, y)$ equals $\exists y\, \exists x\, P(x, y)$ ("some pair satisfies $P$"). It is only when a $\forall$ and an $\exists$ are adjacent and in mixed order that swapping them can change the meaning. So the rule worth memorizing is narrow and precise: you may reorder like quantifiers; you may not, in general, swap a $\forall$ past an $\exists$.

A worked translation with three quantifiers

Statements with three quantifiers appear in real specifications (the definition of a limit in calculus is the famous example: $\forall \varepsilon\, \exists \delta\, \forall x\, \dots$). Let's translate one.

Claim to translate. Domain: the integers. "Between any two distinct integers there is no third integer strictly between them is false; but for any integer there is always a larger one." Take the second part: every integer has a strictly larger integer.

$$\forall x\, \exists y\, (y > x).$$

This is true over $\mathbb{Z}$: given $x$, the witness $y = x + 1$ satisfies $y > x$. Note again the nesting — $y$ depends on $x$ — and note that the reversed form $\exists y\, \forall x\,(y > x)$ ("there is a single integer larger than every integer") is false, since the integers have no maximum.

Here is the same idea checked in code over a finite slice of the domain — and the finite case carries a warning worth absorbing. Watch what happens when the domain has a largest element:

domain = range(-5, 6)        # a finite slice WITH a maximum: -5, -4, ..., 5
# Forall x, Exists y in domain: y > x
forall_exists = all(any(y > x for y in domain) for x in domain)
# Exists y, Forall x in domain: y > x
exists_forall = any(all(y > x for x in domain) for y in domain)
print(forall_exists, exists_forall)
# Expected output:
# False False

Over the infinite integers, $\forall x\,\exists y\,(y>x)$ was true. Over this finite slice it is false — and that is the whole point. The slice has a largest element, $5$, and for $x = 5$ there is no $y$ in the slice with $y > 5$, so the inner any(...) fails and forall_exists is False. The reversed statement is also False: no element of the slice exceeds every element, since even the largest, $y = 5$, fails at $x = 5$ (because $5 > 5$ is false). Let's verify by hand-building the table, reasoning each cell directly from the definitions:

Statement Meaning over $D = \{-5,\dots,5\}$ Value Why
$\forall x\, \exists y\,(y>x)$ every element has a larger element in $D$ False $x=5$ has no larger element in $D$
$\exists y\, \forall x\,(y>x)$ some element exceeds every element of $D$ False even $y=5$ fails at $x=5$ ($5>5$ is false)

The moral is not about this particular slice — it is that the truth of a quantified statement depends on its domain, boundary and all. A statement true over $\mathbb{Z}$ (which has no maximum) can turn false over a finite range (which has one). This is exactly why we hand-derive these tables from the definitions instead of trusting a glance.

⚠️ Common Pitfall: When you test a quantified claim in code, you are testing it only over the finite domain you actually looped over. "No counterexample in range(-5, 6)" is not "true over all integers" — the untested elements (here, every integer past $5$) could break it. This is theme four again: code evaluates a slice; only a proof settles the whole, possibly infinite, domain. (The runnable version lives in code/example-02-nested.py.)

🔄 Check Your Understanding 1. In English, what is the difference between "everyone has a best friend" ($\forall x\, \exists y$) and "someone is everyone's best friend" ($\exists y\, \forall x$)? 2. Over the positive integers, is $\forall x\, \exists y\, (y > x)$ true? Is $\exists y\, \forall x\, (y > x)$ true? 3. Do $\exists x\, \exists y\, P(x,y)$ and $\exists y\, \exists x\, P(x,y)$ ever differ in truth value?

Answers

  1. The first lets each person have a (possibly different) best friend — it just says nobody is friendless. The second insists on one specific person who is simultaneously everyone's best friend. The second is much stronger and implies the first. 2. $\forall x\, \exists y\,(y>x)$ is true (take $y = x+1$); $\exists y\, \forall x\,(y>x)$ is false (the positive integers have no largest element, so no single $y$ beats them all). 3. No — two existentials of the same kind commute; both say "there is some pair $(x,y)$ with $P(x,y)$."

2.4 Negation: pushing $\neg$ through quantifiers

You negate quantified statements constantly, usually without realizing it. "It is not true that every test passes" — what exactly are you claiming? You are claiming some test fails. That move — turning the negation of a "for all" into a "there exists" — is the single most useful manipulation in this chapter, and it follows two clean, memorizable rules.

The quantifier negation laws (De Morgan for quantifiers). $$\neg \big(\forall x\, P(x)\big) \equiv \exists x\, \neg P(x),$$ $$\neg \big(\exists x\, P(x)\big) \equiv \forall x\, \neg P(x).$$ In words: negation flips the quantifier and moves inward. "Not all are $P$" becomes "some is not $P$"; "none is $P$" (i.e., not even one is $P$) becomes "all are not $P$."

🔗 Connection. These are exactly De Morgan's laws from Chapter 1, lifted to quantifiers. Recall over a finite domain that $\forall$ is a big $\land$ and $\exists$ is a big $\lor$. Chapter 1 told you $\neg(p \land q) \equiv \neg p \lor \neg q$ and $\neg(p \lor q) \equiv \neg p \land \neg q$. Push that across $n$ conjuncts: $\neg(P(d_1)\land\dots\land P(d_n)) \equiv \neg P(d_1)\lor\dots\lor\neg P(d_n)$, which is precisely "$\exists x\,\neg P(x)$." The quantifier laws are De Morgan's laws stretched over the whole domain.

Why this is the strategy before every disproof

The negation laws are not just symbol-shuffling — they tell you exactly what to look for when you want to disprove a statement. To refute "$\forall x\, P(x)$," negate it: you need "$\exists x\, \neg P(x)$" — a single element where $P$ fails. That element has a name.

Definition (counterexample). A counterexample to a universal statement $\forall x\, P(x)$ is a specific element $c$ of the domain for which $P(c)$ is false. Exhibiting one counterexample proves $\neg \forall x\, P(x)$ — it disproves the universal claim outright.

This is liberating. To prove a "for all" you must handle the entire (possibly infinite) domain. To disprove it, you exhibit one bad element and you are done. The asymmetry is the existential/​ universal asymmetry from 2.2, now put to work.

Worked example (disproof by counterexample). Claim: "Every prime number is odd." Domain: prime numbers; predicate $P(x)$ = "$x$ is odd." To disprove $\forall x\, P(x)$, find one prime that is even. The number $2$ is prime and even, so $P(2)$ is false. One counterexample, $x = 2$, disproves the claim. (Notice we did not need to inspect any other prime.)

Pushing negation through nested quantifiers

For nested statements, apply the two laws one quantifier at a time, from the outside in, flipping each quantifier as the negation passes it, until $\neg$ lands on the inner predicate. Mechanical, repeatable, no cleverness required.

Worked example. Negate $\forall x\, \exists y\, (x + y = 0)$ over the integers. Push $\neg$ inward:

$$ \neg\,\forall x\, \exists y\,(x+y=0) \;\equiv\; \exists x\, \neg\,\exists y\,(x+y=0) \;\equiv\; \exists x\, \forall y\, \neg(x+y=0) \;\equiv\; \exists x\, \forall y\,(x+y \ne 0). $$

Read the result: "there is an integer $x$ such that, for every integer $y$, $x + y \ne 0$" — i.e., "some integer cannot be cancelled by any integer." The original was true (every $x$ has the partner $-x$), so its negation is false, exactly as it should be. The procedure delivered the correct negation without any insight beyond "flip and move inward."

⚠️ Common Pitfall: negating an implication inside a quantifier. A huge fraction of universal statements have the restricted form $\forall x\,(Q(x) \rightarrow P(x))$ ("every $x$ that is $Q$ is also $P$"). Its negation is not $\exists x\,(Q(x) \rightarrow \neg P(x))$. Use Chapter 1's law $\neg(a \rightarrow b) \equiv a \land \neg b$: $$\neg\,\forall x\,(Q(x)\rightarrow P(x)) \;\equiv\; \exists x\,\big(Q(x) \land \neg P(x)\big).$$ A counterexample is an $x$ that is $Q$ and fails $P$. (To disprove "every prime is odd": find something that is prime and not odd — namely $2$. This matches the worked example exactly.)

Here is the negation move expressed as code that finds the counterexample — which is precisely what a property-based testing tool does under the hood:

def disprove_forall(predicate, domain):
    """Return a counterexample to 'forall x in domain: predicate(x)',
    or None if the predicate holds for every element (no counterexample found)."""
    for x in domain:
        if not predicate(x):
            return x          # witness to Exists x. not P(x)
    return None

primes = [2, 3, 5, 7, 11, 13]
print(disprove_forall(lambda p: p % 2 == 1, primes))   # "every prime is odd"?
# Expected output:
# 2

The returned 2 is the counterexample: the negation $\exists x\, \neg P(x)$ made concrete. Returning None would mean "no counterexample in this domain" — evidence, not proof, exactly as Chapter 6 will stress when it formalizes induction.

🔄 Check Your Understanding 1. Negate, in plain English: "Every file in the directory is read-only." 2. Push the negation all the way in: $\neg\, \exists x\, \forall y\, P(x, y)$. 3. What single thing must you produce to disprove "for all integers $n$, $n^2 > n$"? Produce it.

Answers

  1. "Some file in the directory is not read-only." (Flip $\forall$ to $\exists$, negate the predicate.) 2. $\neg\exists x\,\forall y\,P(x,y) \equiv \forall x\,\neg\forall y\,P(x,y) \equiv \forall x\,\exists y\,\neg P(x,y)$. 3. A single **counterexample** — an integer $n$ with $n^2 \le n$. Take $n = 1$: $1^2 = 1 \not> 1$. (Or $n = 0$.) One such $n$ disproves the claim.

2.5 Quantifiers as loops: all() and any()

Everything so far has a direct computational reading, and once you see it you will never read a for loop the same way. A universal quantifier over a finite domain is a loop that checks every element and fails fast; an existential quantifier is a loop that searches and succeeds fast. Python even ships the two quantifiers as built-in functions.

Bound and free variables (a necessary aside)

Before the code, one piece of vocabulary that the loop analogy makes vivid. In $\forall x\, P(x)$, the variable $x$ is controlled by the quantifier — you cannot substitute a value for it from outside, and renaming it ($\forall z\, P(z)$) changes nothing. Such a variable is bound. A variable not controlled by any quantifier is free, and the statement's truth still depends on it.

Definition (bound and free variables). An occurrence of a variable in a logical formula is bound if it falls within the scope of a quantifier ($\forall$ or $\exists$) over that variable; otherwise it is free. A formula with no free variables is a proposition (it has a definite truth value, relative to the domain); a formula with at least one free variable is a predicate.

The loop analogy makes this concrete: a bound variable is the loop variable (local to the loop, invisible outside, freely renameable), while a free variable is a parameter from the enclosing scope (its value comes from outside and matters). Compare:

def all_positive(items):       # 'items' is FREE (a parameter); 'x' is BOUND (loop-local)
    return all(x > 0 for x in items)   # x ranges over the domain, like ∀x

Here items plays the role of a free variable (the statement's truth depends on which list you pass), and x plays the role of the bound variable in $\forall x\,(x > 0)$ — internal to the comprehension, renameable to y with no effect, meaningless outside the all(...).

all() is $\forall$; any() is $\exists$

The correspondence is exact:

$$\forall x \in D,\ P(x) \quad\longleftrightarrow\quad \texttt{all(P(x) for x in D)},$$ $$\exists x \in D,\ P(x) \quad\longleftrightarrow\quad \texttt{any(P(x) for x in D)}.$$

nums = [4, 8, 15, 16, 23, 42]
print(all(n % 2 == 0 for n in nums))   # forall n: n is even?
print(any(n % 2 == 0 for n in nums))   # exists n: n is even?
print(any(n > 100 for n in nums))      # exists n: n > 100?
# Expected output:
# False
# True
# False

Trace the first: all(...) walks the list and returns False as soon as it meets an odd number — and $15$ is the first odd number, so it stops there. That early exit is not an optimization detail; it is the logic. $\forall x\, P(x)$ is false the instant one $P(x)$ fails (a single false conjunct sinks the big $\land$), so all() is entitled to stop and report False. Symmetrically, any(...) returns True the instant it finds one even number ($4$, immediately), because one true disjunct settles the big $\lor$.

🔗 Connection: short-circuit evaluation is the quantifier asymmetry in your compiler. The reason and/or short-circuit (Chapter 1's payoff) and the reason all/any stop early are the same reason: $\land$ needs only one False, $\lor$ needs only one True. When you write if user and user.is_admin:, you are relying on the same logical fact that lets all() bail out at the first counterexample. Logic, evaluated.

What is $\forall x\, P(x)$ when the domain is empty? There are no elements to violate $P$, so by the "one false conjunct sinks it" reading there is nothing to sink it — the statement is vacuously true. And $\exists x\, P(x)$ over an empty domain is false — there is no element to serve as a witness. Python agrees, and the behavior trips up beginners constantly:

print(all(x > 0 for x in []))    # forall over empty domain
print(any(x > 0 for x in []))    # exists over empty domain
# Expected output:
# True
# False

all([]) is True (vacuously — "every element of the empty set is positive" is technically correct, the best kind of correct) and any([]) is False (no witness can exist). This is not a Python quirk; it is the only consistent choice, matching the conjunction/​disjunction reading and the identity elements of $\land$ (which is True) and $\lor$ (which is False).

⚠️ Common Pitfall: vacuous truth in real code. all(user.has_paid for user in users) returns True when users is empty — which may not be what your business logic wants ("all customers have paid" when you have zero customers?). Guard explicitly when the empty case matters: users and all(...). Countless validation bugs are a vacuously-true all() over an unexpectedly empty collection.

🔄 Check Your Understanding 1. Rewrite "$\exists x \in \texttt{xs}$ such that $x < 0$" as a one-line Python expression. 2. Why does all() return as soon as it sees one falsy element, but any() keeps going past falsy elements? 3. What does any(x for x in []) evaluate to, and which fact about $\exists$ over an empty domain explains it?

Answers

  1. any(x < 0 for x in xs). 2. all computes a big $\land$, which is False the moment any conjunct is False — so one falsy element settles it. any computes a big $\lor$, which needs a True; falsy elements don't settle it, so it must keep searching until it finds a truthy one (or exhausts the domain). 3. False — an existential over an empty domain has no possible witness, so it is false.

2.6 Specifying programs: preconditions and postconditions

Now the payoff that justifies the whole chapter. Predicate logic is the language in which you say what a program is supposed to do — not how it does it, but what must be true before it runs and what it promises afterward. This is the bedrock of program specification, of assertions, of API contracts, and of every formal-verification tool in existence.

A function's contract has two halves, and both are predicates on the program's state:

  • A precondition is a predicate that must be true when the function is called — the caller's obligation. ("The list is sorted." "The denominator is non-zero.")
  • A postcondition is a predicate that the function guarantees will be true when it returns — the function's promise, assuming the precondition held. ("The result is the smallest index of the target." "The output list is a sorted permutation of the input.")

These read directly as quantified statements. Consider binary search:

def binary_search(arr, target):
    """Precondition:  arr is sorted ascending:
                      forall i. 0 <= i < len(arr)-1  ->  arr[i] <= arr[i+1]
       Postcondition: returns an index j with arr[j] == target if target is in arr
                      (exists j. arr[j] == target), else returns -1."""
    lo, hi = 0, len(arr) - 1
    while lo <= hi:
        mid = (lo + hi) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            lo = mid + 1
        else:
            hi = mid - 1
    return -1

Read the precondition out loud and you are reading a universal statement: $$\forall i\,\big(0 \le i < \text{len}(arr)-1 \;\rightarrow\; arr[i] \le arr[i+1]\big).$$ Note the restricted-$\forall$-with-$\rightarrow$ idiom from 2.2: for all indices $i$, if $i$ is in range, then the element at $i$ is $\le$ the next one. And the "found" case of the postcondition is an existential: $\exists j\,(arr[j] = target)$. The contract of binary search is two quantified statements, one $\forall$ and one $\exists$ — predicate logic, doing its actual job.

Checking a precondition is evaluating a quantifier

Because the precondition is a universal statement over a finite domain (the indices), you can check it with exactly the loop from 2.5:

def is_sorted(arr):
    """True iff forall i in [0, len-2]: arr[i] <= arr[i+1]."""
    return all(arr[i] <= arr[i + 1] for i in range(len(arr) - 1))

print(is_sorted([1, 3, 3, 7, 9]))   # the precondition holds
print(is_sorted([1, 3, 2, 7]))      # violated at i = 1 (3 > 2)
# Expected output:
# True
# False

is_sorted is the precondition predicate $\forall i\,(\dots)$ rendered as all(...). A False result hands you the negation $\exists i\,\neg(\dots)$ — a witnessing index where order breaks. Defensive code that does assert is_sorted(arr) at function entry is literally checking a quantified precondition before trusting the algorithm whose correctness depends on it.

🔗 Connection. The postcondition "the output is sorted and a permutation of the input" is the spec every sorting algorithm must meet, and proving an algorithm meets its postcondition is what loop invariants are for — the technique you'll develop fully in Chapter 6. A loop invariant is a predicate that stays true on every pass; initialization establishes it, maintenance preserves it, and at termination it implies the postcondition. Specifications (this section) say what; invariants (Chapter 6) prove that. You will also see these contracts again as the inputs and outputs of functions when we study them formally in Chapter 9.

Why specifications beat tests (theme two)

A test checks the postcondition for one input: "for this array, binary search returned the right index." A specification states the postcondition for all valid inputs: $\forall$ arrays satisfying the precondition, the function meets its promise. The quantifier is the entire difference. "It passed the tests" verifies finitely many points of the domain; "it satisfies its specification" is a universal claim over the whole domain — and only a proof (Part I's real subject, beginning in earnest in Chapters 4–6) can establish a universal claim. This is theme two of the book, stated in the language of this chapter: a passing test is one true conjunct; correctness is the whole $\forall$.

🔄 Check Your Understanding 1. Classify each as a precondition or a postcondition for a pop() on a stack: (a) "the stack is non-empty"; (b) "the returned value was the most recently pushed element." 2. Write the precondition "every element of arr is non-negative" as a Python expression. 3. In one sentence, why can a finite test suite never establish a postcondition that is universally quantified over an infinite input domain?

Answers

  1. (a) precondition (must hold when pop is called); (b) postcondition (the guarantee on return). 2. all(x >= 0 for x in arr). 3. A test checks finitely many inputs (finitely many true conjuncts of the big $\land$), but a universal claim over an infinite domain has infinitely many conjuncts — no finite check can rule out a counterexample among the untested ones; only a proof can.

Project Checkpoint: a predicate evaluator for the Toolkit

Theme four of this book is that computation and proof are complementary: code can evaluate a quantified statement over a finite domain (fast, but only for the elements you actually loop over), while a proof settles it for the whole domain. In Chapter 1 you began dmtoolkit/logic.py with a truth-table generator. Now we extend it with the two quantifiers, plus a counterexample finder — the computational core of everything in 2.4 and 2.5.

Add to dmtoolkit/logic.py:

def for_all(predicate, domain):
    """Evaluate ∀x in domain: predicate(x). True iff predicate holds for every element.
    Mirrors all(); over an EMPTY domain this is vacuously True."""
    return all(predicate(x) for x in domain)

def there_exists(predicate, domain):
    """Evaluate ∃x in domain: predicate(x). True iff predicate holds for some element.
    Mirrors any(); over an EMPTY domain this is False."""
    return any(predicate(x) for x in domain)

def counterexample(predicate, domain):
    """Return the first x in domain with predicate(x) False (a witness to
    ∃x. ¬predicate(x)), or None if predicate holds for all of domain.
    Finding None is EVIDENCE the ∀ holds over this domain, not a PROOF."""
    for x in domain:
        if not predicate(x):
            return x
    return None

A quick hand-traced demonstration on the claims from this chapter:

ints = range(-5, 6)
print(for_all(lambda x: x * x >= 0, ints))         # ∀x. x² ≥ 0  over the slice
print(there_exists(lambda x: x * x == 4, ints))    # ∃x. x² = 4  (x = 2 or -2)
print(counterexample(lambda p: p % 2 == 1, [2, 3, 5, 7]))  # "every prime is odd"?
# Expected output:
# True
# True
# 2

The first is True (every square is non-negative — and here it truly holds over the whole slice); the second is True (witnesses $2$ and $-2$ lie in the slice); the third returns 2, the counterexample that disproves "every prime is odd." Note the duality baked into the API: counterexample(P, D) returns None exactly when for_all(P, D) returns True — the negation law $\neg\forall x\,P(x) \equiv \exists x\,\neg P(x)$, now executable.

Toolkit so far: logic.py now holds the truth-table tools from Chapters 1–3 plus for_all, there_exists, and counterexample. Together with Chapter 6's check_identity, your library can already evaluate and try to refute quantified claims over finite domains — the testing half of theme four. By the capstone, these quantifier primitives reappear inside the Sudoku solver (Track C), where "every row contains each digit exactly once" is a for_all over rows of an exists-style constraint.


Summary

Predicate logic extends propositional logic with objects, properties, and quantities. The reference facts to carry forward:

Core objects

Object What it is Truth value?
Proposition (Ch. 1) A statement, definitely true or false Yes
Predicate $P(x)$ A statement with variable(s) — a boolean-valued function Only after variables are assigned
Domain The collection a variable ranges over (Part of every quantified statement's meaning)
$\forall x\, P(x)$ "For all $x$, $P(x)$" — a giant conjunction Yes (relative to domain)
$\exists x\, P(x)$ "There exists $x$, $P(x)$" — a giant disjunction Yes (relative to domain)

Restriction idioms — $\forall$ pairs with $\rightarrow$; $\exists$ pairs with $\land$:

English Logic
Every $Q$ is a $P$ $\forall x\,(Q(x) \rightarrow P(x))$
Some $Q$ is a $P$ $\exists x\,(Q(x) \land P(x))$

Negation laws (De Morgan for quantifiers — flip the quantifier, move $\neg$ inward):

$$\neg\forall x\, P(x) \equiv \exists x\, \neg P(x), \qquad \neg\exists x\, P(x) \equiv \forall x\, \neg P(x),$$ $$\neg\forall x\,(Q(x)\rightarrow P(x)) \equiv \exists x\,(Q(x) \land \neg P(x)).$$

A counterexample — one element where $P$ fails — disproves $\forall x\, P(x)$ outright.

Nested quantifiers — order is meaning:

Form Reading The dependence
$\forall x\, \exists y\, P(x,y)$ every $x$ has some (possibly different) $y$ inner $y$ may depend on outer $x$
$\exists y\, \forall x\, P(x,y)$ one $y$ works for every $x$ the $y$ is fixed once, for all $x$

Like quantifiers commute ($\forall\forall$, $\exists\exists$); mixed quantifiers in general do not. $\exists y\,\forall x$ implies $\forall x\,\exists y$, but not conversely.

Computational reading

Logic Code Behavior
$\forall x \in D,\ P(x)$ all(P(x) for x in D) fails fast on first false; vacuously True on empty $D$
$\exists x \in D,\ P(x)$ any(P(x) for x in D) succeeds fast on first true; False on empty $D$
bound variable loop variable local, renameable, invisible outside
free variable enclosing parameter value comes from outside; truth depends on it

Specification — a precondition is the caller's obligation (often a $\forall$ over indices/​ elements); a postcondition is the function's guarantee (often an $\exists$ for "found" or a $\forall$ for "all outputs valid"). A passing test verifies one point of the domain; the specification is a universal claim only a proof can settle.


Spaced Review

Retrieval keeps knowledge available. Answer from memory before checking. (These revisit Chapter 1 — the only prior chapter — plus this chapter's threshold idea.)

  1. (Ch. 1) State De Morgan's laws for $\land$ and $\lor$. Then explain in one sentence how the quantifier negation laws of §2.4 are the same laws applied to the conjunction/​disjunction readings of $\forall$/$\exists$.
  2. (Ch. 1) Why does the restricted universal "every $Q$ is a $P$" use the implication $Q(x) \rightarrow P(x)$ rather than $Q(x) \land P(x)$? (Hint: what is the truth value of $F \rightarrow T$, and what should happen for elements that aren't $Q$?)
  3. (Ch. 1) Short-circuit evaluation of and/or and the early exit of all/any rest on one shared logical fact. State it.
  4. (Ch. 2) Negate $\forall x\,\exists y\,(x \cdot y = 1)$ by pushing $\neg$ all the way in, and say in English what the negation claims.

Answers

  1. $\neg(p \land q) \equiv \neg p \lor \neg q$ and $\neg(p \lor q) \equiv \neg p \land \neg q$. Over a finite domain $\forall$ is a big $\land$ and $\exists$ is a big $\lor$, so negating $\forall x\,P(x) = P(d_1)\land\dots\land P(d_n)$ by De Morgan gives $\neg P(d_1)\lor\dots\lor\neg P(d_n) = \exists x\,\neg P(x)$ — same law, stretched over the domain. 2. Because the claim only constrains elements that are $Q$; for an element that isn't $Q$, the implication $Q(x)\rightarrow P(x)$ is vacuously true ($F \rightarrow \text{anything} = T$), harmlessly ignoring it, whereas $Q(x)\land P(x)$ would falsely demand *every* element be $Q$. 3. $\land$ is False as soon as one operand is False; $\lor$ is True as soon as one operand is True — so evaluation can stop at the first decisive operand. 4. $\neg\forall x\,\exists y\,(xy=1) \equiv \exists x\,\forall y\,(xy \ne 1)$: "there is an $x$ such that no $y$ gives $x \cdot y = 1$" — i.e., some element has no multiplicative partner (true over the integers: $x = 0$, or any $x$ with $\lvert x\rvert \ge 2$).

What's Next

You can now express claims about all and some, negate them mechanically, and read them as loops and as program contracts. But expressing a claim is not the same as justifying one. When you assert $\forall x\, P(x)$, how do you actually establish it — beyond testing finitely many elements and hoping? And when you chain claims together — "if every input is valid, and validity implies success, then ..." — which inference steps are legitimate and which are seductive fallacies? That is the subject of Chapter 3, Rules of Inference, which takes the quantifiers you just learned and the connectives from Chapter 1 and forges them into the valid argument forms — modus ponens, universal instantiation, and their kin — that every proof in the rest of this book is built from.