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_syntax [2008/03/18 12:17]
vkuncak
sav08:first-order_logic_syntax [2008/03/24 11:36]
vkuncak
Line 71: Line 71:
 \[\begin{array}{rcl} \[\begin{array}{rcl}
   FV(x) &=& \{ x \}, \mbox{ for } x \in V \\   FV(x) &=& \{ x \}, \mbox{ for } x \in V \\
-  FV(f(t_1,​\ldots,​t_n) &=& F(t_1) \cup \ldots \cup F(t_n) \\ +  FV(f(t_1,​\ldots,​t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\ 
-  FV(R(t_1,​\ldots,​t_n) &=& F(t_1) \cup \ldots \cup F(t_n) \\+  FV(R(t_1,​\ldots,​t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\
   FV(t_1 = t_2) &=& F(t_1) \cup F(t_2) \\   FV(t_1 = t_2) &=& F(t_1) \cup F(t_2) \\
-  FV(\lnot F) = FV(F) \\ +  FV(\lnot F) &=FV(F) \\ 
-  FV(F_1 \land F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(F_1 \land F_2) &=FV(F_1) \cup FV(F_2) \\ 
-  FV(F_1 \lor F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(F_1 \lor F_2) &=FV(F_1) \cup FV(F_2) \\ 
-  FV(F_1 \rightarrow F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(F_1 \rightarrow F_2) &=FV(F_1) \cup FV(F_2) \\ 
-  FV(F_1 \leftrightarrow F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(F_1 \leftrightarrow F_2) &=FV(F_1) \cup FV(F_2) \\ 
-  FV(\forall x.F) = FV(F) \setminus \{x\} \\ +  FV(\forall x.F) &=FV(F) \setminus \{x\} \\ 
-  FV(\exists x.F) = FV(F) \setminus \{x\} +  FV(\exists x.F) &=FV(F) \setminus \{x\} 
 \end{array}\] \end{array}\]
  
-If $FV(F) = \emptyset$, we call $F$ a //closed formula//.+If $FV(F) = \emptyset$, we call $F$ a //​closed ​first-order logic formula//, or //sentence//.