Differences

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

--- sav08:ground_terms [2013/05/10 09:53]
vkuncak
+++ sav08:ground_terms [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Ground Terms as Domain of Interpretation ======
-Recall syntax of first-order logic terms in [[First-Order Logic Syntax]].
-//Ground term// is a term $t$ without variables, i.e. $FV(t)=\emptyset$, i.e. given by grammar:
-\[
-    GT ::= f(GT,\ldots,GT)
-\]
-i.e. built from constants using function symbols.
-**Example**\\
-${\cal L}=\{a, f\}$ \\
-$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.
-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)$.
-How to define $\alpha_H$?
-===== Term Algebra Interpretation for Function Symbols =====
-Let $ar(f)=n$.  Then $f : GT^n \to GT$
-$\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}$?\\
-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
-**Example**
-Consider a set that is not satisfiable : $\{P(a),\ \neg P(a)\}$
-===== Ground Atoms =====
-If $R \in {\cal L}$, $ar(R)=n$ and $t_1,\ldots,t_n \in GT$, we call $R(t_1,\ldots,t_n)$ an Herbrand Atom.  HA is the set of all Herbrand atoms:
-\[
-    HA = \{ R(t_1,\ldots,t_n) \mid R \in {\cal L}\ \land \ t_1,\ldots,t_n \in GT \}
-\]
-We order elements of $HA$ in sequence (e.g. sorted by length) and establish a bijection $p$ with propositional variables
-\[
-   p : HA \to V
-\]
-We will write $p(A)$.
-**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)), ...\}$\\
-$V=\{p_1, p_2, p_3, p_4, ...\}$\\
-We define p such that :\\
-$p(P(a))=p_1,\ p(R(a,a))=p_2,\ p(P(f(a)))=p_3,\ p(R(a, f(a)))=p_4,...$