- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

Both sides previous revision Previous revision Next revision | Previous revision | ||

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. | 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 ===== | ===== 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: | 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 33: | 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: | ||

+ | \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 | 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". | ||