doc-src/Logics/syntax.tex
 changeset 14209 180cd69a5dbb parent 9695 ec7d7f877712 child 42637 381fdcab0f36
equal inserted replaced
14208:144f45277d5a 14209:180cd69a5dbb
    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.