Simply typed lambda calculus and intuitionistic propositions

Alpha-classes of explicitly annotated terms; simple types generated by atomic types, booleans, and arrows, extended by products, sums, unit, and the empty type; ordered distinct-variable contexts; deterministic call-by-value evaluation whose beta, projection, and case roots require value arguments; and a separate proof-reduction relation generated by seven roots and the complete one-hole context grammar of subappendix A.2. The Curry–Howard presentation is intuitionistic propositional natural deduction. There is no polymorphism, subtyping, recursive type, general recursion, state, or effect.

Renaming, alpha-invariance of typing, scope, weakening, substitution, inversion, canonical forms, preservation, progress, and type safety are proved in chapter 2. Compatible proof reduction satisfies subject reduction. A reducibility argument with an explicit finite reduction-height induction, under the finitely branching König principle declared in the chapter, proves strong normalization. Every call-by-value step is a proof step, so closed typed terms evaluate to values; typed normal forms then give consistency of the propositional system.

The annotated boolean–arrow calculus has unique types and syntax-directed synthesis. Products, unit, empty elimination, and cases retain syntax-directed checking, but bare sum injections do not synthesize a unique unused summand. No polymorphic principal-type theorem is claimed.

None is used for these metatheorems.