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

MOSES SCHÖNFINKEL ◧ 2D · ◍ 3D · ◆ 4D · ◐ shadow · 👶 TAP

Schönfinkel showed you can throw away variables entirely. Two combinators — K (keep the first, drop the second) and S (share the argument) — are enough to build every function. Their most famous trick: S K K is the identity. Slide to choose an input and watch S K K x reduce, step by step, back to x.

◆ LIT▲ AMBER
◧ THE MEASURE · 2D
◍ THE TREE COLLAPSES · 3D · S K K x → x
◆ THE FOURTH · 4D · a tesseract turns
◐ THE SHADOW · one dimension down
👶 THE TODDLER CORNER — one fat tap
term
S K K x
reduces to
x preserved
identity

◆ LIT — exact / checkable

K a b = a and S f g x = f x (g x). Apply S K K x = K x (K x) = x, because the outer K keeps its first argument x and discards the second (K x). The reducer here is real closures: K=a=>b=>a, S=f=>g=>x=>f(x)(g(x)), I=S(K)(K). A fail-loud self-check throws unless S(K)(K)(x)===x for a spread of inputs AND K(a)(b)===a — i.e. the identity really is manufactured from S and K with no variable of its own.

▲ AMBER — the figure

Showing x as a coloured token is a stand-in; the mechanism is the closure reduction, which is exact. Full combinatory completeness (that S and K build ALL functions, via bracket abstraction) is Schönfinkel’s 1924 theorem, cited not re-proved 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