Logic, quantifiers, and the anatomy of a proof

"It seems to work" is not the standard. A program is correct when a claim holds for every input, not most - and to reason about "every," you need a language sharper than English. That language is logic: propositions glued by connectives ($\wedge ,\vee ,\neg ,\Rightarrow$), scoped by quantifiers ($\forall ,\exists$), and argued by proof. Get fluent here and "it seems to work" becomes "it cannot fail."

Propositions, connectives, and truth

Take two atomic propositions: $p$ = "it rained" and $q$ = "the ground is wet." Four connectives combine them, and each is defined by what it outputs for every combination of inputs:

• Negation $\neg p$ - "not $p$." Flips true and false.
• Conjunction $p\wedge q$ - "$p$ and $q$." True only when both hold.
• Disjunction $p\vee q$ - "$p$ or $q$." True when at least one holds (inclusive or).
• Implication $p\Rightarrow q$ - "if $p$ then $q$." The workhorse of every proof - and the one that trips people up.

The surprise is implication. $p\Rightarrow q$ is false in exactly one situation: when $p$ is true but $q$ is false (you promised, and broke the promise). Whenever $p$ is false, the implication is vacuously true - an unfired promise is never broken. Flip the switches below and watch that single false cell appear.

Build it: truth tables and a proof you assemble

Two labs in one. First, flip $p$ and $q$ like switches and watch the truth value of every expression light up - including the columns that reveal why the contrapositive is trustworthy and the converse is not. Then, use that fact to build a real proof: drag the rule that justifies each line into its gap before the next line unlocks.

Quantifiers, and how to negate anything

Propositions describe a single situation. To make claims about collections - "sorted for all inputs," "there is an index where..." - you need quantifiers. The universal $\forall xP(x)$ reads "for all $x$, $P(x)$ holds"; the existential $\exists xP(x)$ reads "there exists an $x$ with $P(x)$." A specification like "the array is sorted" unfolds to $\forall i.A[i]\le A[i+1]$.

The single most useful move is negation, because disproving a claim means proving its negation. Negation swaps the quantifiers and pushes the $\neg$ inward - the quantifier version of De Morgan's laws:

For a developer, these rules are already muscle memory in another form - Python's all() is $\forall$, any() is $\exists$, and negating one gives the other:

# all() is the ∀ ("for all") ; any() is the ∃ ("there exists")
nums = [4, 8, 15, 16, 23, 42]

all_even  = all(n % 2 == 0 for n in nums)   # ∀n. even(n)  -> False
some_even = any(n % 2 == 0 for n in nums)   # ∃n. even(n)  -> True

# Negating a "for all" yields a "there exists" (De Morgan for quantifiers):
#     ¬(∀n. even(n))  ==  ∃n. ¬even(n)
not_all_even = not all_even
exists_odd   = any(n % 2 != 0 for n in nums)
assert not_all_even == exists_odd            # same truth value, always

With connectives, quantifiers, and negation in hand, a proof is just a finite chain of statements where each one is a premise, a definition, or follows from earlier lines by a rule you are allowed to use. A direct proof assumes $p$ and marches to $q$. A proof by contradiction assumes the claim is false, then derives an impossibility like $r\wedge \neg r$ - since a contradiction can never hold, the assumption must have been wrong.

Check yourself