On a Question of H. Friedman

Abstract

In this paper we answer a question of Friedman, providing an ω-separable model M of the λβη-calculus. There therefore exists an α-separable model for any α≥0. The model M permits no non-trivial enrichment as a partial order; neither does it permit an enrichment as a category with an initial object. The open term model embeds in M: by way of contrast we provide a model which cannot embed in any non-trivial model separating all pairs of distinct elements.