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.  Doing this removes a longstanding but wholly unnecessary conceptual confound between the idea of an ''assertion'' and 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.  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 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.

<pre>

<pre>

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:

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: