Day 10 — Quantifiers & Direct Proof

Updated

July 30, 2025

Day 10 — Quantifiers & Direct Proof

Day 26 — Predicates & quantifiers

Stage III · concept day
Goal: Work with predicates and a universe of discourse; use $\forall$ and $\exists$ correctly; distinguish free and bound variables; translate English carefully; negate quantified statements with $\neg\forall \equiv \exists\neg$ and $\neg\exists \equiv \forall\neg$; handle multiple variables at a single quantifier nesting depth.

Why this matters

Propositional logic cannot say “every user has a role” or “there exists a free port.” Specifications, type constraints, database integrity, and algorithm pre/postconditions are quantified. Negating “all tests pass” incorrectly is how false confidence survives in reviews. Master single-level quantifiers today; nesting order is Day 27.

Theory

Predicates and open sentences

A predicate $P(x)$ is a statement template that becomes a proposition when $x$ is fixed in a domain. Examples: $E(n)$: “$n$ is even”; $R(u)$: “user $u$ is registered.”

$E(4)$ is a proposition (true).
$E(n)$ with free $n$ is not yet a proposition.

Predicates may take several arguments: $L(x,y)$: “$x < y$”; $T(u,r)$: “user $u$ has role $r$.”

Universe of discourse

The universe (domain) $U$ is the set of values variables range over. Truth of quantified claims depends on $U$.

$\forall x\, (x > 0)$ is false in $\mathbb{Z}$, true if $U = \{1,2,3\}$.
Always state or inherit the universe.

Common universes: $\mathbb{N},\mathbb{Z},\mathbb{R}$, finite sets of IDs, strings, nodes in a graph.

Universal quantifier $\forall$

$\forall x\, P(x)$ means: for every $x \in U$, $P(x)$ is true.

False if at least one counterexample $c\in U$ has $\neg P(c)$.
True on empty universe? Vacuously true (every element—of which there are none—satisfies $P$). Rare in casual speech; remember for empty sets later.

Existential quantifier $\exists$

$\exists x\, P(x)$ means: there exists at least one $x \in U$ such that $P(x)$.

True if a witness $c$ with $P(c)$ exists.
False if $P(x)$ fails for all $x\in U$.
On empty universe: false (no witness).

Restricted quantifiers

\[\forall x \in S\, P(x) \quad\text{means}\quad \forall x\, \bigl(x\in S \rightarrow P(x)\bigr).\]

\[\exists x \in S\, P(x) \quad\text{means}\quad \exists x\, \bigl(x\in S \wedge P(x)\bigr).\]

Do not swap $\rightarrow$ and $\wedge$. “Every even integer is divisible by $2$” is $\forall n\,(E(n)\rightarrow D(n))$, not $\forall n\,(E(n)\wedge D(n))$ (the latter claims every integer is even).

Free and bound variables

An occurrence of $x$ is bound if it is in the scope of a quantifier on $x$; otherwise free.

In $\forall x\, (P(x) \rightarrow Q(y))$, $x$ is bound, $y$ is free.
The formula is a predicate in $y$, not a closed proposition, until $y$ is fixed or quantified.

Alpha renaming: $\forall x\, P(x)$ is the same claim as $\forall t\, P(t)$ if $t$ is fresh. Bound names are dummy.

Scope and parentheses

$\forall x\, P(x) \wedge Q(x)$ is ambiguous in prose. Prefer:

$(\forall x\, P(x)) \wedge Q(x)$ — $x$ free in $Q$, or
$\forall x\, \bigl(P(x) \wedge Q(x)\bigr)$ — both bound.

Write quantifier scope explicitly.

Multiple variables, single “layer”

$\forall x \forall y\, P(x,y)$ means for every pair $(x,y)$, $P$ holds. Same layer of “for all.”
$\exists x \exists y\, P(x,y)$ means some pair works.

When quantifiers are the same kind, order can be swapped:

\[\forall x \forall y\, P(x,y) \equiv \forall y \forall x\, P(x,y), \qquad \exists x \exists y\, P(x,y) \equiv \exists y \exists x\, P(x,y).\]

Mixed $\forall\exists$ vs $\exists\forall$ is Day 27—order matters.

Negation rules (critical)

\[ \begin{align*} \neg \forall x\, P(x) &\equiv \exists x\, \neg P(x),\\ \neg \exists x\, P(x) &\equiv \forall x\, \neg P(x). \end{align*} \]

Push $\neg$ through: flip quantifier, negate matrix. For restricted forms:

\[ \begin{align*} \neg \forall x\in S\, P(x) &\equiv \exists x\in S\, \neg P(x),\\ \neg \exists x\in S\, P(x) &\equiv \forall x\in S\, \neg P(x). \end{align*} \]

De Morgan for quantifiers is the infinite analogue of De Morgan for $\wedge$/$\vee$:
$\forall$ is like a big $\wedge$ over $U$; $\exists$ is like a big $\vee$.

Translating English carefully

English	Logical form (typical)
All $P$s are $Q$s	$\forall x\,(P(x)\rightarrow Q(x))$
Some $P$ is a $Q$	$\exists x\,(P(x)\wedge Q(x))$
No $P$ is a $Q$	$\forall x\,(P(x)\rightarrow \neg Q(x))$ or $\neg\exists x\,(P(x)\wedge Q(x))$
Not all $P$s are $Q$s	$\exists x\,(P(x)\wedge \neg Q(x))$
Only $P$s are $Q$s	$\forall x\,(Q(x)\rightarrow P(x))$

“Any,” “each,” “every” → $\forall$. “There is,” “at least one,” “some” → $\exists$. “Unique” → Day 27 $\exists!$.

Quantifiers and connectives (common valid patterns)

$\forall x\,(P(x) \wedge Q(x)) \equiv (\forall x\, P(x)) \wedge (\forall x\, Q(x))$.
$\exists x\,(P(x) \vee Q(x)) \equiv (\exists x\, P(x)) \vee (\exists x\, Q(x))$.
$\forall x\,(P(x) \vee Q(x))$ is weaker than $(\forall x\,P)\vee(\forall x\,Q)$—not equivalent.
$\exists x\,(P(x) \wedge Q(x))$ is stronger than $(\exists x\,P)\wedge(\exists x\,Q)$—not equivalent (witnesses may differ).

Proof obligations (preview)

To prove $\forall x\, P(x)$: let $x$ be arbitrary in $U$; prove $P(x)$.
To disprove $\forall x\, P(x)$: exhibit one counterexample.
To prove $\exists x\, P(x)$: construct/find a witness (or non-constructive existence later).
To disprove $\exists x\, P(x)$: prove $\forall x\, \neg P(x)$.

Worked examples

Example 1 — Universe matters

$U=\mathbb{Z}$: $\exists n\, (n^2 = 2)$ is false. $U=\mathbb{R}$: true ($n=\sqrt{2}$). Always fix $U$.

Example 2 — Restricted quantifier expansion

$\forall n\in\mathbb{Z}\, (2\mid n \rightarrow 2\mid n^2)$ expands to $\forall n\,(n\in\mathbb{Z} \rightarrow (2\mid n \rightarrow 2\mid n^2))$, or treat $\mathbb{Z}$ as $U$ and write $\forall n\,(2\mid n \rightarrow 2\mid n^2)$.

Example 3 — Negate “all tests pass”

Let $T(x)$: test $x$ passes, $U=$ test suite.
$\neg \forall x\, T(x) \equiv \exists x\, \neg T(x)$: some test fails.
Not “all tests fail” ($\forall x\, \neg T(x)$).

Example 4 — Negate “some server is down”

$D(s)$: server $s$ is down.
$\neg \exists s\, D(s) \equiv \forall s\, \neg D(s)$: every server is up.

Example 5 — Free vs bound

$P(y): \forall x\, (x+y=y+x)$. Here $y$ is free; for $U=\mathbb{Z}$ the statement $\forall x\,(x+y=y+x)$ is true for each fixed $y$. Closing: $\forall y\forall x\,(x+y=y+x)$.

Example 6 — Bad translation

English: “Every user has a password.”
Wrong: $\forall u\, H(u) \wedge P(u)$ if $H$ means “is user.”
Right with $U=$ all users: $\forall u\, P(u)$.
Right with $U=$ all entities: $\forall u\,(User(u)\rightarrow HasPassword(u))$.

Example 7 — Some vs all with and

$(\exists x\, P(x)) \wedge (\exists x\, Q(x))$ allows different witnesses.
$\exists x\,(P(x)\wedge Q(x))$ needs one $x$ with both.
$P=$ “is even”, $Q=$ “is odd” on $\mathbb{Z}$: left true, right false.

Example 8 — Distribute $\forall$ over $\wedge$

$\forall n\,(n\ge 0 \wedge n\le n)$ $\equiv$ $(\forall n\, n\ge 0)\wedge(\forall n\, n\le n)$—but on $\mathbb{Z}$ left is false because $n\ge 0$ fails. On $\mathbb{N}$ both sides true. Structure of $\equiv$ holds regardless.

Example 9 — No $P$ is $Q$

$\neg \exists x\,(P(x)\wedge Q(x)) \equiv \forall x\, \neg(P(x)\wedge Q(x)) \equiv \forall x\,(\neg P(x)\vee \neg Q(x)) \equiv \forall x\,(P(x)\rightarrow \neg Q(x))$.

Example 10 — Multiple same quantifiers

$\forall x \forall y\, (x+y=y+x)$ on $\mathbb{R}$: true. Same as $\forall y \forall x$.
$\exists x \exists y\, (x^2+y^2=0)$ on $\mathbb{R}$: true, witness $(0,0)$.

Example 11 — Vacuous restricted universal

$\forall x\in\emptyset\, P(x)$ is true for any $P$ (empty $\rightarrow$ product).
$\exists x\in\emptyset\, P(x)$ is false.

Example 12 — Program spec

“For every request $r$, if $r$ is authenticated then $r$ receives $200$ or $403$.”
$\forall r\, \bigl(Auth(r) \rightarrow (Ok(r) \vee Forbidden(r))\bigr)$.

Example 13 — Negate nested same-type carefully

$\neg \forall x \forall y\, P(x,y) \equiv \exists x\, \neg\forall y\, P(x,y) \equiv \exists x \exists y\, \neg P(x,y)$.
Flip each quantifier as $\neg$ moves right.

Example 14 — “Only if” with quantifiers

“A file is deleted only if it is marked trash”: $\forall f\,(Deleted(f)\rightarrow Trash(f))$.

Exercises

Let $U=\mathbb{Z}$. Truth value: $\forall n\, (n^2 \ge 0)$; $\exists n\, (n^2 < 0)$; $\exists n\, (n^2=2)$.
Translate: “Every prime greater than $2$ is odd.”
Translate: “Some integer is both even and divisible by $3$.”
Negate and simplify: $\forall x\, (P(x) \rightarrow Q(x))$.
Negate: $\exists x\, (P(x) \wedge \neg Q(x))$.
Expand $\exists n\in\mathbb{N}\, (n^2=n)$ with $\wedge$ form; is it true?
Identify free/bound: $\forall x\, (P(x,y) \rightarrow \exists y\, Q(x,y))$. Careful with the two $y$s—rewrite with safe names.
Show by counter-universe or reasoning: $\forall x\,(P\vee Q) \not\equiv (\forall x\,P)\vee(\forall x\,Q)$ with predicates on a $2$-element set.
Same for $\exists(P\wedge Q)$ vs $(\exists P)\wedge(\exists Q)$.
Write “No logged-in user is banned” in two equivalent ways.
Universe $U=\{1,2,3\}$. Expand $\forall x\, P(x)$ as a conjunction; $\exists x\, P(x)$ as a disjunction.
Negate $\forall x\in S\, \exists y\, R(x,y)$ fully (push $\neg$ all the way)—preview Day 27.
Translate: “Not every process is runnable.”
Is $\forall x\, P(x) \rightarrow \exists x\, P(x)$ always true? Discuss empty universe.
Formalize: “There is a user with no roles.”
Formalize: “Every even integer is a sum of two integers” (trivial on $\mathbb{Z}$)—write it, then specialize.
Which is stronger on nonempty $U$: $\forall x\, P(x)$ or $\exists x\, P(x)$?
Prove or disprove on $\mathbb{Z}$: $\exists n\, \forall m\, (n \le m)$.
Prove or disprove on $\mathbb{Z}$: $\forall m\, \exists n\, (n \le m)$. (Order still single insight.)
Give alpha-renaming of $\forall x \exists y\, (y > x)$ with variables $a,b$.
Translate a DB constraint: “Every order has at least one line item.”
Negate: $\exists x\, \forall y\, (x \le y)$ on $\mathbb{R}$ and state truth of original.
Write $\forall x\in A\, P(x)$ and $\exists x\in A\, P(x)$ using only unrestricted quantifiers and $\in$.
English → logic: “Any cache miss causes a fetch.”
Logic → English: $\neg\exists u\,(Admin(u)\wedge Banned(u))$.

CS connection

Preconditions/postconditions: $\forall$ inputs satisfying pre, post holds; $\exists$ path that fails is a bug report.
SQL: ALL / EXISTS / NOT EXISTS mirror quantifiers; WHERE NOT EXISTS is often $\neg\exists$.
Type systems: “for all types $T$” in generics/parametric polymorphism (awareness).
Access control: “every request has a principal” as integrity invariant.
Testing: universal claims need counterexample search; existential claims need a witness test.
Configuration: “some replica is primary” ($\exists$! often desired—Day 27).

Common pitfalls

Pitfall	What to do instead
$\forall$ with $\wedge$ for “all $P$ are $Q$”	Use $\rightarrow$ for restricted universals
$\exists$ with $\rightarrow$	Use $\wedge$: $\exists x\,(P\wedge Q)$
Negating $\forall$ to $\forall\neg$	$\neg\forall \equiv \exists\neg$
Ignoring universe	State $U$ or $x\in S$
Free variables left in “theorems”	Quantify or instantiate
Same witness assumed for two $\exists$	Combine into one $\exists$ only if joint property
Scope ambiguity	Parenthesize quantifier bodies

Checkpoint

Define predicate, universe, $\forall$, $\exists$
Expand restricted $\forall$/$\exists$ correctly
Mark free vs bound in a mixed formula
Negate $\forall$ and $\exists$ statements fluently
Translate “all / some / no / not all”
Know when $\forall$ distributes over $\wedge$ and when $\exists$ over $\vee$
Give witness vs counterexample proof obligations
Exercises done or logged

Two takeaways:

Deep dive — quantifiers as big meet/join

If $U=\{a_1,\ldots,a_n\}$ is finite,
\[\forall x\, P(x) \;\equiv\; P(a_1)\wedge\cdots\wedge P(a_n), \qquad \exists x\, P(x)\;\equiv\; P(a_1)\vee\cdots\vee P(a_n).\]
De Morgan for quantifiers is then ordinary De Morgan on a long conjunction/disjunction. On infinite $U$, the same idea holds but the conjunction is infinite—still the right mental model for negation and for restricted quantifiers.

Order of rewriting restricted forms

\[\neg\forall x\in S\, P(x) \equiv \neg\forall x\,(x\in S\rightarrow P(x)) \equiv \exists x\, \neg(x\in S\rightarrow P(x)) \equiv \exists x\,(x\in S \wedge \neg P(x)).\]
Do not “flip $\in S$.” The restriction stays existential with $\wedge$.

Common valid/invalid quantifier–connective moves

Claim	Status
$\forall x(P\wedge Q)\equiv(\forall x P)\wedge(\forall x Q)$	Valid
$\exists x(P\vee Q)\equiv(\exists x P)\vee(\exists x Q)$	Valid
$\forall x(P\vee Q)\equiv(\forall x P)\vee(\forall x Q)$	Invalid
$\exists x(P\wedge Q)\equiv(\exists x P)\wedge(\exists x Q)$	Invalid
$\forall x(P\rightarrow Q)\Rightarrow ((\forall x P)\rightarrow(\forall x Q))$	Valid (careful proof)
converse of previous	Invalid in general

More worked examples

Example 15 — Empty domain
On $U=\emptyset$: $\forall x\, P$ true, $\exists x\, P$ false, for any $P$.

Example 16 — Translate “only admins can delete”
$\forall u\,(Delete(u)\rightarrow Admin(u))$.

Example 17 — Negate “every even is sum of two primes” (Goldbach form)
$\exists n\,(Even(n)\wedge n>2 \wedge \neg\exists p,q\,(Prime(p)\wedge Prime(q)\wedge p+q=n))$
(status open for all even $n$—here only practice negation).

Example 18 — Free variable bug
Claim written $\forall x\, P(x,y)$ as a “theorem” still depends on $y$ unless quantified.

Additional exercises

Expand and negate $\forall x\in\mathbb{Z}\, (x>0 \rightarrow x^2>0)$.
Give a universe where $\forall x(P\vee Q)$ true but $(\forall x P)\vee(\forall x Q)$ false.
Formalize: “There is exactly one empty string” without $\exists!$ using length.
SQL-flavored: negate NOT EXISTS (SELECT 1 FROM t WHERE bad(t)) in logic.
Prove carefully $\forall x(P\rightarrow Q)$ and $\forall x P$ imply $\forall x Q$.

Synthesis

Single-layer quantifiers are the bridge from propositional logic to real specifications. Everything you do with nested quantifiers (Day 27), proofs (Days 28–32), and set theory (Stage IV) still rests on: fix a universe, expand restricted forms correctly, push negations by flipping quantifiers, and know whether you need a witness or a counterexample.

Translation → negation → proof duty pipeline

English → formal. Identify “all / some / no / not all / only.”
Expand restrictions. $\forall x\in S$ uses $\rightarrow$; $\exists x\in S$ uses $\wedge$.
Negate if disproving or writing the dual claim. Flip each quantifier; push $\neg$ onto the matrix.
Choose obligation. Prove $\forall$ by arbitrary $x$; disprove $\forall$ by one counterexample; prove $\exists$ by a witness; disprove $\exists$ by proving $\forall\neg$.

More worked examples

Example 19 — “Only $P$s are $Q$s” vs “all $P$s are $Q$s.”
Only: $\forall x\,(Q(x)\rightarrow P(x))$. All: $\forall x\,(P(x)\rightarrow Q(x))$. These are converses—neither implies the other.
Counter-models: $U=\{1,2\}$, $P=\{1\}$, $Q=\{1,2\}$ makes “all $P$ are $Q$” true and “only $P$ are $Q$” false.

Example 20 — Spec that looks universal but is existential.
“The system has a recovery path” is $\exists$ path, not $\forall$ paths. Formalize: $\exists p\, Recovery(p)$. Negation: every path fails recovery.

Example 21 — Finite expansion as a proof tool.
On $U=\{a,b,c\}$, $\forall x\, P(x)$ is $P(a)\wedge P(b)\wedge P(c)$. To prove it, prove three propositions. To disprove, falsify one. Same discipline scales to infinite $U$ with an arbitrary-element proof instead of a finite $\wedge$-chain.

Example 22 — When $\forall x(P\rightarrow Q)$ and $(\forall x P)\rightarrow(\forall x Q)$ differ in flavor.
The first is “every individual that is $P$ is $Q$.” The second is “if everything is $P$, then everything is $Q$.” On a nonempty universe, $\forall x(P\rightarrow Q)$ implies the second, but the second can hold vacuously when $\forall x P$ is false even if some $P$ fails to be $Q$.

Extra exercises (synthesis)

Pipeline practice: translate “No expired token is accepted,” negate it, then state how you would prove the original (arbitrary token that is expired…).
On $U=\{0,1\}$, invent predicates making $\exists x(P\wedge Q)$ false while $(\exists x P)\wedge(\exists x Q)$ true.
Expand $\forall n\in\mathbb{N}\, (n\ge 2 \rightarrow \exists p\,(Prime(p)\wedge p\mid n))$ and identify free vs bound names.
Explain in two sentences why empty-universe $\forall$ is true and empty-universe $\exists$ is false.
Write a four-row “mini truth table” of proof duties: prove/disprove $\forall$ and $\exists$.

Self-check before Day 27

Can you expand and negate restricted $\forall$/$\exists$ without swapping $\rightarrow$ and $\wedge$?
Can you give a $2$-element counter-model to illicit distribution of $\forall$ over $\vee$?
Can you mark free and bound variables after $\alpha$-renaming collisions?

If any answer is no, rework Examples 3–7 and Exercises 4–9 cold before nesting quantifiers.

Tomorrow

Day 27 — Nested quantifiers. Order matters; $\forall\exists$ vs $\exists\forall$; unique existence $\exists!$; witnesses; sorting and database English.

Day 27 — Nested quantifiers

Stage III · concept day
Goal: Read and write nested quantifiers; prove that order matters for mixed $\forall$/$\exists$; use witnesses and dependence; introduce unique existence $\exists!$; apply restricted nested quantifiers; translate sorting/database English carefully.

Why this matters

“For every request there is a server that handles it” is not “there is a server that handles every request.” One is load-balanced routing; the other is a single global bottleneck (or a fixed handler). Distributed systems, SQL, and algorithm specs live in nested quantifiers. Getting order wrong is a semantic bug, not a typo.

Theory

Reading nested quantifiers left to right

Quantifiers bind from the outside in:

$\forall x \exists y\, P(x,y)$: for each $x$, you may choose a $y$ (possibly depending on $x$) with $P(x,y)$.
$\exists y \forall x\, P(x,y)$: there is one $y$ that works for all $x$ simultaneously.

Think of a game: $\forall$ is adversary choosing $x$; $\exists$ is you responding with $y$. In $\forall x\exists y$, you see $x$ before choosing $y$. In $\exists y\forall x$, you must commit to $y$ first.

Order matters: inequivalence

Theorem (pattern). In general
\[\forall x \exists y\, P(x,y) \;\not\equiv\; \exists y \forall x\, P(x,y).\]

Proof of inequivalence (standard witness domain).
Let $U=\mathbb{Z}$ and $P(x,y): y > x$.

$\forall x \exists y\, (y > x)$ is true: for $x$, take $y=x+1$.
$\exists y \forall x\, (y > x)$ is false: no integer is $> $ all integers.

Since one is true and one false, the forms are not equivalent. $\square$

When the matrix is independent of order in special cases, equivalence can hold—but never assume it.

Same quantifier, order free

As on Day 26:

\[\forall x \forall y\, P \equiv \forall y \forall x\, P, \qquad \exists x \exists y\, P \equiv \exists y \exists x\, P.\]

Dependence and Skolem intuition (awareness)

From $\forall x \exists y\, P(x,y)$, classical logic allows a function $f$ with $\forall x\, P(x,f(x))$ (Skolem function)—“$y$ as a function of $x$.” In programming terms: $y = f(x)$ is computed from $x$. The $\exists y\forall x$ form is a constant Skolem function.

Unique existence $\exists!$

\[\exists! x\, P(x)\]
means: there exists a unique $x$ such that $P(x)$. Formally:

\[\exists x\, \Bigl(P(x) \wedge \forall z\, \bigl(P(z) \rightarrow z = x\bigr)\Bigr),\]
or equivalently

\[\exists x\, P(x) \;\wedge\; \forall y \forall z\, \bigl((P(y)\wedge P(z)) \rightarrow y=z\bigr).\]

Examples: $\exists! n\in\mathbb{N}\, (n^2=0)$ if $0\in\mathbb{N}$; unique empty string of length $0$; unique identity element in a group (when it exists).

Restricted nested quantifiers

\[\forall x\in A\, \exists y\in B\, R(x,y)\]
means $\forall x\, \bigl(x\in A \rightarrow \exists y\,(y\in B \wedge R(x,y))\bigr)$.

\[\exists y\in B\, \forall x\in A\, R(x,y)\]
means $\exists y\, \bigl(y\in B \wedge \forall x\,(x\in A \rightarrow R(x,y))\bigr)$.

Negating nested quantifiers

Push $\neg$ inward, flipping each quantifier:

\[\neg \forall x \exists y\, P(x,y) \equiv \exists x \forall y\, \neg P(x,y).\]

\[\neg \exists y \forall x\, P(x,y) \equiv \forall y \exists x\, \neg P(x,y).\]

Sorting and order examples

Let $A[1..n]$ be an array of numbers (universe of indices $\{1,\ldots,n\}$).

Sorted nondecreasing: $\forall i \forall j\, \bigl(1\le i < j \le n \rightarrow A[i] \le A[j]\bigr)$, or adjacent form $\forall i\, (1\le i < n \rightarrow A[i]\le A[i+1])$ (equivalent for total orders on values).
Exists inversion: $\exists i\, (A[i] > A[i+1])$.
Maximum at index $k$: $\forall i\, (A[i] \le A[k])$.
Unique maximum value: more care—unique index vs unique value.

Database / systems English

English	Nested form
Every student takes some course	$\forall s \exists c\, Takes(s,c)$
Some course is taken by every student	$\exists c \forall s\, Takes(s,c)$
Every student takes every course	$\forall s \forall c\, Takes(s,c)$
Some student takes some course	$\exists s \exists c\, Takes(s,c)$
Every key maps to exactly one value	$\forall k \exists! v\, Maps(k,v)$ (function)
There is a primary replica for each shard	$\forall s \exists r\, Primary(s,r)$
There is one coordinator for all nodes	$\exists c \forall n\, Coordinates(c,n)$

Alternation depth

Number of switches between $\forall$ and $\exists$ along the prefix measures quantifier alternation. More alternations → harder for humans and for many automated solvers. Awareness: $\forall\exists\forall$ specs are easy to misread.

Proving nested statements

Claim	Strategy
$\forall x \exists y\, P(x,y)$	Fix arbitrary $x$; construct $y=y(x)$; prove $P$
$\exists y \forall x\, P(x,y)$	Exhibit one $y$; let $x$ be arbitrary; prove $P$
$\neg \forall x \exists y\, P$	Find one $x$ such that $\forall y\, \neg P(x,y)$
$\exists! x\, P(x)$	Existence + uniqueness (often uniqueness by assuming two and equating)

Worked examples

Example 1 — Classic $y>x$

On $\mathbb{Z}$: $\forall x\exists y\,(y>x)$ true; $\exists y\forall x\,(y>x)$ false—as in the theorem proof.

Example 2 — Both true

$P(x,y): x+y=y+x$ on $\mathbb{R}$. Both $\forall x\exists y$ and $\exists y\forall x$ and $\forall x\forall y$ hold (any $y$ works for all $x$).

Example 3 — Both false

$P(x,y): y^2 = x$ on $\mathbb{Z}$. $\forall x\exists y$ false ($x=2$). $\exists y\forall x$ false.

Example 4 — Function as $\forall\exists!$

“$f$ is a function from $A$ to $B$” includes: $\forall a\in A\, \exists! b\in B\, \bigl((a,b)\in f\bigr)$ when $f$ is a set of pairs (Day 41+). Nested uniqueness.

Example 5 — Negation practice

Negate $\forall \varepsilon > 0\, \exists N\, \forall n\ge N\, (|a_n - L| < \varepsilon)$ (limit definition).
$\exists \varepsilon > 0\, \forall N\, \exists n\ge N\, (|a_n-L|\ge \varepsilon)$.
“There is a fixed error tolerance that is violated infinitely often.”

Example 6 — Sorting adjacent vs global

For real arrays, $\forall i\, A[i]\le A[i+1]$ implies $\forall i<j\, A[i]\le A[j]$ by induction on $j-i$ (Day 31). Nested $\forall i\forall j$ is the spec; adjacent is the loop check.

Example 7 — SQL mental model

FOR ALL students EXISTS enrollment row with that student_id. Different from one course_id appearing in all enrollments.

Example 8 — Unique existence of identity

On $(\mathbb{Z},+)$, $\exists! e\, \forall x\, (x+e=x)$: $e=0$. Uniqueness: if $e,e'$ both identities, $e=e+e'=e'$.

Example 9 — Dependence

$\forall x \exists y\, (x\cdot y = 1)$ on $\mathbb{R}\setminus\{0\}$: true, $y=1/x$.
$\exists y \forall x\, (x\cdot y = 1)$: false. Same matrix, different dependence.

Example 10 — Empty outer set

$\forall x\in\emptyset\, \exists y\, P(x,y)$ is vacuously true.
$\exists y\, \forall x\in\emptyset\, P(x,y)$ is true for any $y$ if $P$ has no constraint—vacuous inner $\forall$. Subtle; track empty domains.

Example 11 — Friends and strangers (structure)

$\forall u \exists v\, Friend(u,v)$: no isolated person (if $v\neq u$ required, add $v\neq u$).
$\exists v \forall u\, Friend(u,v)$: someone friends with everyone (celebrity).

Example 12 — Array maximum

$\exists k\, \forall i\, (A[i] \le A[k])$ asserts a maximum exists (true for nonempty finite real arrays). Constructive: scan and keep best index.

Example 13 — Disprove $\exists\forall$ with adversary

To refute $\exists y\forall x\, P(x,y)$: for every candidate $y$, find an $x_y$ breaking $P$. That is $\forall y \exists x\, \neg P$.

Example 14 — Compose restrictions

$\forall u\in Users\, \exists r\in Roles\, Has(u,r)$ vs $\exists r\in Roles\, \forall u\in Users\, Has(u,r)$: “role per user” vs “one global role for all users.”

Exercises

On $\mathbb{R}$, truth values of $\forall x\exists y\,(xy=1)$ and $\exists y\forall x\,(xy=1)$. Careful at $0$.
Restrict to $\mathbb{R}\setminus\{0\}$ and re-evaluate both.
Prove inequivalence of $\forall\exists$ vs $\exists\forall$ with $P(x,y): y = x^2$ on $\mathbb{R}$? Check carefully whether both true/false.
Let $P(x,y): y^2 = x$ on $\mathbb{R}$. Truth of $\forall x\exists y$ and $\exists y\forall x$.
Negate fully: $\forall x \exists y \forall z\, Q(x,y,z)$.
Translate: “Every email is stored on some server.”
Translate: “There is a server that stores every email.”
Formalize unique primary key: each row id appears once.
Write $\exists! n\, (n>0 \wedge n<2)$ on $\mathbb{Z}$ and prove it.
Array $A[1..n]$: formalize “strictly increasing.”
Formalize “$A$ has a duplicate value.”
On $\mathbb{N}$, is $\forall m \exists n\, (n > m)$ true? Is $\exists n \forall m\, (n > m)$ true?
Give Skolem-style $f$ for $\forall x\exists y\,(y>x)$ on $\mathbb{Z}$.
Students/courses: write all four $\forall/\exists$ combinations for $Takes(s,c)$ and one English each.
Prove uniqueness part: if $e,e'$ are additive identities on $\mathbb{Z}$, then $e=e'$.
Negate $\exists! x\, P(x)$ into a form without $\exists!$ (two failure modes: none or $\ge 2$).
Does $\forall x\forall y\, P \equiv \forall y\forall x\, P$ always? Yes/no + one sentence.
Limit-style: write “$a_n$ does not converge to $L$” by negating the $\varepsilon$-$N$ definition.
Formalize: “For every shard there is a unique primary.”
True or false on nonempty finite $U$: $\exists y\forall x\, R(x,y)$ implies $\forall x\exists y\, R(x,y)$. Prove or counterexample.
Sorting: prove from adjacent inequalities $A[1]\le A[2]\le\cdots\le A[n]$ that $A[1]\le A[n]$ (short chain).
Database: “No two users share an email” as a quantified uniqueness statement.
Find $P$ on $\{1,2\}$ such that $\forall x\exists y\,P$ true but $\exists y\forall x\,P$ false.
Express “$f$ is surjective” from $A$ to $B$ with nested quantifiers (preview Day 41).
Express “$f$ is injective” with quantifiers over $A$.

CS connection

Load balancing vs single leader: $\forall\exists$ vs $\exists\forall$ handlers.
SQL correlated subqueries implement $\forall x\exists y$ patterns; uncorrelated often look like $\exists$ once.
API gateways: “each tenant has a config” vs “one global config.”
Time complexity specs: $\forall n\exists c\, T(n)\le c\cdot f(n)$ is big-O shape (Stage VIII).
Consensus: “there exists a value decided by all nodes” is $\exists v\forall n\, Decided(n,v)$ patterns.
Sorting correctness proofs use nested $\forall$ over indices.

Common pitfalls

Pitfall	What to do instead
Swapping $\forall\exists$ freely	Check dependence; invent a counter-model
Reading quantifiers right-to-left only	Read left-to-right as a game
Forgetting $\exists!$ splits into existence + uniqueness	Prove both parts
Negating only the outer quantifier	Flip each as $\neg$ moves in
Using same witness for every $x$ in a $\forall\exists$ proof	$y$ may depend on $x$
Vacuous truths on empty sets	Track empty $A$ in $\forall x\in A$
Adjacent sorted check without justifying global	Induction for full $\forall i<j$

Checkpoint

Explain $\forall x\exists y$ vs $\exists y\forall x$ in English and symbols
Prove inequivalence with a concrete $P$ and domain
Negate a triple nested quantifier string
Write and expand $\exists!$
Translate one DB/systems sentence two ways (swapped order)
Formalize a sorted-array property
Prove a small $\forall\exists$ claim by constructing $y(x)$
Exercises done or logged

Two takeaways:

Deep dive — prenex form (awareness)

Many formulas can be rewritten with all quantifiers in a prefix and a quantifier-free matrix (prenex normal form), e.g.
$(\forall x\, P(x)) \rightarrow (\exists y\, Q(y))$ becomes carefully quantified after rewriting $\rightarrow$ as $\vee$ and pushing quantifiers—variable capture is the danger. Awareness: automated solvers love prenex/CNF; humans should parenthesize scopes first.

Dependence table

Form	$y$ may depend on $x$?	English
$\forall x\exists y$	Yes	“for each $x$, some $y_x$”
$\exists y\forall x$	No (one $y$)	“one $y$ for all $x$”
$\forall x\forall y$	N/A	all pairs
$\exists x\exists y$	N/A	some pair

Sorting proofs need quantifiers

Adjacent: $\forall i\in\{1,\ldots,n-1\},\; A[i]\le A[i+1]$.
Global: $\forall i\forall j\,(i\le j \rightarrow A[i]\le A[j])$.
Prove adjacent $\Rightarrow$ global by induction on $j-i$ (Day 31)—state both forms on exams.

More worked examples

Example 15 — Unique root
$\exists! x\in\mathbb{R}\, (2x+3=0)$: existence $x=-3/2$; uniqueness from injection of $x\mapsto 2x+3$.

Example 16 — Negate function property
Negate $\forall a\exists! b\, F(a,b)$ (functional graph):
$\exists a\, \bigl(\neg\exists b\, F(a,b) \;\lor\; \exists b_1\exists b_2\,(F(a,b_1)\wedge F(a,b_2)\wedge b_1\neq b_2)\bigr)$.

Example 17 — Database
“Every order has a unique customer” $\forall o \exists! c\, Owns(o,c)$.

Example 18 — Swap same quantifiers with matrix care
$\forall x\forall y\, (x\le y \vee y\le x)$ on $\mathbb{R}$ true; order of $\forall$ irrelevant.

Additional exercises

Prove on $\mathbb{N}$ that $\forall m\exists n\,(n=m+m)$ and that $\exists n\forall m\,(n=m+m)$ is false.
Formalize surjectivity and injectivity of $f:A\to B$ (Day 41 preview) and negate both.
Give English for $\exists s\forall t\, (Sent(s,t)\rightarrow Delivered(t))$.
Can $\forall x\exists y\, P$ and $\exists y\forall x\, P$ both be true for nontrivial $P$? Give $P$.
Array: formalize “exactly one maximum index” (unique argmax).

Extended practice workshop

Order games (true/false on given $U$)

For each $P$, evaluate $\forall x\exists y\,P$ and $\exists y\forall x\,P$ on $\mathbb{Z}$ unless noted:

$y=x+1$
$y>x$
$xy=0$
$y^2=x$ on $\mathbb{R}$
$y^2=x$ on $\mathbb{Z}$
$x+y=y+x$

Translations both ways

7–10. Write both $\forall\exists$ and $\exists\forall$ readings for: servers/emails; students/courses; shards/primaries; keys/values.

Negation drills

$\forall\varepsilon>0\,\exists\delta>0\,\forall x\,(|x-a|<\delta\rightarrow|f(x)-L|<\varepsilon)$
$\forall u\exists r\forall p\,(HasRole(u,r)\rightarrow Perm(r,p))$
$\exists! n\, P(n)$ to a $\neg$ form with two failure modes.

Proof drills

Prove $\forall x\exists y\,(y=2x)$ on $\mathbb{Z}$ by constructing $y$.
Disprove $\exists y\forall x\,(y=2x)$ on $\mathbb{Z}$.
Prove uniqueness of additive identity on $\mathbb{Z}$.

Sorting/database

Adjacent sorted $\Rightarrow$ write global form.
“Exactly one admin” as $\exists!$.
“No two users share email” without $\exists!$.
Array has a duplicate—quantifiers.

Game metaphor card

$\forall$ = adversary moves; $\exists$ = you respond.
If $\exists$ is outside, you move first and must commit.

Tomorrow

Day 28 — Direct proof. Structure of “if $P$ then $Q$”; even/odd and divisibility templates; biconditionals both ways; choosing good definitions.

Day 28 — Direct proof

Stage III · concept day
Goal: Structure a direct proof of $P\rightarrow Q$; prove even/odd and divisibility claims; unpack definitions; prove biconditionals in both directions; choose definitions that make the algebra work.

Why this matters

Direct proof is the default tool: assume the hypothesis, unfold definitions, chain equalities/implications, conclude the goal. Most correctness arguments for arithmetic properties, invariant maintenance steps, and “if pre then post” lemmas are direct. Without a clean template, write-ups ramble and hide gaps.

Theory

What a proof is (working contract)

A proof is a finite sequence of statements, each a premise, a definition, a logical consequence of earlier statements, or a cited theorem, ending at the claim. Audience: a competent peer who may challenge any unjustified leap.

Direct proof of $P \rightarrow Q$

Template:

State the claim clearly (quantifiers explicit).
Assume $P$ (for arbitrary objects named in $\forall$).
Unpack definitions in $P$.
Reason with algebra, known theorems, earlier lemmas.
Pack the definition of $Q$.
Conclude $Q$, hence $P\rightarrow Q$. Discharge the assumption.

For $\forall x\,(P(x)\rightarrow Q(x))$: fix arbitrary $x$, assume $P(x)$, prove $Q(x)$.

Definitions to own (parity)

Let $n\in\mathbb{Z}$.

$n$ is even iff $\exists k\in\mathbb{Z}\, (n = 2k)$.
$n$ is odd iff $\exists k\in\mathbb{Z}\, (n = 2k+1)$.

These are existentially packed. Direct proofs often: assume even, choose a witness $k$, manipulate, exhibit a witness for the conclusion.

Definitions to own (divisibility)

For $a,b\in\mathbb{Z}$, $a \mid b$ (“$a$ divides $b$”) iff $\exists m\in\mathbb{Z}\, (b = a m)$.
$a$ is a divisor of $b$; $b$ is a multiple of $a$.

Choosing good definitions

Equivalent definitions must be used consistently. Prefer the form that matches the algebra:

Even as $2k$ helps products and sums.
Sometimes $n \equiv 0 \pmod{2}$ (Day 5/73 family) is cleaner for modular reasoning—same idea.

Biconditional proofs

To prove $P \leftrightarrow Q$, prove both:

$P \rightarrow Q$ (⇒ direction),
$Q \rightarrow P$ (⇐ direction).

Label directions. Do not assume both at once.

“If and only if” via chain

Sometimes $P \Leftrightarrow Q \Leftrightarrow R$ by a chain of equivalences (each step iff). Valid when every step is reversible. One-directional chains only prove one arrow.

Common direct-proof patterns

Pattern	Skeleton
Parity of sum/product	Expand $2k$, $2m+1$ forms
Divisibility preserve	$b=am$, $c=an$ ⇒ linear combo
Equality of numbers	Transform expression
Subset-style (later)	element chase
From inequality hyp	algebraic rearrangement with justified steps

What direct proof is not

Not proof by example (“true for $n=3$”).
Not proof by converse (proving $Q\rightarrow P$ when you needed $P\rightarrow Q$).
Not assuming $Q$ mid-stream without derivation.

Quantifiers in the write-up

Arbitrary but fixed: “Let $n$ be an arbitrary even integer.”
Witnesses: “So $n=2k$ for some $k\in\mathbb{Z}$.”
Exhibit: “Thus $n^2 = 2(2k^2)$, so $n^2$ is even with witness $2k^2$.”

Lemmas and structure

Factor repeated algebra as a lemma (e.g. product of evens is even) and cite it. Large proofs are trees of direct lemmas.

Worked examples

Example 1 — Even square

Claim. If $n$ is even, then $n^2$ is even.

Proof. Assume $n$ even. Then $n=2k$ for some $k\in\mathbb{Z}$.
$n^2 = (2k)^2 = 4k^2 = 2(2k^2)$.
So $n^2 = 2\cdot m$ with $m=2k^2\in\mathbb{Z}$. Hence $n^2$ is even. $\square$

Example 2 — Odd square

Claim. If $n$ is odd, then $n^2$ is odd.

Proof. $n=2k+1$ ⇒ $n^2 = 4k^2+4k+1 = 2(2k^2+2k)+1$, odd. $\square$

Example 3 — Sum of evens

Claim. If $a,b$ even then $a+b$ even.

Proof. $a=2k$, $b=2m$ ⇒ $a+b=2(k+m)$. $\square$

Example 4 — Divisibility transitive

Claim. If $a\mid b$ and $b\mid c$ then $a\mid c$.

Proof. $b=as$, $c=bt$ for some $s,t\in\mathbb{Z}$.
$c = (as)t = a(st)$, so $a\mid c$. $\square$

Example 5 — Linear combination

Claim. If $a\mid b$ and $a\mid c$ then $a\mid (bx+cy)$ for all $x,y\in\mathbb{Z}$.

Proof. $b=am$, $c=an$ ⇒ $bx+cy = a(mx+ny)$. $\square$

Example 6 — Biconditional parity

Claim. $n$ even iff $n^2$ even. (One direction Example 1; converse often by contrapositive Day 29—or cases.)

Direct-ish converse via cases: if $n$ odd then $n^2$ odd (Ex. 2), so if $n^2$ even, $n$ cannot be odd, hence even (law of excluded middle on parity). Full case hygiene is Day 30.

Example 7 — If divides then divides square

Claim. If $a\mid b$ then $a\mid b^2$.

Proof. $b=ak$ ⇒ $b^2 = a^2 k^2 = a(ak^2)$. $\square$

Example 8 — Unpack carefully

Claim. If $n\mid m$ and $n>0$, $m>0$, then $n \le m$.

Proof. $m = nq$ with $q\in\mathbb{Z}$. Since $m>0$, $n>0$, must have $q \ge 1$ (if $q\le 0$ then $m\le 0$). Thus $m = nq \ge n\cdot 1 = n$. $\square$

Example 9 — Algebraic identity as direct proof

Claim. For all $n\in\mathbb{Z}$, $(n+1)^2 - n^2 = 2n+1$.

Proof. Expand left: $n^2+2n+1-n^2=2n+1$. $\square$
(Universal claim proved by arbitrary $n$ and algebra.)

Example 10 — Product of odds

Claim. If $a,b$ odd then $ab$ odd.

Proof. $a=2k+1$, $b=2m+1$ ⇒ $ab = 4km+2k+2m+1 = 2(\cdots)+1$. $\square$

Example 11 — Spec style

Claim. If a buffer’s size $n$ is even and we split into two equal halves, each half has integer length $n/2$.

Proof. $n=2k$ ⇒ half length $k\in\mathbb{Z}$. $\square$
(Trivial but matches how systems proofs start.)

Example 12 — Two directions labeled

Claim. For $n\in\mathbb{Z}$, $3\mid n$ iff $3\mid 2n$ is false as biconditional? Check: if $3\mid n$ then $3\mid 2n$ (direct). Converse: $3\mid 2n$ does not imply $3\mid n$ (counterexample $n=1$ fails $3\mid 2$; actually $n=3$ works both. Counterexample for converse: need $3\mid 2n$ but not $3\mid n$. Since $3$ prime, $3\mid 2n$ ⇒ $3\mid n$. So on integers with Euclid’s lemma it holds—use Day 71+ or accept via prime property. Alternative claim: $4\mid 2n$ not iff $4\mid n$ ($n=2$: $4\mid 4$ but $4\nmid 2$). Use that.

Claim. $4\mid 2n$ does not imply $4\mid n$. Counterexample $n=2$. Direct proof of ⇒ for $2\mid n \Rightarrow 4\mid 2n$? If $n=2k$, $2n=4k$. Yes.

Example 13 — From hypothesis equality

If $a=b$, then $a+c=b+c$ (add same to both sides)—direct from properties of equality (substitution).

Example 14 — Rational closed under multiplication (sketch)

If $x=p/q$, $y=r/s$ with $q,s\neq 0$, then $xy = (pr)/(qs)$ with $qs\neq 0$. Direct from definition of $\mathbb{Q}$.

Exercises

Write full proofs. Quantify variables.

If $n$ is even, then $n+2$ is even.
If $n$ is odd, then $n+1$ is even.
If $a\mid b$ and $a\mid c$, then $a\mid (b+c)$.
If $a\mid b$, then $a\mid (-b)$.
If $n$ is even, then $3n$ is even.
If $a$ and $b$ are even, then $ab$ is even.
Prove: for all $n\in\mathbb{Z}$, $n(n+1)$ is even. (Hint: cases on parity—or note consecutive.)
If $5\mid n$, then $5\mid n^2$.
Prove transitivity of $\mid$ again in your own words.
If $a\mid b$ and $b\neq 0$, then $|a| \le |b|$. (Careful with negatives.)
Prove: $n$ odd iff $n=2k+1$ for some $k$—if this is your definition, instead prove $n$ odd iff $n-1$ even.
Show if $a\mid b$ and $a\mid c$ then $a^2 \mid bc$ need not hold? Or prove $a\mid b \Rightarrow a^2 \mid b^2$.
Prove $(n+1)^3 - n^3 = 3n^2+3n+1$ by expansion.
If $x$ and $y$ are rational, $x+y$ is rational (direct from definitions).
Prove: if $n\mid m$ and $m\mid n$ then $|n|=|m|$ for integers.
Biconditional: $n$ even iff $n+1$ odd. Both directions.
If $a\mid b$ and $c\mid d$ then $ac\mid bd$.
Disprove by counterexample: if $a\mid bc$ then $a\mid b$ or $a\mid c$.
Prove: sum of an even and an odd is odd.
Write a direct proof that for all $n\ge 1$, the number of edges in a path of $n$ nodes is $n-1$ (define path graph cleanly in one sentence).
If $2\mid n$ and $3\mid n$ then $6\mid n$ (may use $\mathrm{lcm}$ or explicit $n=2a=3b$ and solve—or wait for number theory; try $n=6k$ construction from Bézout awareness).
Prove: if $n=2k$ then $n^2 \equiv 0 \pmod 4$.
Direct proof from definition: $\forall n\in\mathbb{Z}\, (n \le n)$.
Prove if $A\subseteq B$ and $B\subseteq C$ then $A\subseteq C$ (element chase—sets Day 35 preview).
State and prove a small lemma you invent about odd integers (e.g. difference of odds is even).

CS connection

Spec lemmas: if request is authorized ($P$), then status is not $401$ ($Q$)—direct from auth module definition.
Invariant step: assume invariant holds before iteration, show after—direct proof body (Day 32).
Parity bits and alignment: “if size even then can pair bytes” is Example 11-shaped.
Divisibility in paging / blocks: block size divides segment length.
Proof reviews: demand unpacked definitions the same way code reviews demand unpacked invariants.
Automated provers still need human-structured direct lemmas for readable assurance cases.

Common pitfalls

Pitfall	What to do instead
Proof by example	Arbitrary $n$, not $n=4$
Assuming the conclusion	Assume only $P$
Forgetting to exhibit witnesses	Produce $k$ explicitly
Circular use of the claim	Only prior lemmas/definitions
One direction for iff	Prove both ⇒ and ⇐
Hidden quantifier on $k$	“for some $k\in\mathbb{Z}$”
Division by zero in rational proofs	Track denominators $\neq 0$
Using “clearly” for a multi-step gap	Write the steps

Checkpoint

Write the direct-proof template from memory
Prove even ⇒ even square without notes
Prove a divisibility claim with witnesses
Complete one full biconditional
Spot a proof-by-example fallacy
Unpack at least two definitions in a proof
Exercises done or logged

Two takeaways:

Deep dive — definition hygiene

Every direct proof is only as good as its definitions. Before writing:

Write the claim with quantifiers.
Expand every keyword (even, divides, rational, subset, …).
Note what a witness looks like for existential parts of the hypothesis.
Note what witness you must build for the conclusion.

Parity closed-form toolkit

Object	Algebraic form
Even $n$	$2k$
Odd $n$	$2k+1$
Even + even	even
Odd + odd	even
Even + odd	odd
Even $\times$ anything	even
Odd $\times$ odd	odd

Prove each once; cite thereafter.

Divisibility toolkit

$a\mid a$, $a\mid 0$, $1\mid a$ for all $a$.
If $a\mid b$ and $b\mid c$ then $a\mid c$.
If $a\mid b$ and $a\mid c$ then $a\mid (bx+cy)$.
If $a\mid b$ and $b\neq 0$ then $|a|\le|b|$.

More worked examples

Example 15 — Difference of squares
If $n$ odd then $n^2-1$ divisible by $8$: $n=2k+1$, $n^2-1=4k(k+1)$ and $k(k+1)$ even so extra factor $2$.

Example 16 — Rational sum
Direct from $p/q+r/s=(ps+qr)/(qs)$.

Example 17 — Spec lemma
If buffer length $n$ divisible by $4$, then number of 4-byte words is $n/4\in\mathbb{Z}$.

Example 18 — Biconditional trap
$2\mid n$ iff $2\mid n^2$ is true (both directions)—prove carefully; do not assume the converse of a random divisibility.

Additional exercises

Prove: if $n$ odd then $n^2\equiv 1\pmod 8$.
Prove: $a\mid b$ iff $a\mid -b$.
Prove both directions: $n$ odd iff $n^2$ odd.
If $3\mid n$ and $3\mid m$ then $3\mid (n^2+m^2)$—direct.
Write a graded rubric: what must appear in a full direct proof of “even $\Rightarrow$ even square.”

Extended practice workshop

Parity proofs (full write-ups)

Even + even = even
Odd + odd = even
Even + odd = odd
Even × anything = even
Odd × odd = odd
Even ⇒ even square
Odd ⇒ odd square
$n(n+1)$ always even

Divisibility proofs

Transitivity of $\mid$
Linear combination closure
$a\mid b \Rightarrow a\mid b^2$
$a\mid b$ and $b\neq 0$ ⇒ $|a|\le|b|$ (careful signs)
$a\mid b$ and $b\mid a$ ⇒ $|a|=|b|$

Biconditionals

$n$ even iff $n+1$ odd
$n$ odd iff $n^2$ odd

Spec-shaped

If block size divides segment length, segment is whole number of blocks.
If $n$ divisible by $4$, half of half is integer.

Direct proof pocket card

Assume P (arbitrary objects)
Unpack definitions
Algebra / known lemmas
Pack definition of Q
Conclude P → Q

Tomorrow

Day 29 — Contrapositive & contradiction. When to switch methods; $\sqrt{2}$ irrational; infinite primes recall; uniqueness via contradiction.

English	Logical form (typical)
All \(P\)s are \(Q\)s	\(\forall x\,(P(x)\rightarrow Q(x))\)
Some \(P\) is a \(Q\)	\(\exists x\,(P(x)\wedge Q(x))\)
No \(P\) is a \(Q\)	\(\forall x\,(P(x)\rightarrow \neg Q(x))\) or \(\neg\exists x\,(P(x)\wedge Q(x))\)
Not all \(P\)s are \(Q\)s	\(\exists x\,(P(x)\wedge \neg Q(x))\)
Only \(P\)s are \(Q\)s	\(\forall x\,(Q(x)\rightarrow P(x))\)

Pitfall	What to do instead
\(\forall\) with \(\wedge\) for “all \(P\) are \(Q\)”	Use \(\rightarrow\) for restricted universals
\(\exists\) with \(\rightarrow\)	Use \(\wedge\): \(\exists x\,(P\wedge Q)\)
Negating \(\forall\) to \(\forall\neg\)	\(\neg\forall \equiv \exists\neg\)
Ignoring universe	State \(U\) or \(x\in S\)
Free variables left in “theorems”	Quantify or instantiate
Same witness assumed for two \(\exists\)	Combine into one \(\exists\) only if joint property
Scope ambiguity	Parenthesize quantifier bodies

Claim	Strategy
\(\forall x \exists y\, P(x,y)\)	Fix arbitrary \(x\); construct \(y=y(x)\); prove \(P\)
\(\exists y \forall x\, P(x,y)\)	Exhibit one \(y\); let \(x\) be arbitrary; prove \(P\)
\(\neg \forall x \exists y\, P\)	Find one \(x\) such that \(\forall y\, \neg P(x,y)\)
\(\exists! x\, P(x)\)	Existence + uniqueness (often uniqueness by assuming two and equating)

Form	\(y\) may depend on \(x\)?	English
\(\forall x\exists y\)	Yes	“for each \(x\), some \(y_x\)”
\(\exists y\forall x\)	No (one \(y\))	“one \(y\) for all \(x\)”
\(\forall x\forall y\)	N/A	all pairs
\(\exists x\exists y\)	N/A	some pair

Day 10 — Quantifiers & Direct Proof

Day 26 — Predicates & quantifiers

Why this matters

Theory

Predicates and open sentences

Universe of discourse

Universal quantifier \(\forall\)

Existential quantifier \(\exists\)

Restricted quantifiers

Free and bound variables

Scope and parentheses

Multiple variables, single “layer”

Negation rules (critical)

Translating English carefully

Quantifiers and connectives (common valid patterns)

Proof obligations (preview)

Worked examples

Exercises

CS connection

Common pitfalls

Checkpoint

Deep dive — quantifiers as big meet/join

Order of rewriting restricted forms

Common valid/invalid quantifier–connective moves

More worked examples

Additional exercises

Synthesis

Translation → negation → proof duty pipeline

More worked examples

Extra exercises (synthesis)

Self-check before Day 27

Tomorrow

Day 27 — Nested quantifiers

Why this matters

Theory

Reading nested quantifiers left to right

Order matters: inequivalence

Same quantifier, order free

Dependence and Skolem intuition (awareness)

Unique existence \(\exists!\)

Restricted nested quantifiers

Negating nested quantifiers

Sorting and order examples

Database / systems English

Alternation depth

Proving nested statements

Worked examples

Exercises

CS connection

Common pitfalls

Checkpoint

Deep dive — prenex form (awareness)

Dependence table

Sorting proofs need quantifiers

More worked examples

Additional exercises

Extended practice workshop

Order games (true/false on given \(U\))

Translations both ways

Negation drills

Proof drills

Sorting/database

Game metaphor card

Tomorrow

Day 28 — Direct proof

Why this matters

Theory

What a proof is (working contract)

Direct proof of \(P \rightarrow Q\)

Definitions to own (parity)

Definitions to own (divisibility)

Choosing good definitions

Biconditional proofs

“If and only if” via chain

Common direct-proof patterns

What direct proof is not

Quantifiers in the write-up

Lemmas and structure

Worked examples

Exercises