34 $(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as a binder |
34 $(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as a binder |
35 for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the |
35 for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the |
36 syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall |
36 syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall |
37 x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is |
37 x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is |
38 possible for any constant provided that $\tau$ and $\tau'$ are the same type. |
38 possible for any constant provided that $\tau$ and $\tau'$ are the same type. |
39 HOL's description operator $\varepsilon x.P\,x$ has type $(\alpha\To |
39 The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To |
40 bool)\To\alpha$ and can bind only one variable, except when $\alpha$ is |
40 bool)\To\alpha$ and normally binds only one variable. |
41 $bool$. ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a |
41 ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a |
42 binder because it has type $[i, i\To o]\To o$. The syntax for binders allows |
42 binder because it has type $[i, i\To o]\To o$. The syntax for binders allows |
43 type constraints on bound variables, as in |
43 type constraints on bound variables, as in |
44 \[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \] |
44 \[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \] |
45 |
45 |
46 To avoid excess detail, the logic descriptions adopt a semi-formal style. |
46 To avoid excess detail, the logic descriptions adopt a semi-formal style. |