Differences

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

--- sav08:syntax_and_shorthands_of_hol [2008/05/29 17:02]
vkuncak
+++ sav08:syntax_and_shorthands_of_hol [2015/04/21 17:30] (current)
@@ Line 20: / Line 20: @@
 Everything else (most of mathematics) can be defined in this logic, and to a large extent has been done in systems such as Isabelle and HOL.
 ===== Defining Logical Functions =====
@@ Line 25: / 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:
-\[\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 \\
 true & (({=}_{o \Rightarrow o \Rightarrow o}) = ({=}_{o \Rightarrow o \Rightarrow o})) \\
@@ Line 33: / Line 34: @@
 \forall x. F &  (\lambda x. F) = (\lambda x. true) \\
 \end{array}
-\]
+\end{equation*}
 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:
+\begin{equation*}
+    \lambda g. (g = (\lambda x. true))
+\end{equation*}
+so that $\forall (\lambda x.F)$ evaluates to $(\lambda x.F) = (\lambda x. true)$.
 Note also that we can express
-\[
+\begin{equation*}
    \mbox{ let } x = E \mbox{ in } F
-\]
+\end{equation*}
 by $(\lambda x.F)E$.
 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
-\]
+\end{equation*}
 we can express the phrase "let y in F denote the unique x such that P(x) holds".