Differences

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

--- sav08:first-order_logic_semantics [2008/03/19 21:46]
damien
+++ sav08:first-order_logic_semantics [2008/04/02 20:49]
vkuncak
@@ Line 32: / Line 32: @@
 ++++How do we evaluate quantifiers?|
 \[\begin{array}{rcl}
-e_F(\exists x.F) &=& (\exists d \in D_I.\ e_F(F)(I[x \mapsto d])) \\
+e_F(\exists x.F)((D_I,\alpha_I)) &=& (\exists d \in D_I.\ e_F(F)((D_I,\alpha_I[x \mapsto d])) \\
-e_F(\forall x.F) &=& (\forall d \in D_I.\ e_F(F)(I[x \mapsto d]))
+e_F(\forall x.F)((D_I,\alpha_I)) &=& (\forall d \in D_I.\ e_F(F)((D_I,\alpha_I[x \mapsto d]))
 \end{array}
 \]
-where $I[x \mapsto d] = (D_I,\alpha^\prime_I)$ and
+See [[Sets and relations#function update|function update notation]] for definition of $\alpha_I[x \mapsto d]$.
-$\alpha^\prime_I(v) = \left \{ { {\alpha_I(v)~~\text{if}~ v \neq x} ~~ \atop {d ~~~~\text{if} ~ v=x}} \right. $
 ++++
@@ Line 130: / Line 129: @@
 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 =====
@@ Line 149: / Line 149: @@
 \[
 \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) \\