Changes

Perhaps this looks like a lot of work for the sake of what seems to be such a trivial form of syntactic transformation, but it is an important step in loosening up the syntactic privileges that are held by the sign of logical equivalence <math>{}^{\backprime\backprime} \Leftrightarrow {}^{\prime\prime},</math> as written between logical sentences, and the sign of equality <math>{}^{\backprime\backprime} = {}^{\prime\prime},</math> as written between their logical values, or else between propositions and their boolean values, respectively.  Doing this removes a longstanding but wholly unnecessary conceptual confound between the idea of an ''assertion'' and the notion of an ''equation'', and it allows one to treat logical equality on a par with the other logical operations.

Perhaps this looks like a lot of work for the sake of what seems to be such a trivial form of syntactic transformation, but it is an important step in loosening up the syntactic privileges that are held by the sign of logical equivalence <math>{}^{\backprime\backprime} \Leftrightarrow {}^{\prime\prime},</math> as written between logical sentences, and the sign of equality <math>{}^{\backprime\backprime} = {}^{\prime\prime},</math> as written between their logical values, or else between propositions and their boolean values, respectively.  Doing this removes a longstanding but wholly unnecessary conceptual confound between the idea of an ''assertion'' and the notion of an ''equation'', and it allows one to treat logical equality on a par with the other logical operations.

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 it saves us 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 us 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, lists, or sequences of objects.  Typically, the elements of the <math>k\!</math>-tuple, list, or sequence are all of one type, and the underscored letter is typically the same basic character as the letters that are indexed or subscripted to denote the individual components of the <math>k\!</math>-tuple, list, or sequence.  When the dimension of the <math>k\!</math>-tuple, list, or sequence is clear from context, the underscoring may be omitted.  For example, the following patterns of construction are very often seen:

 

Another convention of use in this context is to let underscored letters stand for <math>k\!</math>-tuples, lists, or sequences of objects.  Typically, the elements of the <math>k\!</math>-tuple, list, or sequence are all of one type, and the underscored letter is typically of the same basic character as the letters that are indexed or subscripted to denote the individual components of the <math>k\!</math>-tuple, list, or sequence.  When the dimension of the <math>k\!</math>-tuple, list, or sequence is clear from context, the underscoring may be omitted.  By way of example, the following patterns of construction are very often seen:

{| align="center" cellpadding="8" width="90%"

{| align="center" cellpadding="8" width="90%"