LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:syntax_and_shorthands_of_hol [2009/03/05 13:08]
vkuncak
sav08:syntax_and_shorthands_of_hol [2015/04/21 17:30] (current)
Line 26: Line 26:
 Of course, some of the following defined notions could have been taken as primitive, but this shows that they can also be considered as shorthands if we wish to keep the basic system simple. ​ The definitions illustrate the expressive power of equality over functions: Of course, some of the following defined notions could have been taken as primitive, but this shows that they can also be considered as shorthands if we wish to keep the basic system simple. ​ The definitions illustrate the expressive power of equality over functions:
  
-\[\begin{array}{l@{\mbox{ stands for }}l}+\begin{equation*}\begin{array}{l@{\mbox{ stands for }}l}
 A \leftrightarrow B & A =_{o \Rightarrow o \Rightarrow o} B \\ A \leftrightarrow B & A =_{o \Rightarrow o \Rightarrow o} B \\
 true & (({=}_{o \Rightarrow o \Rightarrow o}) = ({=}_{o \Rightarrow o \Rightarrow o})) \\ true & (({=}_{o \Rightarrow o \Rightarrow o}) = ({=}_{o \Rightarrow o \Rightarrow o})) \\
Line 34: Line 34:
 \forall x. F &  (\lambda x. F) = (\lambda x. true) \\ \forall x. F &  (\lambda x. F) = (\lambda x. true) \\
 \end{array} \end{array}
-\]+\end{equation*}
 Note that we have defined negation, conjunction,​ and universal quantification,​ so all propositional operations and existential quantification are expressible. Note that we have defined negation, conjunction,​ and universal quantification,​ so all propositional operations and existential quantification are expressible.
  
 We can also treat $\forall$, $\exists$ as operators, with the understanding that $\forall x. F$ means $\forall (\lambda x.F)$. In that case, the meaning of $\forall$ is: We can also treat $\forall$, $\exists$ as operators, with the understanding that $\forall x. F$ means $\forall (\lambda x.F)$. In that case, the meaning of $\forall$ is:
-\[+\begin{equation*}
     \lambda g. (g = (\lambda x. true))     \lambda g. (g = (\lambda x. true))
-\]+\end{equation*}
 so that $\forall (\lambda x.F)$ evaluates to $(\lambda x.F) = (\lambda x. true)$. so that $\forall (\lambda x.F)$ evaluates to $(\lambda x.F) = (\lambda x. true)$.
  
  
 Note also that we can express Note also that we can express
-\[+\begin{equation*}
    ​\mbox{ let } x = E \mbox{ in } F    ​\mbox{ let } x = E \mbox{ in } F
-\]+\end{equation*}
 by $(\lambda x.F)E$.  ​ by $(\lambda x.F)E$.  ​
  
 The selection operator $\iota$ is not essential, but is a useful notation. ​ By writing The selection operator $\iota$ is not essential, but is a useful notation. ​ By writing
-\[+\begin{equation*}
    ​\mbox{ let } y = \iota(\lambda x. P(x)) \mbox{ in } F    ​\mbox{ let } y = \iota(\lambda x. P(x)) \mbox{ in } F
-\]+\end{equation*}
 we can express the phrase "let y in F denote the unique x such that P(x) holds"​. we can express the phrase "let y in F denote the unique x such that P(x) holds"​.