Differences

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

--- sav08:first-order_logic_semantics [2008/03/19 20:33]
damien correction of typos + def of I[x -> d]
+++ sav08:first-order_logic_semantics [2008/03/19 21:46]
damien
@@ Line 43: / Line 43: @@
 ===== Examples =====
 ==== Example with Finite Domain ====
@@ Line 50: / Line 51: @@
   D &=& \{ 0,1, 2 \} \\
   \alpha(x) &=& 1 \\
-  \alpha(f) &=& \{ (0,1), (1,2), (2,0) \} \\
+  \alpha(s) &=& \{ (0,1), (1,2), (2,0) \} \\
   \alpha({<}) &=& \{ (0,1), (0,2), (1,2) \}
 \end{array}
@@ Line 57: / Line 58: @@
 Let us evaluate the truth value of these formulas:
   * $x < s(x)$
-  * $\exists x. \lnot (x < s(x)$
+++++answer|
+\[\begin{array}{rcl}
+  e_F(x < s(x))(I) &=& (e_T(x)(I),e_T(s(x))(I)) \in \alpha(<) \\
+  &=& (\alpha(x),\alpha(s)(e_T(x)(I))) \in \alpha(<) \\
+  &=& (1,\alpha(s)(1)) \in \alpha(<) \\
+  &=& (1,2) \in \alpha(<) \\
+  &=& true
+\end{array}
+\]
+++++
+  * $\exists x. \lnot (x < s(x))$
+++++answer|
+\[\begin{array}{rcl}
+  e_F(\exists x. \lnot (x < s(x)))(I) &=& (\exists d \in D.\ e_F(\lnot (x < s(x))(I[x \mapsto d]))\\
+  &=& \exists d \in D.\ \neg e_F((x < s(x))(I[x \mapsto d])\\
+  &=& \exists d \in D.\ (d, \alpha(s)(d)) \notin \alpha(<)\\
+  &=& (2,0)\notin \alpha(<)\\
+  &=& true
+\end{array}
+\]
+++++
   * $\forall x. \exists y. x < y$
+++++answer|
+\[\begin{array}{rcl}
+  e_F(\forall x. \exists y. x < y)(I) &=& (\forall d \in D.\ e_F(\exists y. x < y)(I[x \mapsto d]))\\
+  &=& \forall d \in D.\ e_F(\exists y. x < y)(I[x \mapsto d])\\
+  &=& \forall d \in D.\ \exists e \in D. e_F(x < y)(I[x \mapsto d][y \mapsto e])\\
+  &=& \forall d \in D.\ \exists e \in D. (d,e) \in \alpha(<) \\
+  &=& \exists e \in D. (2,e) \in \alpha(<) \\
+  &=& ((2,0) \in \alpha(<)) \vee ((2,1) \in \alpha(<)) \vee ((2,2) \in \alpha(<))\\
+  &=& false
+\end{array}
+\]
+++++
 ==== Example with Infinite Domain ====
-Consider language ${\cal L} = \{ s, dvd \}$ where $s$ is a unary function symbol ($ar(s)=1$) and ${<}$ is a binary relation symbol ($ar({<})=2$).  Let $I = (D,\alpha)$ where $D = \{7, 8, 9, 10, \ldots\}$.  Let $dvd$ be defined as the "strictly divides" relation:
+Consider language ${\cal L} = \{ s, dvd \}$ where $s$ is a unary function symbol ($ar(s)=1$) and $dvd$ is a binary relation symbol ($ar(dvd)=2$).  Let $I = (D,\alpha)$ where $D = \{7, 8, 9, 10, \ldots\}$.  Let $dvd$ be defined as the "strictly divides" relation:
 \[
    \alpha(dvd) = \{ (i,j).\  \exists k \in \{2,3,4,\ldots\}.\ j = k \cdot i \}
@@ Line 70: / Line 105: @@
     \forall x.\, \exists y.\, dvd(x,y)
 \]
+++answer|
+$true$. For any $x$ choose $y$ as $2 \cdot x$.
+++
 What is the truth value of this formula
 \[
     \exists x.\, \forall y. dvd(x,y)
 \]
+++answer|
+$false$
+++
 ==== Domain Non-Emptiness ====
@@ Line 83: / Line 126: @@
 What is its truth value in $I$?  Which condition on definition of $I$ did we use?
+This formula is true with the assumption that $D$ is not empty.
+With an empty domain, this formula would be false.
+There are other problems, for instance "how to evaluate a variable?".
 ===== Satisfiability, Validity, and Semantic Consequence =====