LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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))) \\