Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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