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:41] vkuncak |
sav08:predicate_logic_informally [2008/02/21 14:41] 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 100: | Line 102: | ||
| * There is //no algorithm// that given a first-order logic formula outputs "yes" when the formula is satisfiable and "no" otherwise - //finite satisfiability of first-order logic formulas is undecidable// | * There is //no algorithm// that given a first-order logic formula outputs "yes" when the formula is satisfiable and "no" otherwise - //finite satisfiability of first-order logic formulas is undecidable// | ||
| * There exists an enumeration procedure that systematically lists //all// finitely satisfiable formulas (and only finitely satisfiable formulas) - //finite satisfiability of first-order logic formulas is enumerable// | * There exists an enumeration procedure that systematically lists //all// finitely satisfiable formulas (and only finitely satisfiable formulas) - //finite satisfiability of first-order logic formulas is enumerable// | ||
| + | |||
| ===== Some Valid First-Order Logic Formulas ===== | ===== Some Valid First-Order Logic Formulas ===== | ||
| Line 108: | Line 111: | ||
| \[\begin{array}{l} | \[\begin{array}{l} | ||
| - | (\forall x. (P(x) \land Q(x)) \leftrightarrow ((\exists x. P(x)) \land (\exists 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))) \\ | ||
| (\exists x. (P(x) \lor Q(x)) \leftrightarrow ((\exists x. P(x)) \lor (\exists x. Q(x))) \\ | (\exists x. (P(x) \lor Q(x)) \leftrightarrow ((\exists x. P(x)) \lor (\exists x. Q(x))) \\ | ||