Description of Solution

Reflexive models in which abstraction is unconstrained exist. The lambda calculus is the most widely known such system. We may think of the semantics of such a system as being determined by a semantic domain `D' and by the semantics of application, which must be a function of type:

App : D -> (D - -> D)

Where we use the symbol -> for the space of total functions and - -> for the space of partial functions. Under the normal semantics for the lambda calculus (induced by normal order semantics) the function spaces in the range will be total, but this does not hold of our intended models so we admit the possibility that a value in the domain is interpreted under application as a partial function. This gives rise to the possibility of non denoting terms formed by applying a term denoting a partial function to a term denoting a value not in its domain. Application is to be considered strict in relation to such non denoting terms. If some other behaviour is required then this is best achieved by adding undefined values into the semantic domain and reverting to total functions.

The problem so far as the lambda calculus is concerned is that the operators which we require for logical purposes are simply not in the range of the semantics of application. So we are looking for models consisting of a suitable domain, with an application semantic which has the appropriate logical operators in its range. Aczel's work suggests that this may be a vain hope, there may be no such models.