Differences

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

--- sav08:herbrand_s_expansion_theorem [2008/03/24 11:38]
vkuncak
+++ sav08:herbrand_s_expansion_theorem [2009/05/26 10:26]
vkuncak
@@ Line 28: / Line 28: @@
 **Example**
+Let's consider the expanded formula $F=P(f(a)) \wedge R(a, f(a))$, then $p(F)=p_1 \wedge p_4$
-Define propositional model $I_P : V \to \{{\it true},{\it false\}\}$ by
+Define propositional model $I_P : V \to \{\it true},{\it false\}$ by
 \[
     I_P(p(C_G)) = e_F(C_G)(I)
@@ Line 65: / Line 66: @@
   * set $propExpand(S)$ has a propositional model
   * set $S$ has a model with domain $GT$
+**Example:** Take the first three clauses our example (from [[Normal Forms for First-Order Logic]]):
+  * $R(x,g(x))$
+  * $\neg R(x,y) \lor R(x,f(y,z)))$
+  * $P(x) \lor P(f(x,a))$
+Taking as domain $D$ the set of natural numbers, the structure $(D,\alpha)$ is a model of the conjunction of these three clauses, where $\alpha$ is given by:
+  * $\alpha(a) = 1$
+  * $\alpha(c) = 2$
+  * $\alpha(g)(x) = (x + 1)$
+  * $\alpha(f)(y,z) = y+z$
+  * $\alpha(R) = \{(x,y).\ x < y\}$
+  * $\alpha(P) = \{x.\ x \mbox{ is even} \}$
+This model induces an Herbrand model $(GT,\alpha_H)$, in which $\alpha_H(P)$ is a set of ground terms and $\alpha_H(R)$ is a relation on ground terms, $\alpha_H(R) \subseteq GT^2$.
+To determine, for example, whether $(f(a,a),g(g(a))) \in \alpha_H(R)$ we check the truth value of the formula
+\[
+   R(f(a,a),g(c)))
+\]
+in the original interpretation $(D,\alpha)$. In this case, the formula reduces to $1+1 < 2+1$ and is true in the interpretation. Therefore, we define $\alpha_H(R)$ to contain the pair of ground terms $(f(a,a),g(c)))$.