| Line 92: |
Line 92: |
| | | | |
| | <pre> | | <pre> |
| − | 1.3.10.3 Propositions & Sentences (cont.)
| |
| − |
| |
| − | As a purely informal aid to interpretation, I frequently use the letters
| |
| − | "p", "q" to denote propositions. This can serve to tip off the reader
| |
| − | that a function is intended as the indicator function of a set, and
| |
| − | it saves us the trouble of declaring the type f : X -> %B% each
| |
| − | time that a function is introduced as a proposition.
| |
| − |
| |
| − | Another convention of use in this context is to let boldface letters
| |
| − | stand for k-tuples, lists, or sequences of objects. Typically, the
| |
| − | elements of the k-tuple, list, or sequence are all of one type, and
| |
| − | typically the boldface letter is of the same basic character as the
| |
| − | indexed or subscripted letters that are used denote the components
| |
| − | of the k-tuple, list, or sequence. When the dimension of elements
| |
| − | and functions is clear from the context, we may elect to drop the
| |
| − | bolding of characters that name k-tuples, lists, and sequences.
| |
| − |
| |
| − | For example:
| |
| − |
| |
| − | 1. If x_1, ..., x_k in X, then #x# = <x_1, ..., x_k> in X' = X^k.
| |
| − |
| |
| − | 2. If x_1, ..., x_k : X, then #x# = <x_1, ..., x_k> : X' = X^k.
| |
| − |
| |
| − | 3. If f_1, ..., f_k : X -> Y, then #f# = <f_1, ..., f_k> : (X -> Y)^k.
| |
| − |
| |
| | There is usually felt to be a slight but significant distinction between | | There is usually felt to be a slight but significant distinction between |
| | the "membership statement" that uses the sign "in" as in Example (1) and | | the "membership statement" that uses the sign "in" as in Example (1) and |