Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:ground_terms [2008/04/01 15:26] giuliano |
sav08:ground_terms [2013/05/10 11:02] vkuncak |
||
---|---|---|---|
Line 10: | Line 10: | ||
**Example**\\ | **Example**\\ | ||
- | ${\cal L}=\{a, f_1\}$ \\ | + | ${\cal L}=\{a, f\}$ \\ |
$GT=\{a, f(a), f(f(a)), f(f(f(a))), ...\}$ | $GT=\{a, f(a), f(f(a)), f(f(f(a))), ...\}$ | ||
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$? | ||
Line 23: | Line 23: | ||
Let $ar(f)=n$. Then $f : GT^n \to GT$ | Let $ar(f)=n$. Then $f : GT^n \to GT$ | ||
- | $\alpha_H(f)(t_1,\ldots,t_n) =$ ++| $f(t_1,\ldots,t_n)$++ | + | $\alpha_H(f)(t_1,\ldots,t_n) = f(t_1,\ldots,t_n)$ |
This defines $\alpha_H(f)$. How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$?\\ | This defines $\alpha_H(f)$. How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$?\\ | ||
Partition $GT^n$ in two sets, one over which $\alpha_H(R)(t_1,...,t_n)$ is true and the other over which it is false. | Partition $GT^n$ in two sets, one over which $\alpha_H(R)(t_1,...,t_n)$ is true and the other over which it is false. | ||
- | * is this possible for arbitrary set? ++| no ++ | + | * is this possible for arbitrary set? no |
**Example** | **Example** | ||
Line 46: | Line 46: | ||
**Example**\\ | **Example**\\ | ||
+ | ${\cal L}=\{a, f_1, P_1, R_2\}$ \\ | ||
+ | $GT=\{a, f(a), f(f(a)), f(f(f(a))), ...\}$\\ | ||
$HA=\{P(a), R(a,a), P(f(a)), R(a, f(a)), ...\}$\\ | $HA=\{P(a), R(a,a), P(f(a)), R(a, f(a)), ...\}$\\ | ||
$V=\{p_1, p_2, p_3, p_4, ...\}$\\ | $V=\{p_1, p_2, p_3, p_4, ...\}$\\ | ||
We define p such that :\\ | We define p such that :\\ | ||
- | $p(P(a))=v_1,\ p(R(a,a))=v_2,\ p(P(f(a)))=p_3,\ p(R(a, f(a)))=p_4,...$ | + | $p(P(a))=p_1,\ p(R(a,a))=p_2,\ p(P(f(a)))=p_3,\ p(R(a, f(a)))=p_4,...$ |