Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:first-order_logic_semantics [2008/04/02 20:49]
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]$.
 ++++ ++++
  
 We generalize this notion as follows: if $I$ is an interpretation and $T$ is a set of first-order formulas, we write $e_S(T)(I)={\it true}$ iff for every $F \in T$ we have $e_F(F)(I)={\it true}$ (set is treated as infinite conjunction). ​  This is a generalization because $e_S(\{F\})(I) = e_F(F)(I)$. We generalize this notion as follows: if $I$ is an interpretation and $T$ is a set of first-order formulas, we write $e_S(T)(I)={\it true}$ iff for every $F \in T$ we have $e_F(F)(I)={\it true}$ (set is treated as infinite conjunction). ​  This is a generalization because $e_S(\{F\})(I) = e_F(F)(I)$.
 +
 +
 +**A terminological note:** in algebra, an interpretation is often called a //​structure//​. Instead of using $\alpha$ mapping language ${\cal L} = \{ f_1,​\ldots,​f_n,​ R_1,​\ldots,​R_m\}$ to interpretation of its symbols, the structure is denoted by a tuple $(D,​\alpha(f_1),​\ldots,​\alpha(f_n),​\alpha(R_1),​\ldots,​\alpha(R_n))$. ​ For example, an interpretation with domain ${\can N}$, with one binary operation whose interpretation is $+$ and one binary relation whose interpretation is $\leq$ can be written as $({\cal N},​+,​\leq)$. ​ This way we avoid writing $\alpha$ all the time, but it becomes more cumbersome to describe correspondence between structures.
 +
  
 ===== Examples ===== ===== Examples =====
Line 47: 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 53: 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 65: 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 76: 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 89: Line 93:
   &=& false   &=& false
 \end{array} \end{array}
-\]+\end{equation*}
 ++++ ++++
  
Line 97: 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 109: 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 120: 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 147: 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 156: 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 164: 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 178: 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*}
  
 
sav08/first-order_logic_semantics.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice