Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:first-order_logic_syntax [2008/03/18 12:17] vkuncak |
sav08:first-order_logic_syntax [2008/03/19 10:24] vkuncak |
||
|---|---|---|---|
| Line 74: | Line 74: | ||
| 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//. |