Standard-Model Semantics of HOL
Generalizing domain set of FOL and a family of domains for each sort in multisorted logic, in HOL we have one domain for each type (including structured types).
We require that and we call its elements truth values. We call elements of individuals. We require that is a subset of the set of all total from to .
(If contains all total functions from to , we are talking about a standard model.)
Such a collection of for each is called a frame.
An interpretation consists of frames for each type , and a function that maps constants to elements of appropriate sets in the frames.
We require that map constant into (curried) equality relation on the set . That is, it is a function that, given , returns a characteristic function of the singleton set , given by
On the other hand, we require to be some choice function, which has the property that . Note that is defined for other functions as well, but we do not specify how it should behave on such functions.
Whereas maps values of equalities and the choice function, an assignment maps values of variables, mapping each variable of type into element of .
We call an interpretation a general model if there exists a meaning function mapping each term of type to element of such that for all interpretations the following holds:
If such interpretation function exists, then it is unique. The reason it may not exist is only if for some does not have sufficiently many elements so that . But for standard model this is not a concern, and in such case the meaning is what we would expect, with lambda terms denoting total functions and quantification denoting quantification over all functions.
We will focus on standard models in this lecture; they correspond to our expected interpretation of HOL, but they do not have an enumerable set of axioms. If we allow non-standard models (where only some of the functions in exist, that is, at least those that have names), then we can have an enumerable set of axioms, but then we allow small models (like Herbrand models in FOL). This is very analogous to what happens when we add axioms to FOL and consider theories of integers or set theory: we must accept either non-standard models or non-effetive axiomatization. HOL is in fact similar to having FOL with some extra axioms.