Diary of an itinerant turnstilist in their daily quest for deeper confusion....
{Previously: Part 0 } What I'm calling structural normalization -- a normalization procedure for simply-typed lambda calculus derived from concepts from structural proof theory -- can be achieved as a round trip with four stops. STLC -> intuitionistic sequent calculus (LJ) Cut elimination for LJ (to LJ-) LJ- to canonical forms STLC (CF) Home again: transliteration of canonical forms (CF) back to…
In 1935, Gentzen [1] introduced natural deduction as a system of formal logic and wanted to prove it sound. To do this, he also invented the sequent calculus, proved it sound (via the Hauptsatz, better known today as Cut Elimination), and showed that every natural deduction proof could be translated to it via a funny intermediate system called LHJ (the "H" is for Hilbert, because the system is…
[Based on conversations with Rob Simmons . Reader prerequisites: comfortable with inference rules, peano notation, state machines.] The following inference rules, it can be argued, define addition: whenever plus N M P holds, the numbers N and M sum to P . ----------------- pz plus 0 N N plus N M P -------------------- ps plus (s N) M (s P) With these rules, here's a derivation that 2 + 2 = 4:…