Differences

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

--- sav08:first-order_logic_semantics [2008/03/19 21:09]
damien typo + answer to the evaluation
+++ sav08:first-order_logic_semantics [2008/03/19 21:52]
damien
@@ Line 92: / Line 92: @@
 \]
 ++++
 ==== 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 103: / 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 115: / Line 125: @@
 \]
 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?".
@@ Line 135: / Line 150: @@
 \[
 \begin{array}{rcl}
-T \models G & \leftrightarrow &  \forall I. ((\forall F \in T. e_F(F)(I)) \rightarrow e_F(G)) \\
+T \models G & \leftrightarrow &  \forall I. ((\forall F \in T. e_F(F)(I)) \rightarrow e_F(G)(I)) \\
-            & \leftrightarrow &  \forall I. (\lnot (\forall F \in T. e_F(F)(I)) \lor \lnot e_F(\lnot G)) \\
+            & \leftrightarrow &  \forall I. (\lnot (\forall F \in T. e_F(F)(I)) \lor \lnot e_F(\lnot G)(I)) \\
-            & \leftrightarrow &  \forall I. (\exists F \in T. \lnot e_F(F)(I)) \lor \lnot e_F(\lnot G)) \\
+            & \leftrightarrow &  \forall I. (\exists F \in T. \lnot e_F(F)(I)) \lor \lnot e_F(\lnot G)(I)) \\
             & \leftrightarrow &  \forall I. \exists F \in T \cup \{\lnot G\}. \lnot e_F(F)(I) \\
             & \leftrightarrow & \lnot \exists I. \forall F \in T \cup \{\lnot G\}. e_F(F)(I) \\