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]
Line 1: Line 1:
-====== First-Order Logic Semantics ====== 
- 
-(Recall [[First-Order Logic Syntax]] and [[Propositional Logic Semantics]] as well as [[Predicate Logic Informally]].) 
- 
-An interpretation for first-order logic language ${\cal L}$ is the pair $I = (D,\alpha)$ where $D$ is a //​nonempty//​ set, called the //domain// of interpretation,​ and $\alpha$ is the //​interpretation function//, which assigns 
-  * to each first-order variable $x \in V$, an element $\alpha(x) \in D$ 
-  * to each relation symbol $R \in {\cal L}$ with arity $ar(R)=n$, a relation $\alpha(R) \subseteq D^n$ 
-  * to each function symbol $f \in {\cal L}$ with arity $ar(f)=n$, a function $\alpha(f) : D^n \to D$ 
-If $I=(D,​\alpha)$ we denote $D$ by $D_I$ and $\alpha$ by $\alpha_I$. 
- 
-Because terms denote values from domain $D_I$ and formulas denote truth values from ${\cal B} = \{{\it false}, {\it true}\}$, we define two semantic evaluation functions: 
-  * $e_F : {\cal F} \to I \to {\cal B}$ 
-  * $e_T : {\cal T} \to I \to D_I$ 
- 
-We evaluate terms by recursion on the structure of $T$: 
-\[ 
-\begin{array}{rcl} 
-  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)) ​ 
-\end{array} ​ 
-\] 
-We evaluate formulas by recursion on the structure of $F$: 
-\[ 
-\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(t_1 = t_2)(I) &=& (e_T(t_1)(I) = e_T(t_2)(I)) \\ 
-  e_F(F_1 \land F_2)(I) &=& e_F(F_1)(I) \land e_F(F_2)(I) \\ 
-  e_F(F_1 \lor F_2)(I) &=& e_F(F_1)(I) \lor e_F(F_2)(I) \\ 
-  e_F(\lnot F)(I) &=& \lnot e_F(F)(I) \\ 
-\end{array} ​ 
-\] 
-++++How do we evaluate quantifiers?​| 
-\[\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(\forall x.F)((D_I,​\alpha_I)) &=& (\forall d \in D_I.\ e_F(F)((D_I,​\alpha_I[x \mapsto d])) 
-\end{array} 
-\] 
-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)$. 
- 
-===== Examples ===== 
- 
- 
-==== Example with Finite Domain ==== 
- 
-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} 
-  D &=& \{ 0,1, 2 \} \\ 
-  \alpha(x) &=& 1 \\ 
-  \alpha(s) &=& \{ (0,1), (1,2), (2,0) \} \\ 
-  \alpha({<​}) &=& \{ (0,1), (0,2), (1,2) \}  
-\end{array} 
-\] 
- 
-Let us evaluate the truth value of these formulas: 
-  * $x < s(x)$ 
-++++answer| 
-\[\begin{array}{rcl} 
-  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(<​) \\ 
-  &=& (1,​\alpha(s)(1)) \in \alpha(<​) \\ 
-  &=& (1,2) \in \alpha(<​) \\ 
-  &=& true 
-\end{array} 
-\] 
-++++ 
-  * $\exists x. \lnot (x < s(x))$ 
-++++answer| 
-\[\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]))\\ 
-  &=& \exists d \in D.\ \neg e_F((x < s(x))(I[x \mapsto d])\\ 
-  &=& \exists d \in D.\ (d, \alpha(s)(d)) \notin \alpha(<​)\\ 
-  &=& (2,0)\notin \alpha(<​)\\ 
-  &=& true 
-\end{array} 
-\] 
-++++ 
-  * $\forall x. \exists y. x < y$ 
-++++answer| 
-\[\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]))\\ 
-  &=& \forall d \in D.\ e_F(\exists y. x < y)(I[x \mapsto d])\\ 
-  &=& \forall d \in D.\ \exists e \in D. e_F(x < y)(I[x \mapsto d][y \mapsto e])\\ 
-  &=& \forall d \in D.\ \exists e \in D. (d,e) \in \alpha(<​) \\ 
-  &=& \exists e \in D. (2,e) \in \alpha(<​) \\ 
-  &=& ((2,0) \in \alpha(<​)) \vee ((2,1) \in \alpha(<​)) \vee ((2,2) \in \alpha(<​))\\ 
-  &=& false 
-\end{array} 
-\] 
-++++ 
- 
- 
- 
-==== Example with Infinite Domain ==== 
- 
-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 \} 
-\] 
-What is the truth value of this formula 
-\[ 
-    \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 ==== 
- 
-Let $I=(D,​\alpha)$ be an arbitrary interpretation. ​ Consider formula 
-\[ 
-    (\forall x. P(x)) \rightarrow (\exists y. P(y)) 
-\] 
-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?"​. 
- 
- 
-===== Satisfiability,​ Validity, and Semantic Consequence ===== 
- 
-**Definition (satisfiability of set)**: If $T$ is a set of formulas, a //model of// $T$ is an interpretation such that $e_S(T)$. ​ A set $T$ of first-order formulas is //​satisfiable//​ if there exists a model for $T$.  A set $T$ is //​unsatisfiable (contradictory)//​ iff it is not satisfiable (it has no model). 
- 
-Note: taking $T = \{F\}$ we obtain notion of satisfiability for formulas. 
- 
-**Definition (semantic consequence)**:​ We say that a set of formulas $T_2$ is a //semantic consequence//​ of a set of formulas $T_1$ and write $T_1 \models T_2$, iff every model of $T_1$ is also a model of $T_2$. 
- 
-**Definition**:​ Formula is valid, denoted $\models F$ iff $\emptyset \models F$. 
- 
-**Lemma**: $\models F$ iff for every interpretation $I$ we have $e_F(F)(I)$. 
- 
-**Lemma**: A set $T$ of formulas is unsatisfiable iff $T \models {\it false}$. 
- 
-**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:| 
-\[ 
-\begin{array}{rcl} 
-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)(I)) \\ 
-            & \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) \\ 
-            & \leftrightarrow & \lnot \exists I. e_S(T \cup \{\lnot G\})(I) 
-\end{array} 
-\] 
-++++ 
- 
-One of the central questions is the study of whether a set of formulas is contradictory,​ many basic questions reduce to this problem. 
- 
-==== Consequence Set ==== 
- 
-**Definition**:​ The set of all consequences of $T$: 
-\[ 
-   ​Conseq(T) = \{ F \mid T \models F \} 
-\] 
- 
-Note $T \models F$ is equivalent to $F \in Conseq(T)$. 
- 
-**Lemma**: The following properties hold: 
-\[ 
-\begin{array}{rcl} 
-  T &​\subseteq & Conseq(T) \\ 
-  T_1 \subseteq T_2 &​\rightarrow&​ Conseq(T_1) \subseteq Conseq(T_2) \\ 
-  Conseq(Conseq(T)) &=& Conseq(T) ​ \\ 
-  T_1 \subseteq Conseq(T_2) \land T_2 \subseteq Conseq(T_1) & \rightarrow & Conseq(T_1) = Conseq(T_2) 
-\end{array} 
-\]