Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:standard-model_semantics_of_hol [2008/05/28 02:24] vkuncak |
sav08:standard-model_semantics_of_hol [2008/05/28 02:26] vkuncak |
||
|---|---|---|---|
| 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 ===== | ||
| Line 36: | Line 37: | ||
| \end{array} | \end{array} | ||
| \] | \] | ||
| - | 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 ===== | ||