Differences

This shows you the differences between two versions of the page.

 sav08:standard-model_semantics_of_hol [2008/05/28 02:24]vkuncak sav08:standard-model_semantics_of_hol [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/05/28 02:26 vkuncak 2008/05/28 02:24 vkuncak 2008/05/28 02:19 vkuncak 2008/05/27 17:26 vkuncak created Next revision Previous revision 2008/05/28 02:26 vkuncak 2008/05/28 02:24 vkuncak 2008/05/28 02:19 vkuncak 2008/05/27 17:26 vkuncak created Line 16: Line 16: 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 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{array}{l} + \begin{equation*}\begin{array}{l} ​sing_x(y) = true, \mbox{ if } y=x \\ ​sing_x(y) = true, \mbox{ if } y=x \\ ​sing_x(y) = false, \mbox{ if } y \neq x \\ ​sing_x(y) = false, \mbox{ if } y \neq x \\ - \end{array}$ + \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. 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. Line 25: Line 25: 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$.  ​ 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 ===== ===== 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: 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{array}{l} + \begin{equation*}\begin{array}{l} e(\varphi)(x) = \varphi(x) \\ e(\varphi)(x) = \varphi(x) \\ e(\varphi)(c) = \alpha(c) \mbox{ i{}f } c \mbox { is a constant } \\ e(\varphi)(c) = \alpha(c) \mbox{ i{}f } c \mbox { is a constant } \\ Line 35: Line 36: e(\varphi)(\lambda x_t. B) = f \mbox{ where } f(v) = e(\varphi[x:​=v])(B) \mbox{ for all } v \in D_t 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{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 ​to define all functions.  But for standard model this is certainly true, and the meaning ​of terms is the expected one. + 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 ===== ===== Standard Model =====