Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:ground_terms [2013/05/10 09:53] vkuncak |
sav08:ground_terms [2013/05/10 11:02] vkuncak |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| If ${\cal L}$ has no constants then $GT$ is empty. In that case, we add a fresh constant $a_0$ into the language and consider ${\cal L} \cup \{a_0\}$ that has a non-empty $GT$. We call the set $GT$ Herbrand Universe. | If ${\cal L}$ has no constants then $GT$ is empty. In that case, we add a fresh constant $a_0$ into the language and consider ${\cal L} \cup \{a_0\}$ that has a non-empty $GT$. We call the set $GT$ Herbrand Universe. | ||
| - | Goal: show that if a formula //without equality// (for now) has a model, then it has a model whose domain is Herbrand universe, that is, a model of the form $I_H = (HU,\alpha_H)$. | + | Goal: show that if a formula //without equality// (for now) has a model, then it has a model whose domain is Herbrand universe, that is, a model of the form $I_H = (GT,\alpha_H)$. |
| How to define $\alpha_H$? | How to define $\alpha_H$? | ||