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/20 15:46] vkuncak |
sav08:predicate_logic_informally [2010/02/22 14:00] vkuncak |
||
---|---|---|---|
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 102: | Line 103: | ||
* 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 110: | Line 112: | ||
\[\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))) \\ |