Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:first-order_logic_semantics [2008/04/02 21:27] vkuncak |
sav08:first-order_logic_semantics [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 14: | Line 14: | ||
We evaluate terms by recursion on the structure of $T$: | We evaluate terms by recursion on the structure of $T$: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{rcl} | \begin{array}{rcl} | ||
e_T(x)(I) & = & \alpha_I(x) \\ | e_T(x)(I) & = & \alpha_I(x) \\ | ||
e_T(f(t_1,\ldots,t_n))(I) &=& \alpha_I(f)(e_T(t_1)(I),\ldots,e_T(t_2)(I)) | e_T(f(t_1,\ldots,t_n))(I) &=& \alpha_I(f)(e_T(t_1)(I),\ldots,e_T(t_2)(I)) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
We evaluate formulas by recursion on the structure of $F$: | We evaluate formulas by recursion on the structure of $F$: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{rcl} | \begin{array}{rcl} | ||
e_F(R(t_1,\ldots,t_n)(I) &=& (e_T(t_1)(I),\, \ldots,\, e_T(t_n)(I)) \, \in \, \alpha_I(R) \\ | e_F(R(t_1,\ldots,t_n)(I) &=& (e_T(t_1)(I),\, \ldots,\, e_T(t_n)(I)) \, \in \, \alpha_I(R) \\ | ||
Line 29: | Line 29: | ||
e_F(\lnot F)(I) &=& \lnot e_F(F)(I) \\ | e_F(\lnot F)(I) &=& \lnot e_F(F)(I) \\ | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
++++How do we evaluate quantifiers?| | ++++How do we evaluate quantifiers?| | ||
- | \[\begin{array}{rcl} | + | \begin{equation*}\begin{array}{rcl} |
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(\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)((D_I,\alpha_I)) &=& (\forall d \in D_I.\ e_F(F)((D_I,\alpha_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} | \end{array} | ||
- | \] | + | \end{equation*} |
See [[Sets and relations#function update|function update notation]] for definition of $\alpha_I[x \mapsto d]$. | See [[Sets and relations#function update|function update notation]] for definition of $\alpha_I[x \mapsto d]$. | ||
++++ | ++++ | ||
Line 51: | Line 51: | ||
Consider language ${\cal L} = \{ s, {<} \}$ where $s$ is a unary function symbol ($ar(s)=1$) and ${<}$ is a binary relation symbol ($ar({<})=2$). Let $I = (D,\alpha)$ be given by | Consider language ${\cal L} = \{ s, {<} \}$ where $s$ is a unary function symbol ($ar(s)=1$) and ${<}$ is a binary relation symbol ($ar({<})=2$). Let $I = (D,\alpha)$ be given by | ||
- | \[\begin{array}{rcl} | + | \begin{equation*}\begin{array}{rcl} |
D &=& \{ 0,1, 2 \} \\ | D &=& \{ 0,1, 2 \} \\ | ||
\alpha(x) &=& 1 \\ | \alpha(x) &=& 1 \\ | ||
Line 57: | Line 57: | ||
\alpha({<}) &=& \{ (0,1), (0,2), (1,2) \} | \alpha({<}) &=& \{ (0,1), (0,2), (1,2) \} | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
Let us evaluate the truth value of these formulas: | Let us evaluate the truth value of these formulas: | ||
* $x < s(x)$ | * $x < s(x)$ | ||
++++answer| | ++++answer| | ||
- | \[\begin{array}{rcl} | + | \begin{equation*}\begin{array}{rcl} |
e_F(x < s(x))(I) &=& (e_T(x)(I),e_T(s(x))(I)) \in \alpha(<) \\ | 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(<) \\ | &=& (\alpha(x),\alpha(s)(e_T(x)(I))) \in \alpha(<) \\ | ||
Line 69: | Line 69: | ||
&=& true | &=& true | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
++++ | ++++ | ||
* $\exists x. \lnot (x < s(x))$ | * $\exists x. \lnot (x < s(x))$ | ||
++++answer| | ++++answer| | ||
- | \[\begin{array}{rcl} | + | \begin{equation*}\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]))\\ | 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.\ \neg e_F((x < s(x))(I[x \mapsto d])\\ | ||
Line 80: | Line 80: | ||
&=& true | &=& true | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
++++ | ++++ | ||
* $\forall x. \exists y. x < y$ | * $\forall x. \exists y. x < y$ | ||
++++answer| | ++++answer| | ||
- | \[\begin{array}{rcl} | + | \begin{equation*}\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]))\\ | 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.\ e_F(\exists y. x < y)(I[x \mapsto d])\\ | ||
Line 93: | Line 93: | ||
&=& false | &=& false | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
++++ | ++++ | ||
Line 101: | Line 101: | ||
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: | 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: | ||
- | \[ | + | \begin{equation*} |
\alpha(dvd) = \{ (i,j).\ \exists k \in \{2,3,4,\ldots\}.\ j = k \cdot i \} | \alpha(dvd) = \{ (i,j).\ \exists k \in \{2,3,4,\ldots\}.\ j = k \cdot i \} | ||
- | \] | + | \end{equation*} |
What is the truth value of this formula | What is the truth value of this formula | ||
- | \[ | + | \begin{equation*} |
\forall x.\, \exists y.\, dvd(x,y) | \forall x.\, \exists y.\, dvd(x,y) | ||
- | \] | + | \end{equation*} |
++answer| | ++answer| | ||
$true$. For any $x$ choose $y$ as $2 \cdot x$. | $true$. For any $x$ choose $y$ as $2 \cdot x$. | ||
Line 113: | Line 113: | ||
What is the truth value of this formula | What is the truth value of this formula | ||
- | \[ | + | \begin{equation*} |
\exists x.\, \forall y. dvd(x,y) | \exists x.\, \forall y. dvd(x,y) | ||
- | \] | + | \end{equation*} |
++answer| | ++answer| | ||
$false$ | $false$ | ||
Line 124: | Line 124: | ||
Let $I=(D,\alpha)$ be an arbitrary interpretation. Consider formula | Let $I=(D,\alpha)$ be an arbitrary interpretation. Consider formula | ||
- | \[ | + | \begin{equation*} |
(\forall x. P(x)) \rightarrow (\exists y. P(y)) | (\forall x. P(x)) \rightarrow (\exists y. P(y)) | ||
- | \] | + | \end{equation*} |
What is its truth value in $I$? Which condition on definition of $I$ did we use? | What is its truth value in $I$? Which condition on definition of $I$ did we use? | ||
Line 151: | Line 151: | ||
**Lemma**: Let $T$ be a set of formulas and $G$ a formula. Then $T \models \{G\}$ iff the set $T \cup \{\lnot G\}$ is contradictory. | **Lemma**: Let $T$ be a set of formulas and $G$ a formula. Then $T \models \{G\}$ iff the set $T \cup \{\lnot G\}$ is contradictory. | ||
++++Proof:| | ++++Proof:| | ||
- | \[ | + | \begin{equation*} |
\begin{array}{rcl} | \begin{array}{rcl} | ||
T \models G & \leftrightarrow & \forall I. ((\forall F \in T. e_F(F)(I)) \rightarrow e_F(G)(I)) \\ | T \models G & \leftrightarrow & \forall I. ((\forall F \in T. e_F(F)(I)) \rightarrow e_F(G)(I)) \\ | ||
Line 160: | Line 160: | ||
& \leftrightarrow & \lnot \exists I. e_S(T \cup \{\lnot G\})(I) | & \leftrightarrow & \lnot \exists I. e_S(T \cup \{\lnot G\})(I) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
++++ | ++++ | ||
Line 168: | Line 168: | ||
**Definition**: The set of all consequences of $T$: | **Definition**: The set of all consequences of $T$: | ||
- | \[ | + | \begin{equation*} |
Conseq(T) = \{ F \mid T \models F \} | Conseq(T) = \{ F \mid T \models F \} | ||
- | \] | + | \end{equation*} |
Note $T \models F$ is equivalent to $F \in Conseq(T)$. | Note $T \models F$ is equivalent to $F \in Conseq(T)$. | ||
**Lemma**: The following properties hold: | **Lemma**: The following properties hold: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{rcl} | \begin{array}{rcl} | ||
T &\subseteq & Conseq(T) \\ | T &\subseteq & Conseq(T) \\ | ||
Line 182: | Line 182: | ||
T_1 \subseteq Conseq(T_2) \land T_2 \subseteq Conseq(T_1) & \rightarrow & Conseq(T_1) = Conseq(T_2) | T_1 \subseteq Conseq(T_2) \land T_2 \subseteq Conseq(T_1) & \rightarrow & Conseq(T_1) = Conseq(T_2) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |