Another purpose is to illustrate that for this kind of foundational discussion, Higher Order Set Theory is a congenial environment, and to illustrate one way of proceeding about such an exercise. The aim was to come up with semantic domains for well-founded strong languages which included local polymorphic function definitions and elementary modularity. I was looking for a simple foundation system which could be used to define the semantics and derive the proof rules for specification languages such as VDM-SL and Z, and I had a prejudice in favour of high proof theoretic strength. Pure functions were the first step in a three stage construction which I then envisaged but did not complete. An elaborate hierarchy of sets is built out of the empty set and nothing else.
Pure functions are analogous.
The empty function is the only function whose domain and range are the empty set, and in set theory is identical with the empty set. Since we start by constructing a model rather than a logic it may not be immediately obvious what this means. What it means is that the model should be sufficiently rich to establish the consistency of an axiomatisation of the theory which has high proof theoretic strength. This isn't targeted as a first order theory, though a first order presentation should be straightforward. Just as in set theory, there should be no type system, and only one kind of object in the universe.