# Predicate Logic & Quantifiers

> Propositional logic treats whole statements as atoms. Predicate logic looks inside them - at properties of things and the words 'for all' and 'there exists' - which is how you say precise things about whole collections at once.


---

# Predicate Logic & Quantifiers

[Propositional Logic](/guides/propositional-logic) gave you AND, OR, and NOT - but it treats every
statement as a single sealed atom. "All users have a password" is only `P` to it; it can't see the
*all*, can't see the *users*, can't reason about them one by one. That's a ceiling you hit fast, because
almost everything worth saying is a statement *about a collection*: every request, some account, no
file.

Predicate logic raises that ceiling. It cracks statements open to talk about **properties of things**
(predicates) and adds two small words that do enormous work: **for all** (∀) and **there exists** (∃).
With them you can say exactly what's true of an entire set, spot when someone overclaims ("*all*?
really?"), and negate a sweeping statement correctly. If you've ever written `.all()`, `.any()`,
`.every()`, or `.some()`, you've already used this - here's the logic underneath.

## How to read this
- **Want the two power words?** [Phase 2](02-quantifiers-for-all-there-exists.md) is ∀ and ∃ - the heart
  of the guide.
- **Want it solid?** Read in order - Phase 1 explains predicates, which the quantifiers act on.

## The phases
1. **[Predicates: Statements With Variables](01-predicates-statements-with-variables.md)** - a statement
   with a blank in it, and the "domain" it ranges over.
2. **[Quantifiers: For All and There Exists](02-quantifiers-for-all-there-exists.md)** - ∀ and ∃, what
   makes each true, and the counterexample that kills a "for all."
3. **[Negating & Nesting Quantifiers](03-negating-and-nesting-quantifiers.md)** - how to negate "for
   all" / "there exists" correctly, and why the *order* of nested quantifiers changes the meaning.

> This builds on [Propositional Logic](/guides/propositional-logic) and uses the idea of a set from
> [Sets, Relations & Functions](/guides/sets-relations-and-functions). The Logic track continues into
> proof and spotting fallacies.


---

# Predicates: Statements With Variables

## Where we left off

In [propositional logic](/guides/propositional-logic), every statement was a single sealed box.
"It is raining" was one atom, either true or false, and you never looked inside it. You combined
those boxes with `and`, `or`, `not`, and `→`, but the box stayed opaque. That worked until you
wanted to say something that wasn't about *one* fixed thing.

Try saying "every number greater than one has a prime factor" with only sealed boxes. You can't.
There's no single true-or-false statement there - there's a *pattern* that's supposed to hold for
many things at once. To talk about that, you have to open the box and look at the variable inside.

That's what predicate logic does. It looks *inside* a statement.

## A predicate is a statement with a blank

Here's the core idea. A **predicate** is a statement with one or more variables in it. On its own
it has no truth value - not true, not false - because it isn't finished. It's a statement with a
blank, waiting for you to fill it.

```text
"___ is even"
```

Until you say what goes in the blank, asking "is that true?" makes no sense. True for *what*?

We write predicates like functions, with the blank named as a variable:

```text
P(x) = "x is even"
```

The `x` is the blank. `P` is the name we gave this predicate, the way you'd name a function. Now
fill the blank by handing it a value:

```text
P(4)  →  "4 is even"   →  true
P(7)  →  "7 is even"   →  false
```

Notice what happened. `P(x)` had no truth value. `P(4)` does - a real, finished statement that
happens to be true. Filling the blank turned a *predicate* into a proposition, the kind of sealed
box from the last guide.

💡 A clean way to hold this: a predicate is a *machine that produces propositions*. Feed it a value,
it hands you back something true or false. It is not, itself, true or false.

## Predicates can have more than one blank

A predicate isn't limited to one variable. Some statements relate two things, or three:

```text
Older(a, b) = "a is older than b"
```

This one has two blanks, so you fill both before you get a truth value:

```text
Older(Maya, Sam)   →  "Maya is older than Sam"   →  true or false (depends on the people)
Older(Sam, Maya)   →  "Sam is older than Maya"   →  the opposite
```

Order matters, the same way it does in subtraction. `Older(a, b)` and `Older(b, a)` are different
statements. Filling one blank but not the other still gets you no truth value -
`Older(Maya, x)` is *still* a predicate, only a smaller one. It now means "Maya is older than ___",
true or false only once you say who `x` is.

📝 The number of blanks is the predicate's **arity**: one blank is *unary*, two is *binary*. You
don't need the vocabulary, but you'll see it.

## The domain: what the blank is allowed to be

There's a quiet question behind every predicate: *what kinds of things are allowed in the blank?*

For `P(x) = "x is even"`, plugging in `4` is fine. But what would `P("banana")` mean? "Banana is
even" isn't false - it's nonsense. Evenness is about numbers, not fruit. So we always have in mind a
set of things the variable is allowed to range over. That set is the **domain of discourse** (or the
*domain*, or *universe*).

If you've met [sets, relations, and functions](/guides/sets-relations-and-functions), this is
exactly a set: the collection of legal values for the variable. Stating the domain is part of
stating the predicate. "`P(x) = "x is even"` over the domain of integers" is a complete thought;
"`P(x) = "x is even"`" with no domain is vague about what you're allowed to ask.

Here's why this matters and isn't mere bookkeeping: **the same predicate behaves differently over
different domains.**

```text
P(x) = "x is even"

Domain = whole numbers {0, 1, 2, 3, ...}
   →  some are even (0, 2, 4), some are not (1, 3, 5)

Domain = even numbers {0, 2, 4, 6, ...}
   →  every single x in the domain makes P(x) true

Domain = odd numbers {1, 3, 5, 7, ...}
   →  P(x) is false for every x in the domain
```

Same words, "x is even." Three different domains. Whether the predicate is *ever* true, *always*
true, or *never* true depends entirely on what you let `x` be. That dependence is the whole game in
the next phase, so let it sink in now: the domain isn't a detail, it's half the statement.

## For builders

If you write code, you use predicates constantly - under a different name.

A predicate is a **function that returns a boolean**:

```text
is_even(x):
    return x % 2 == 0
```

`is_even` on its own isn't true or false - it's a function. `is_even(4)` returns `true`;
`is_even(7)` returns `false`. That's `P(4)` and `P(7)`, exactly. The mathematician's `P(x)` and the
programmer's `is_even(x)` are the same object in different clothes.

And the domain? That's roughly the *type* of the argument. `is_even` expects an integer; handing it a
string is a type error - the programming version of "banana is even" being nonsense rather than
false.

You'll also notice that lots of standard library tools *take a predicate as an argument*. `filter()`
is the clearest case:

```text
filter(is_even, [1, 2, 3, 4, 5, 6])   →  [2, 4, 6]
```

`filter` walks the list and keeps each element for which the predicate returns true. That list is, in
effect, the domain. So `filter` asks, for each `x` in the domain, "is `P(x)` true?" - and that
question is the seed of the quantifiers you'll meet next.

## ⚠️ A predicate alone is not true or false

This is the one trap to remember, because it's tempting to treat `P(x)` like a fact.

```text
P(x) = "x is even"
```

If someone asks "is `P(x)` true?", the real answer is *the question is incomplete*. There's a free
variable `x` with no value, so there's nothing to evaluate. It's like asking "is the door locked?"
when there are a hundred doors and you haven't said which one.

There are exactly two ways to give `P(x)` a truth value:

1. **Fill the blank** with a specific value - `P(4)` - turning it into a proposition.
2. **Quantify** it - say something about *all* x, or *some* x, in the domain.

That second option is the whole next phase. Statements like "*for all* x in the domain, P(x) is
true" and "*there exists* an x in the domain where P(x) is true" take a predicate plus a domain and
produce something true or false - without pinning `x` to a single value. That's the bridge from
"statement with a blank" back to "statement you can actually judge."

## Recap

- A **predicate** is a statement with one or more variables (blanks) in it. We write it `P(x)`.
- A predicate **has no truth value by itself**. It's a machine for producing propositions, not a
  proposition.
- **Fill the blank** with a value and you get something true or false: `P(4)` is true, `P(7)` is
  false.
- Predicates can have several blanks: `Older(a, b)` needs both filled, and order matters.
- The **domain of discourse** is the set of things the variable is allowed to be. The same predicate
  can be sometimes-true, always-true, or never-true depending on its domain.
- **For builders:** a predicate is a boolean-returning function like `is_even(x)`, and `filter()` is
  a function that takes a predicate.
- Next up: how *for all* and *there exists* turn a predicate plus a domain into a real truth value.

## Open-ended exercise

Consider this code:

```text
const admins = users.filter(u => u.role === 'admin');
```

The `filter` method takes a predicate - here, `u.role === 'admin'`. Now write, in
plain English, what the *domain* is for this predicate, and what the predicate claims
about each element. Then: is `filter` checking a `∀` claim or an `∃` claim? Why?

Quick check before you move on:

```quiz
[
  {
    "q": "Which of these best describes a predicate?",
    "choices": [
      "A statement with one or more variables that has no truth value until the variables are filled in",
      "A statement that is always true",
      "A logical connective like 'and' or 'or'",
      "A number that can be even or odd"
    ],
    "answer": 0,
    "explain": "A predicate, like P(x) = 'x is even', is a statement with a blank. It only becomes true or false once the blank is filled (or quantified)."
  },
  {
    "q": "Given P(x) = \"x is even\", what is the truth value of P(x) on its own, with no value chosen for x?",
    "choices": [
      "Always true",
      "Always false",
      "It has no truth value yet - the question is incomplete until x is fixed",
      "It depends on whether x is a letter or a number"
    ],
    "answer": 2,
    "explain": "With a free variable and no value, there's nothing to evaluate. P(4) is true and P(7) is false, but P(x) by itself is neither."
  },
  {
    "q": "What does the 'domain of discourse' of a predicate refer to?",
    "choices": [
      "The truth value the predicate returns",
      "The set of things the variable is allowed to range over",
      "The name given to the predicate, like P or Older",
      "The number of variables (blanks) the predicate has"
    ],
    "answer": 1,
    "explain": "The domain is the set of legal values for the variable. The same predicate can behave very differently over different domains - for example, 'x is even' is always true over the even numbers but never true over the odd numbers."
  }
]
```


---

# Quantifiers: For All and There Exists

In Phase 1 you met predicates - statements with a hole in them, like `P(x): x is even`. A
predicate isn't true or false on its own; it's waiting for an `x`. This phase covers the two
words that fill that hole all at once and turn a predicate into a real claim: **for all** and
**there exists**. Once you can read them like a sentence, a huge amount of formal writing stops
looking like hieroglyphics.

## First, what's a domain again?

Every quantified claim lives inside a **domain**: the collection of things `x` is allowed to be.
Without a domain, "for all x" means nothing - all *what*? People? Numbers? Files on disk? For
most of this phase the domain is the **natural numbers**: `0, 1, 2, 3, …`. When you read a
quantifier, whisper the domain to yourself - "for all `x`" really means "for all `x` *in this
collection*." (The [Sets, Relations & Functions](/guides/sets-relations-and-functions) guide
builds domains up properly, but "the bag of things `x` ranges over" is enough for now.)

## The universal quantifier: ∀ ("for all")

The symbol `∀` is an upside-down A (think **A** for "All"). You write:

```text
∀x P(x)
```

and you read it: **"for all x in the domain, P(x) is true."** `∀x P(x)` is a single statement -
true or false, no leftover hole - and it's true under exactly one condition:

> `∀x P(x)` is **true** only when *every single element* of the domain makes `P` true.
> If even one element fails, the whole statement is **false**.

A "for all" claim is a promise about the entire collection at once. It's a big bet:
*no exceptions, anywhere.*

Concrete example, domain = natural numbers:

```text
∀n (n + 1 > n)        "every natural number is smaller than its successor"
```

Pick any `n` - `0`, `7`, `1000000`. Adding 1 always lands you somewhere bigger. There's no number
where this breaks. So `∀n (n + 1 > n)` is **true**.

Now a false one:

```text
∀n (n is even)        "every natural number is even"
```

This bets that *nothing* is odd. But `1` is right there. One number wrecks it. So `∀n (n is even)`
is **false** - and the number that wrecks it has a name.

## The existential quantifier: ∃ ("there exists")

The symbol `∃` is a backwards E (think **E** for "Exists"). You write:

```text
∃x P(x)
```

and you read it: **"there exists an x in the domain such that P(x) is true."** This is a much
humbler claim - it promises nothing about the whole collection, only that *somewhere in here, at
least one thing works.*

> `∃x P(x)` is **true** as soon as *at least one* element makes `P` true.
> It's **false** only when *nothing at all* in the domain works.

Concrete example, domain = natural numbers:

```text
∃n (n is even)        "some natural number is even"
```

Is there even one even number? Yes - `2` works. (So do `0`, `4`, `100`.) You only needed one. So
`∃n (n is even)` is **true**.

Notice we did *not* check every number. The moment we found `2`, we were done. That "one is enough"
feeling is the whole personality of `∃`.

## Quantifier scope: how far does the claim reach?

A quantifier's **scope** is the part of the statement it controls. When you write
`∀x (P(x) → Q(x))`, the quantifier reaches across the whole parentheses. When you
nest quantifiers, the order changes what's claimed:

```mermaid
flowchart LR
    subgraph Outer[∀x outer]
        subgraph Inner[∃y inner]
            P[P x y]
        end
    end
    Outer --> Result["For every x, there is SOME y"]
```

```mermaid
flowchart LR
    subgraph Outer2[∃y outer]
        subgraph Inner2[∀x inner]
            P2[P x y]
        end
    end
    Outer2 --> Result2["There is ONE y that works for ALL x"]
```

Same letters, opposite meaning. Swapping them is not a style choice - it changes the claim.

## The asymmetry that matters most

Here is the single most useful idea in this entire guide. Read it twice.

- To **disprove** a `∀` claim, you need exactly **one counterexample** - one element where
  the predicate fails.
- To **prove** an `∃` claim, you need exactly **one witness** - one element where the
  predicate holds.

That's it. The two quantifiers are mirror images:

```text
∀x P(x)   →  one FAILING element makes it FALSE   (a counterexample)
∃x P(x)   →  one PASSING element makes it TRUE    (a witness)
```

This asymmetry is *why* the symbols are worth learning. It tells you how to argue about collections
you could never fully inspect - even infinite ones.

Think about `∀n (n is even)` over the natural numbers. You can't check infinitely many numbers. But
you don't have to. You produce `n = 1`, point at it, and say "this is odd, so the claim that *all*
numbers are even is false." Done. One counterexample beats an infinite "for all."

The same trick runs the other way. To show `∃n (n + n = 6)` is true, you don't search the whole
number line. You hand over `n = 3` and say "there's your witness." One example beats an infinite
"there exists" search.

⚠️ **Watch the direction.** One example does *not* prove a `∀`. Showing that `2` is even tells you
*nothing* about whether *all* numbers are even. And one example does not *disprove* an `∃` - finding
one odd number doesn't mean no even number exists. Examples prove `∃` and kill `∀`; they do not
prove `∀` or kill `∃`. Getting this backwards is the classic mistake.

## Why "for all" is the fragile one

A `∀` claim is *strong* - it says a lot - which is exactly why it's *fragile*. It has to be right
about everything, so one overlooked case brings it all down. "All swans are white" survives
thousands of white swans and dies the instant one black swan walks in. A `∃` claim is *weak* - it
says very little - which is exactly why it's *sturdy*: it needs one thing to go right, and that
one thing is usually easy to point at.

So when someone makes a sweeping "every… / all… / always…" statement, the experienced move is to
hunt for the one case that breaks it. And when someone says "that can never happen / no input ever
does X," they've made a `∀` in disguise (for all x, *not* X) - so again, one example settles it.
[Phase 3](03-negating-and-nesting-quantifiers.md) shows exactly how "never" becomes a hidden `∀`.

## For builders

If you write code, you use both quantifiers constantly under different names. A quantifier ranges
over a domain; a loop or a collection method ranges over a list.

- `∀x P(x)` is **`all(...)`** in Python, **`.every(...)`** in JavaScript - true only if the
  predicate holds for *every* element.
- `∃x P(x)` is **`any(...)`** in Python, **`.some(...)`** in JavaScript - true if the predicate
  holds for *at least one* element.

```text
∀n (n > 0)   ≈   all(n > 0 for n in nums)     # all() / .every()
∃n (n > 0)   ≈   any(n > 0 for n in nums)     # any()  / .some()
```

And the asymmetry shows up as a real optimization: these functions **short-circuit**.

- `all()` / `.every()` stops at the **first element that fails** - that failing element is
  your counterexample. (`all` over an empty list is `true`: there's no failure to find.)
- `any()` / `.some()` stops at the **first element that passes** - that passing element is
  your witness. (`any` over an empty list is `false`: there's nothing to witness.)

So "falsify a `∀`" and "find the first failing element" are *literally the same operation*. The
logic you learned is the control flow your language already implements.

## Recap

- **`∀x P(x)`** - "for all x, P(x)." True only when **every** element of the domain
  satisfies `P`. The upside-down A is for **A**ll.
- **`∃x P(x)`** - "there exists an x such that P(x)." True when **at least one** element
  satisfies `P`. The backwards E is for **E**xists.
- The key asymmetry: **one counterexample** makes a `∀` false; **one witness** makes an `∃`
  true. This is how you reason about whole collections - even infinite ones - without
  inspecting them all.
- Examples *prove* `∃` and *kill* `∀`. They do **not** prove `∀` or kill `∃`. Don't mix up
  the direction.
- In code: `∀` is `all()` / `.every()`, `∃` is `any()` / `.some()`, and short-circuiting is
  the counterexample/witness idea in action.

If predicates still feel fuzzy, revisit
[Predicates](01-predicates-statements-with-variables.md). For the bigger picture of what
formal claims even are, [What Logic Actually Is](/guides/what-logic-actually-is) and
[Propositional Logic](/guides/propositional-logic) sit underneath everything here. And if the
symbols still trigger a flinch, [Why Math Isn't Your Enemy](/guides/why-math-isnt-your-enemy)
is a gentler on-ramp.

## Open-ended exercise

A database query returns 10,000 rows. A teammate says: "All of them have a non-null email
address." Is this a `∀` claim or an `∃` claim? What would it take to *prove* it versus
what would it take to *disprove* it? Now suppose the teammate instead says: "At least one
row has a non-null email address." How does the burden of proof flip?

Quick check before you move on:

```quiz
[
  {
    "q": "Over the natural numbers, what does ∀n (n + 1 > n) claim?",
    "choices": [
      "Every natural number is smaller than its successor",
      "Some natural number is smaller than its successor",
      "There is a natural number with no successor",
      "Exactly one natural number satisfies n + 1 > n"
    ],
    "answer": 0,
    "explain": "∀ means 'for all.' ∀n (n + 1 > n) says that for every n in the domain, n + 1 > n holds - every number is smaller than the next."
  },
  {
    "q": "What is the minimum you need to show that ∀x P(x) is FALSE?",
    "choices": [
      "Show P fails for every element",
      "Show P holds for at least one element",
      "Find a single element where P fails (one counterexample)",
      "Check half of the domain"
    ],
    "answer": 2,
    "explain": "A 'for all' claim is fragile: one counterexample - a single element where the predicate fails - makes the whole statement false. You never need more than one."
  },
  {
    "q": "Which statement correctly describes ∃x P(x)?",
    "choices": [
      "It is true only if P holds for every element of the domain",
      "It is true if P holds for at least one element of the domain",
      "It is false if P holds for exactly one element",
      "It says nothing unless the domain is infinite"
    ],
    "answer": 1,
    "explain": "∃ means 'there exists.' ∃x P(x) is true the moment one element (a witness) satisfies P; it's false only when nothing in the domain works."
  }
]
```


---

# Negating & Nesting Quantifiers

You've met `∀` ("for all") and `∃` ("there exists"). You can read them and build statements with
them. Now comes the move that turns quantifiers into a tool you reach for in real arguments:
knowing how to say **no** to one.

Here's the situation you'll be in. Someone makes a sweeping claim - "every one of our tests passes,"
"all the records have a timestamp," "nobody on the team missed the deadline." You suspect they're
wrong. How do you *correctly* push back - not with an equally sweeping counter-claim, but by finding
the one crack? This phase is about doing that precisely, and about a second trap that catches almost
everyone: what happens when quantifiers stack up.

## Negating "for all": one counterexample is enough

Take a claim with `∀`:

```text
∀x P(x)        "every x has property P"
"Every test passed."
```

What makes this **false**? You don't need *every* test to fail, or even most of them. You need
exactly one test that didn't pass. One. That single failing test is a **counterexample**, and it's
the whole ballgame. So the negation of "everyone passed" is not "everyone failed." It's:

```text
¬∀x P(x)  ≡  ∃x ¬P(x)
"It's not the case that every x has P"
   is the same as
"There exists an x that does not have P."
```

In words: *not all passed* means *someone did not pass*. The `∀` flips to `∃`, and the property
flips to its opposite. This matters because the wrong negation is a common mistake: if you think the
opposite of "everyone passed" is "everyone failed," you've claimed something far stronger than you
can support. The real opposite is humble - *at least one exception exists.*

## Negating "there exists": you have to rule out every case

Now the other direction. Take a claim with `∃`:

```text
∃x P(x)        "some x has property P"
"Some test failed."
```

For *this* to be false, pointing at one passing test isn't enough - the failing one could be the
next test over. To kill an existence claim, you have to show the property holds for *nothing in the
domain*:

```text
¬∃x P(x)  ≡  ∀x ¬P(x)
"There is no x with P"
   is the same as
"Every x lacks P."
```

In words: *nobody passed* means *everyone failed*. The `∃` flips to `∀`, and again the property
flips to its opposite. Notice the asymmetry in effort, because it's real and useful:

```text
To DISPROVE "for all"  →  find ONE counterexample.      (cheap)
To DISPROVE "exists"   →  check EVERYTHING.              (expensive)
```

That asymmetry is why mathematicians love disproving universal claims and dread disproving existence
claims. One is a treasure hunt that ends the moment you find the prize; the other is a full
inventory.

## This is De Morgan, stretched over a domain

If those two flips feel familiar, they should. Back in
[propositional logic](/guides/propositional-logic) you met De Morgan's laws:

```text
¬(A ∧ B)  ≡  ¬A ∨ ¬B       "not (both)" = "at least one isn't"
¬(A ∨ B)  ≡  ¬A ∧ ¬B       "not (either)" = "neither"
```

Quantifier negation is the *same idea* applied across a whole collection instead of two named
statements. Think of `∀x P(x)` as a giant AND: P holds for this one, *and* this one, *and* this one,
all the way through the domain. Negate a giant AND and De Morgan gives you a giant OR of the
negations - exactly `∃x ¬P(x)`: P fails for *some* one.

```text
∀x P(x)   is like   P(a) ∧ P(b) ∧ P(c) ∧ ...   (a big AND)
∃x P(x)   is like   P(a) ∨ P(b) ∨ P(c) ∨ ...   (a big OR)

So negating ∀ turns AND into OR  →  ∃¬
   negating ∃ turns OR into AND  →  ∀¬
```

You're not learning two new rules - you're watching one rule you already know operate at scale.

> The mechanical recipe: to negate a quantified statement, **move the `¬` inward** - every `∀`
> you pass becomes `∃`, every `∃` becomes `∀`, and the `¬` finally lands on the property at the
> end. Flip each quantifier, flip the inside.

## Nesting: now order starts to bite

So far, one quantifier at a time. Real statements often use two, and the moment they nest, a new
question appears with no analog in single quantifiers: **which one comes first?**

Watch what changes when you swap the order:

```text
∀x ∃y Loves(x, y)     "Everyone loves someone."
∃y ∀x Loves(x, y)     "There is someone whom everyone loves."
```

These are *not* the same statement, and the gap between them is enormous. The first says: pick any
person, and they have *somebody* they love - but it can be a different somebody for each person. The
second says: there's one specific person - a single celebrity, say - whom absolutely everyone loves.
The first is easy to satisfy; the second is a strong, often false, claim. Same symbols, same
predicate, reordered - completely different meaning.

A picture that makes it stick - locks and keys:

```text
∀ lock, ∃ key that opens it
   "Every lock has a key."
   → Each lock has its own key. Totally normal.

∃ key, ∀ lock it opens
   "There is one master key that opens every lock."
   → A single key for the whole building. Special, and rare.
```

Or mothers, impossible to misread once you've seen it:

```text
∀ person, ∃ mother of that person
   "Every person has a mother."          → TRUE.

∃ mother, ∀ person she is the mother of
   "There is one woman who is the mother of every person."  → FALSE.
```

Both sentences use the exact same pieces. The only difference is whether `∀` or `∃` leads - and that
difference is the difference between an obvious truth and an obvious falsehood. The mental model
that keeps it straight: **the later quantifier is allowed to depend on the earlier one.** In
`∀x ∃y`, you choose `x` first, *then* pick `y` knowing which `x` you got - so `y` can change with
`x`. In `∃y ∀x`, you commit to `y` *before* you see any `x`, so that one `y` has to work for all of
them. Order is "who has to commit first."

## For builders

You already write quantifier negation; you might not call it that.

```text
not all(checks)      ≡   any(not c for c in checks)
not any(checks)      ≡   all(not c for c in checks)
```

That's De Morgan again, in code. When you write `not all(...)`, the clearer intent is often "is
there any failure?" - `any(c is failing ...)`. Reaching for the `∃` form directly reads better and
surfaces the *counterexample* you actually care about.

The nesting trap shows up as real bugs. Compare two requirements that sound almost identical when
spoken:

```text
∀ user, ∃ session for that user     "every user has a session"
∃ session, ∀ user using it          "there is one session for all users"
```

The first is the normal world: each logged-in user gets their own session. The second is a bug you
can actually ship - one shared session object that every user reads and writes. Build the second
when you meant the first, and users start seeing each other's data; the symptom looks like haunting
nonsense until you notice the quantifier order in your design was backwards. The specification was
wrong before a single line of code was.

> ⚠️ **Swapping `∀` and `∃` silently changes the meaning.** Nothing flags an error - both
> statements parse, both are grammatical, both look reasonable in a spec doc. The only protection
> is reading the order out loud: "for every X there is *some* Y" (Y can differ per X) versus
> "there is *one* Y for every X" (one Y, shared). When a requirement involves "every" and "some"
> together, stop and pin down which one commits first.

## Recap

You can now say *no* to a quantifier correctly:

```text
¬∀x P(x)  ≡  ∃x ¬P(x)     not all pass  →  some one fails   (one counterexample)
¬∃x P(x)  ≡  ∀x ¬P(x)     none pass     →  all fail         (rule everything out)
```

It's De Morgan stretched over a domain: flip the quantifier, flip the inside, and refute a sweeping
claim with a single counterexample rather than an equal-and-opposite overclaim. And with nested
quantifiers, **order is meaning.** `∀x ∃y` lets the second choice depend on the first; `∃y ∀x`
forces one fixed witness that works for everyone. Same symbols, different worlds - in math and in
the systems you build.

That's the core of predicate logic. From here, the Logic track goes two directions: *proof*, where
you'll establish that a `∀` is true (you can't check every case) or that an `∃` exists (you produce
a witness), and *spotting fallacies*, where a surprising number of bad arguments turn out to be
quantifier mistakes in disguise - a counterexample mistaken for a counter-claim, or a "some" quietly
swapped for an "all." You now have the eyes for both.

## Open-ended exercise

A system requirement states: "Every user has exactly one primary role." Translate this
into a statement with quantifiers. Then write its negation - what would it mean for the
requirement to be *false*? Your negation should be a concrete claim a tester could check.

Three to lock it in:

```quiz
[
  {
    "q": "What is the negation of ∀x P(x)?",
    "choices": ["∀x ¬P(x)", "∃x ¬P(x)", "∃x P(x)", "¬∃x P(x)"],
    "answer": 1,
    "explain": "To deny that everything has P, you only need one thing that lacks it: ∃x ¬P(x). The ∀ flips to ∃ and the property flips to its opposite - one counterexample is enough."
  },
  {
    "q": "Someone says 'all the records have a timestamp.' What does denying that claim actually assert?",
    "choices": ["No record has a timestamp", "Some record does not have a timestamp", "Every record lacks a timestamp", "Most records have no timestamp"],
    "answer": 1,
    "explain": "'Not all X are Y' means 'some X are not Y.' One record missing its timestamp is the whole disproof - you don't have to claim every record is missing one."
  },
  {
    "q": "Which pair of statements means two genuinely different things?",
    "choices": ["∀x P(x) and P(x) ∧ ... for all x", "¬∃x P(x) and ∀x ¬P(x)", "∀x ∃y Loves(x,y) and ∃y ∀x Loves(x,y)", "¬∀x P(x) and ∃x ¬P(x)"],
    "answer": 2,
    "explain": "'Everyone loves someone' (the y can differ per person) is not 'there's someone everyone loves' (one fixed person). Swapping ∀ and ∃ changes the meaning. The other pairs are equivalences."
  }
]
```
