Lab for Automated Reasoning and Analysis 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/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 =====
 
sav08/predicate_logic_informally.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice