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 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 by 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 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.