  Extensional higher-order logic programming has been introduced as a
generalization of classical logic programming. An important characteristic of
this paradigm is that it preserves all the well-known properties of traditional
logic programming. In this paper we consider the semantics of negation in the
context of the new paradigm. Using some recent results from non-monotonic
fixed-point theory, we demonstrate that every higher-order logic program with
negation has a unique minimum infinite-valued model. In this way we obtain the
first purely model-theoretic semantics for negation in extensional higher-order
logic programming. Using our approach, we resolve an old paradox that was
introduced by W. W. Wadge in order to demonstrate the semantic difficulties of
higher-order logic programming.
