summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/syntax.tex

changeset 14209 | 180cd69a5dbb |

parent 9695 | ec7d7f877712 |

child 42637 | 381fdcab0f36 |

equal
deleted
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. |