Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:syntax_and_shorthands_of_hol [2008/05/29 17:02] vkuncak |
sav08:syntax_and_shorthands_of_hol [2009/03/05 13:08] vkuncak |
||
---|---|---|---|
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 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 |