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:12]
vkuncak
sav08:first-order_logic_syntax [2008/03/24 11:36]
vkuncak
Line 69: Line 69:
  
 $FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows: $FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows:
-\[\begin{array}{l+\[\begin{array}{rcl
-  FV(x) = \{ x \}, \mbox{ for } x \in V \\ +  FV(x) &=\{ x \}, \mbox{ for } x \in V \\ 
-  FV(\lnot F) = FV(F) \\ +  FV(f(t_1,​\ldots,​t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\ 
-  FV(F_1 \land F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(R(t_1,​\ldots,​t_n)) &=& F(t_1) \cup \ldots \cup F(t_n) \\ 
-  FV(F_1 \lor F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(t_1 = t_2) &=& F(t_1) \cup F(t_2) ​\\ 
-  FV(F_1 \rightarrow F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(\lnot F) &=FV(F) \\ 
-  FV(F_1 \leftrightarrow F_2) = FV(F_1) \cup FV(F_2) \\ +  FV(F_1 \land F_2) &=FV(F_1) \cup FV(F_2) \\ 
-  FV(\forall x.F) = FV(F) \setminus \{x\} \\ +  FV(F_1 \lor F_2) &=FV(F_1) \cup FV(F_2) \\ 
-  FV(\exists x.F) = FV(F) \setminus \{x\} +  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(\forall 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//.