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:00] vkuncak |
sav08:syntax_and_shorthands_of_hol [2009/03/05 13:08] vkuncak |
||
|---|---|---|---|
| Line 17: | Line 17: | ||
| To obtain a logic based on such lambda calculus, we add two family of constants: | To obtain a logic based on such lambda calculus, we add two family of constants: | ||
| * equality $=_{t \Rightarrow t \Rightarrow o}$ for each type $t$, denoting equality on elements of type $t$ | * equality $=_{t \Rightarrow t \Rightarrow o}$ for each type $t$, denoting equality on elements of type $t$ | ||
| - | * selection operator $\iota_{(i \Rightarrow o) \Rightarrow o}$, denoting 'choice function' that takes a predicate and returns one element satisfying the predicate (if such element exists) | + | * selection operator $\iota_{(i \Rightarrow o) \Rightarrow i}$, denoting 'choice function' that takes a predicate and returns one element satisfying the predicate (if exactly one such element exists) |
| 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 35: | Line 36: | ||
| \] | \] | ||
| 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: | ||
| + | \[ | ||
| + | \lambda g. (g = (\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 | ||