Formal proof in LEGO of
weak normalization of MIL using Tait computability method. This is
the simplest use I know of Tait computability.
(16/3/04) (First 2 sections of Accumulated lecture notes.) A preview of
two main ideas: the Curry-Howard correspondence, and the duality
between introduction and elimination, with structural recursion being
the induced computation. We then begin with minimal implicational
logic (MIL).
(18/3/04) Through section 3, normalization of MILT.