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:39] vkuncak |
sav08:predicate_logic_informally [2008/02/20 15:46] vkuncak |
||
|---|---|---|---|
| Line 48: | Line 48: | ||
| * if $t_1,\ldots,t_n$ are terms and $f$ is a function symbol that takes $n$ arguments, then $f(t_1,\ldots,t_n)$ is also a term. | * if $t_1,\ldots,t_n$ are terms and $f$ is a function symbol that takes $n$ arguments, then $f(t_1,\ldots,t_n)$ is also a term. | ||
| Example of constants are numerals for natural numbers, such as $0, 1, 2, \ldots$. Examples of function symbols are operations such as $+, -, /$. | Example of constants are numerals for natural numbers, such as $0, 1, 2, \ldots$. Examples of function symbols are operations such as $+, -, /$. | ||
| + | |||
| + | From above we see that the set of formulas depends on the set of predicate and function symbols. This set is is called //vocabulary// or //language//. | ||
| ==== Bounded Quantifiers ==== | ==== Bounded Quantifiers ==== | ||
| Line 53: | Line 55: | ||
| 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 ===== | ||