Generalized filter models

AbstractIn this paper, starting from filters which are a natural generalization of intersection filters (Barendregt et al., J. Symbolic Logic 48 (1983) 931–940), the existence of filter models and filter semimodels for the λ-calculus is investigated. The construction of filters is based on a Z-semilattice of types in which the subsets having infimum are given by a collection Z, called subset system. The set of representable functions is characterized in the obtained domain. In the case where the properties of the subset system Z guarantee the existence of a filter model, the proof of soundness and completeness of the associated natural Z-type assignment system is routine