Changes

As a purely informal aid to interpretation, I frequently use the letters <math>^{\backprime\backprime} p ^{\prime\prime}, ^{\backprime\backprime} q ^{\prime\prime}</math> to denote propositions.  This can serve to tip off the reader that a function is intended as the indicator function of a set, and thus it saves the trouble of declaring the type <math>f : X \to \underline\mathbb{B}</math> each time that a function is introduced as a proposition.

As a purely informal aid to interpretation, I frequently use the letters <math>^{\backprime\backprime} p ^{\prime\prime}, ^{\backprime\backprime} q ^{\prime\prime}</math> to denote propositions.  This can serve to tip off the reader that a function is intended as the indicator function of a set, and thus it saves the trouble of declaring the type <math>f : X \to \underline\mathbb{B}</math> each time that a function is introduced as a proposition.

Another convention of use in this context is to let underscored letters stand for <math>k\!</math>-tuples or sequences of objects.  Typically, the objects are all of one type, and typically the letter that is underscored is the same basic character that is indexed or subscripted, as in a list, to denote the individual components of the <math>k\!</math>-tuple or sequence.  For instance:

Another convention of use in this context is to let underscored letters stand for k-tuples or sequences of objects.  Typically, the objects are all of one type, and typically the letter that is underscored is the same basic character that is indexed or subscripted, as in a list, to denote the individual components of the k-tuple or sequence.  For instance:

1. If v1, ..., vk ? V, then v = <v1, ..., vk> ? V' = Vk.

2. If v1, ..., vk : V, then v = <v1, ..., vk> : V' = Vk.

3. If f1, ..., fk : U �> V, then f = <f1, ..., fk> : (U �> V)k.

\text{If} & x_1, \dots, x_k & \in & X &

\text{then} & \underline{x} = (x_1, \ldots, x_k) & \in & X^k.

\text{If} & x_1, \dots, x_k & : & X &

\text{then} & \underline{x} = (x_1, \ldots, x_k) & : & X^k.

\text{If} & f_1, \dots, f_k & : & X \to Y &

\text{then} & \underline{f} = (f_1, \ldots, f_k) & : & (X \to Y)^k.

There is usually felt to be a slight but significant distinction between the membership statement, that uses the sign "?" as in example (1), and the type statement, that uses the sign ":" as in examples (2) and (3).  The difference that is perceived in categorical statements, those of the form "v ? V" or "v : V", is that a multitude of objects can be said to have the same type without necessarily positing the existence of a set to which they all belong.  Without trying to decide whether I share this feeling or fully understand this distinction, I can only try to maintain a style of notation that respects it to some degree.  It is conceivable that the question of belonging to a set is rightly sensed to be the more serious issue, one that has to do with the reality of an object and the substance of a predicate, than the question of falling under a type, that has more to do with the way that a sign is intepreted and the way that information about an object is organized.  When it comes to the kinds of hypothetical statements that appear in the present instance, those of the form "v ? V => v ? V'" or "v : V => v : V'", these are usually read as implying some kind of synthesis, whose contingent consequences are the construction of a new space to contain the elements as compounded and the recognition of a new type to characterize the elements as listed, respectively.  In this application, the statement about types is again taken to be weaker than the corresponding statement about sets, since the apodosis is only meant to abbreviate and to summarize what is already stated in the protasis.

There is usually felt to be a slight but significant distinction between the membership statement, that uses the sign "?" as in example (1), and the type statement, that uses the sign ":" as in examples (2) and (3).  The difference that is perceived in categorical statements, those of the form "v ? V" or "v : V", is that a multitude of objects can be said to have the same type without necessarily positing the existence of a set to which they all belong.  Without trying to decide whether I share this feeling or fully understand this distinction, I can only try to maintain a style of notation that respects it to some degree.  It is conceivable that the question of belonging to a set is rightly sensed to be the more serious issue, one that has to do with the reality of an object and the substance of a predicate, than the question of falling under a type, that has more to do with the way that a sign is intepreted and the way that information about an object is organized.  When it comes to the kinds of hypothetical statements that appear in the present instance, those of the form "v ? V => v ? V'" or "v : V => v : V'", these are usually read as implying some kind of synthesis, whose contingent consequences are the construction of a new space to contain the elements as compounded and the recognition of a new type to characterize the elements as listed, respectively.  In this application, the statement about types is again taken to be weaker than the corresponding statement about sets, since the apodosis is only meant to abbreviate and to summarize what is already stated in the protasis.