Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:predicate_logic_informally [2008/02/21 14:41] vkuncak |
sav08:predicate_logic_informally [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 11: | Line 11: | ||
* quantifiers "forall" ($\forall$), "exists" ($\exists$) | * quantifiers "forall" ($\forall$), "exists" ($\exists$) | ||
- | Uses of first-order logic: | + | ===== Uses of first-order logic ===== |
* precisely describe arbitrary mathematical statements (theorems, conjectures, properties) | * precisely describe arbitrary mathematical statements (theorems, conjectures, properties) | ||
* specify program properties | * specify program properties | ||
Line 32: | Line 33: | ||
For a given value of variables, each formula evaluates to //true// or //false//. The rules for propositional operators are exactly as in [[Propositional Logic Informally|propositional logic]]. Quantifiers can be seen as a way of generalizing conjunction and disjunction. First-order variables range over some domain $D$. In the special case of finite domain $D = \{d_1,\ldots,d_k\}$, we have that | For a given value of variables, each formula evaluates to //true// or //false//. The rules for propositional operators are exactly as in [[Propositional Logic Informally|propositional logic]]. Quantifiers can be seen as a way of generalizing conjunction and disjunction. First-order variables range over some domain $D$. In the special case of finite domain $D = \{d_1,\ldots,d_k\}$, we have that | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
(\forall x. P(x)) \ \leftrightarrow\ P(d_1) \land \ldots \land P(d_k) \\ | (\forall x. P(x)) \ \leftrightarrow\ P(d_1) \land \ldots \land P(d_k) \\ | ||
(\exists x. P(x)) \ \leftrightarrow\ P(d_1) \lor \ldots \lor P(d_2) \\ | (\exists x. P(x)) \ \leftrightarrow\ P(d_1) \lor \ldots \lor P(d_2) \\ | ||
- | \end{array}\] | + | \end{array}\end{equation*} |
which corresponds to the intuitive definition of terms "for all" and "there exists". Note, however, that $D$ can be infinite in general (for example: the set of integers or reals). | which corresponds to the intuitive definition of terms "for all" and "there exists". Note, however, that $D$ can be infinite in general (for example: the set of integers or reals). | ||
Line 110: | Line 111: | ||
But there are many other valid formulas. Such formulas are valid laws of thinking that we often use in mathematics (explicitly, or implicitly without mentioning them). | But there are many other valid formulas. Such formulas are valid laws of thinking that we often use in mathematics (explicitly, or implicitly without mentioning them). | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
(\forall x. (P(x) \land Q(x)) \leftrightarrow ((\forall x. P(x)) \land (\forall x. Q(x))) \\ | (\forall x. (P(x) \land Q(x)) \leftrightarrow ((\forall x. P(x)) \land (\forall x. Q(x))) \\ | ||
(\exists x. (P(x) \land Q(x)) \rightarrow ((\exists x. P(x)) \land (\exists x. Q(x))) \\ | (\exists x. (P(x) \land Q(x)) \rightarrow ((\exists x. P(x)) \land (\exists x. Q(x))) \\ | ||
Line 122: | Line 123: | ||
(\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}\end{equation*} |
===== More information ===== | ===== More information ===== |