LOGIKĒ · the lineage of logical form · one logician, one sphere · kept by THE LOGICIAN

GIUSEPPE PEANO ◧ 2D · ◍ 3D · ◆ 4D · ◐ shadow · 👶 TAP

Peano built all of arithmetic from almost nothing: a zero, a successor (“the next one”), and induction (true for 0, and if true for n then true for n+1, so true for all n). Slide n and watch induction stack the triangular number 0+1+…+n into the closed form n(n+1)/2 — proved, not asserted.

◆ LIT▲ AMBER
◧ THE MEASURE · 2D
◍ THE SUCCESSOR CHAIN · 3D · 0 climbs
◆ THE FOURTH · 4D · a tesseract turns
◐ THE SHADOW · one dimension down
👶 THE TODDLER CORNER — one fat tap
n
0+1+…+n
n(n+1)/2
induction

◆ LIT — exact / checkable

Addition and multiplication are defined by recursion on the successor: a+0=a, a+S(b)=S(a+b); a·0=0, a·S(b)=a·b+a. Those two clauses, plus induction, are enough. The instrument runs the recursive add and mul live and a fail-loud self-check throws unless they match ordinary arithmetic for all a,b in 0..11 AND the inductive step S(n)=S(n−1)+n reproduces n(n+1)/2 for every n up to 50 — the sum is grown one successor at a time, never plugged into the formula.

▲ AMBER — the figure

The visual triangle is a picture of the theorem, not the proof; the proof is the induction the self-check performs. Peano’s axioms (1889) also assume 0 is not a successor and successor is injective — structural facts we take as given here.

LOGIKĒ: a proof is a machine anyone can run and get the same result.  — THE LOGICIAN
David Lee Wise / ROOT0 / TriPod LLC  ·  the logician’s lineage, with AVAN