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:predicate_logic_informally [2008/02/20 15:38] vkuncak |
sav08:predicate_logic_informally [2008/02/20 15:41] vkuncak |
||
---|---|---|---|
Line 53: | Line 53: | ||
In general all quantifiers range over some universal domain $D$. To restrict them to subsets of $D$, we can use bounded quantifiers: | In general all quantifiers range over some universal domain $D$. To restrict them to subsets of $D$, we can use bounded quantifiers: | ||
- | * $\exists x \in S. P(x)$ means $\exists x. x \in S \and P(x)$ | + | * $\exists x \in S. P(x)$ means $\exists x. (x \in S \land P(x))$ |
- | * $\forall x \in S. P(x)$ means $\forall x. x \in S \rightarrow P(x)$ (note implication instead of conjunction) | + | * $\forall x \in S. P(x)$ means $\forall x. (x \in S \rightarrow P(x))$ (note implication instead of conjunction) |
More generally, if $\rho$ is some binary relation written in infix form, such as $<, \le, >, \ge$ we write | More generally, if $\rho$ is some binary relation written in infix form, such as $<, \le, >, \ge$ we write | ||
- | * $\exists x \rho t. P(x)$ meaning $\exists x. x \rho t \and P(x)$ | + | * $\exists x \mathop{\rho} t. P(x)$ meaning $\exists x. (x \mathop{\rho} t \land P(x))$ |
- | * $\forall x \rho t. P(x)$ means $\forall x. x \rho t \rightarrow P(x)$ (note implication instead of conjunction) | + | * $\forall x \mathop{\rho} t. P(x)$ means $\forall x. (x \mathop{\rho} t \rightarrow P(x))$ (note implication instead of conjunction) |
===== Evaluating First-Order Logic Formulas ===== | ===== Evaluating First-Order Logic Formulas ===== | ||
Line 115: | Line 115: | ||
(\lnot (\exists x. P(x))) \leftrightarrow (\forall x. (\lnot P(x)) \\ | (\lnot (\exists x. P(x))) \leftrightarrow (\forall x. (\lnot P(x)) \\ | ||
(\lnot (\forall x. P(x))) \leftrightarrow (\exists x. (\lnot P(x)) \\ | (\lnot (\forall x. P(x))) \leftrightarrow (\exists x. (\lnot P(x)) \\ | ||
+ | (\lnot (\exists x \rho t. P(x))) \leftrightarrow (\forall x \rho t. (\lnot P(x)) \\ | ||
+ | (\lnot (\forall x \rho t. P(x))) \leftrightarrow (\exists x \rho t. (\lnot P(x)) \\ | ||
(\forall x. (x=t \rightarrow F(x))) \leftrightarrow F(t) \\ | (\forall x. (x=t \rightarrow F(x))) \leftrightarrow F(t) \\ | ||
- | (\exists x. (x=t \land F(x))) \leftrightarrow F(t) \\ | + | (\exists x. (x=t \land F(x))) \leftrightarrow F(t) \\ |
\end{array}\] | \end{array}\] | ||