Syntax and Shorthands of HOL

We define HOL by introducing certain constants into Simply Typed Lambda Calculus and giving appropriate interpretations to them (through axioms or through semantics).

Types

We consider two base types:

the type 'i' of 'i'ndividuals
the type 'o' of truth values (the shorthand whose meaning to me is not 'o'bvious)

All types are built from i and o using function type constructor $\Rightarrow$ . For example,

binary functions are terms of type $i \Rightarrow i \Rightarrow i$ (arrow associates to the right, we use currying to represent functions with multiple arguments)
binary predicates are terms of type $i \Rightarrow i \Rightarrow o$

Logical 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$
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.

Defining Logical 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{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})) \\ false & ((\lambda x. true) = (\lambda x. x) \\ \lnot F & (F = false) \\ F_1 \land F_2 & (\lambda g.\ g\ true\ true) = (\lambda g.\ F_1\ F_2) \\ \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”.