Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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