Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:first-order_logic_syntax [2008/03/18 11:44] vkuncak |
sav08:first-order_logic_syntax [2008/03/24 11:36] vkuncak |
||
---|---|---|---|
Line 30: | Line 30: | ||
When in doubt, use parentheses. | When in doubt, use parentheses. | ||
- | Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with | + | Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with $ar(P) = 1$, $ar(Q) = 1$, $ar(R) = 2$, $ar(f) = 2$. Then |
- | \[\begin{array}{l} | + | |
- | ar(P) = 1 \\ | + | |
- | ar(Q) = 1 \\ | + | |
- | ar(R) = 2 \\ | + | |
- | ar(f) = 2 | + | |
- | \end{array} | + | |
- | \] | + | |
- | Then | + | |
\[ | \[ | ||
\lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x) | \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x) | ||
Line 77: | 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//. |