Type Preorders and Recursive Terms

We show how to use intersection types for building models of a λ-calculus enriched with recursive terms, whose intended meaning is of minimal fixed points. As a by-product we prove an interesting consistency result.