Standard-Model Semantics of HOL

Frame

Generalizing domain set $D$ of FOL and a family of domains $D_\tau$ for each sort $\tau$ in multisorted logic, in HOL we have one domain $D_t$ for each type $t$ (including structured types).

We require that $D_o = \{ t, f\}$ and we call its elements truth values. We call elements of $D_i$ individuals. We require that $D_{s \Rightarrow t}$ is a subset of the set of all total from $D_s$ to $D_t$ .

(If $D_{s \Rightarrow t}$ contains all total functions from $D_s$ to $D_t$ , we are talking about a standard model.)

Such a collection of $D_t$ for each $t$ is called a frame.

Interpretation

An interpretation consists of frames $D_t$ for each type $t$ , and a function $\alpha$ that maps constants to elements of appropriate sets in the frames.

We require that $\alpha$ map constant $=_{t \Rightarrow t \Rightarrow o}$ into (curried) equality relation on the set $D_t$ . That is, it is a function that, given $x$ , returns a characteristic function $sing_x$ of the singleton set $\{x\}$ , given by

$\begin{equation*}\begin{array}{l} sing_x(y) = true, \mbox{ if } y=x \\ sing_x(y) = false, \mbox{ if } y \neq x \\ \end{array}\end{equation*}$

On the other hand, we require $\alpha(\iota_{(i \Rightarrow o) \Rightarrow o})$ to be some choice function, which has the property that $\alpha(\iota)(sing_x) = x$ . Note that $\iota$ is defined for other functions as well, but we do not specify how it should behave on such functions.

Assignment

Whereas $\alpha$ maps values of equalities and the choice function, an assignment $\varphi$ maps values of variables, mapping each variable of type $t$ into element of $D_t$ .

General Model

We call an interpretation $((D_t)_t, \alpha)$ a general model if there exists a meaning function $e$ mapping each term of type $t$ to element of $D_t$ such that for all interpretations $\varphi$ the following holds:

$\begin{equation*}\begin{array}{l} e(\varphi)(x) = \varphi(x) \\ e(\varphi)(c) = \alpha(c) \mbox{ i{}f } c \mbox { is a constant } \\ e(\varphi)(F_1 F_2) = (e(\varphi)(F_1))(e(\varphi)(F_2)) \mbox{ (evaluate both arguments, perform function application) }\\ e(\varphi)(\lambda x_t. B) = f \mbox{ where } f(v) = e(\varphi[x:=v])(B) \mbox{ for all } v \in D_t \end{array} \end{equation*}$

If such interpretation function $e$ exists, then it is unique. The reason it may not exist is only if $D_t$ for some $t$ does not have sufficiently many elements so that $e(\varphi)(F) \in D_t$ . 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.

Standard Model

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 $D_{s \Rightarrow t}$ 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.