Part 0 · 1 chapters · ~8 min

Logic and Proof

Propositions and connectives, truth tables, implication and vacuous truth, equivalences (De Morgan, distribution, contrapositive), predicates and quantifiers, negating quantified statements, proof techniques (direct, contrapositive, contradiction, cases), and loop invariants as proofs about code.

1

Propositions in code

code
// De Morgan: these two guards are the same
if (!(user.verified && user.kycTier >= 2)) deny();
if (!user.verified || user.kycTier < 2) deny();

// quantifiers: ∀ and ∃, and negation swapping them
const allSettled = payouts.every(p => p.state === 'settled');       // ∀p. settled(p)
const anyOpen    = payouts.some(p => p.state !== 'settled');        // ¬∀p. settled(p) ≡ ∃p. ¬settled(p)
console.assert(allSettled === !anyOpen);
[].every(() => false)   // true: vacuous truth, every element of nothing satisfies anything

Proof by contradiction: to show √2 is irrational, assume √2 = a/b in lowest terms; then a² = 2b², so a is even, a = 2c, so b² = 2c², so b is even: both even contradicts "lowest terms". Loop invariants are proofs about code: state something true before each iteration, show the body preserves it, and read off the result at exit (Algorithms course on binary search).

LOGIC IN THE CODE YOU WRITE
propositions, connectives, laws
and, or, notp && q, p || q, !p: truth tablesdefine them completely.implicationp → q is false only when p is trueand q is false.De Morgan!(a && b) == !a || !b ; !(a || b)== !a && !bquantifiers∀ = every (arr.every), ∃ = some(arr.some).negating ∀not (every x ok) = some x not ok.contrapositivep → q is equivalent to ¬q → ¬p.
swipe the figure sideways, or tap expand for full screen
1/5
connectives
Boolean operators are logical connectives; a truth table lists every input combination, which is also how to test a complex condition exhaustively.
truth tablestest conditions exhaustively