Statman′s 1-Section Theorem

Statman′s 1-Section Theorem (Statman, 1985a, in "Harvey Friedman′s Research on the Foundations of Mathematics" ( L. Harrington et al. , Eds.), pp. 331-338, North-Holland, Amsterdam) is an important but little-known result in the model theory of the simply typed λ-calculus. The 1-Section Theorem states a necessary and sufficient condition on models of the simply-typed λ-calculus for determining whether βη-equational reasoning is complete for proving equations that hold in a model. We review the statement of the theorem, give a detailed proof, and discuss its significance.

Authors

• J.G. Riecke

Keywords

No keywords are indexed for this paper.