Changes

====Option 1 : Less General====

====Option 1 : Less General====

We now examine measures at the high end of the standard ordering.  Instrumental to this purpose we define a couple of higher order operators, <math>\Upsilon_1 : (X \to \mathbb{B}) \to \mathbb{B}</math> and <math>\Upsilon : (X \to \mathbb{B}) \times (X \to \mathbb{B}) \to \mathbb{B},</math> both symbolized by cursive upsilon characters and referred to as the absolute and relative "umpire operators", respectively.  If either one of these operators is defined in terms of more primitive notions then the remaining operator can be defined in terms of the one first established.

We now examine measures at the high end of the standard ordering.  Instrumental to this purpose we define a couple of higher order operators, <math>\Upsilon_1 : (X_{\mathbb{B}^2} \to \mathbb{B}) \to \mathbb{B}</math> and <math>\Upsilon : (X_{\mathbb{B}^2} \to \mathbb{B}) \times (X_{\mathbb{B}^2} \to \mathbb{B}) \to \mathbb{B},</math> both symbolized by cursive upsilon characters and referred to as the absolute and relative "umpire operators", respectively.  If either one of these operators is defined in terms of more primitive notions then the remaining operator can be defined in terms of the one first established.

The relative operator takes two propositions of type <math>X \to \mathbb{B}</math> as arguments and reports the value 1 if the first implies the second, otherwise 0.

The relative operator takes two propositions of type <math>X_{\mathbb{B}^2} \to \mathbb{B}</math> as arguments and reports the value 1 if the first implies the second, otherwise 0.

{| align="center" cellpadding="8"

{| align="center" cellpadding="8"

|}

|}

Finally, it is often convenient to write the first argument as a subscript, hence <math>\Upsilon_e \langle f \rangle = \Upsilon \langle e, f \rangle.</math>

Finally, it is often convenient to write the first argument as a subscript, hence <math>\Upsilon_e (f) = \Upsilon (e, f).\!</math>

As a special application of this operator, we next define the absolute umpire operator, also called the "umpire measure".  This is a higher order proposition <math>\Upsilon_1 : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}</math> which is given by the relation <math>\Upsilon_1 \langle f \rangle = \Upsilon \langle 1, f \rangle.</math>  Here, the subscript "1" on the left and the argument "1" on the right both refer to the constant proposition <math>1 : \mathbb{B}^2 \to \mathbb{B}.</math>  In most contexts where <math>\Upsilon_1\!</math> is actually applied the reference to "1" is safely omitted, since the number of arguments indicates which type of operator is intended.  Thus, we have the following identities and equivalents:

As a special application of this operator, we next define the absolute umpire operator, also called the ''umpire measure''.  This is a higher order proposition <math>\Upsilon_1 : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}</math> which is given by the relation <math>\Upsilon_1 \langle f \rangle = \Upsilon \langle 1, f \rangle.</math>  Here, the subscript "1" on the left and the argument "1" on the right both refer to the constant proposition <math>1 : \mathbb{B}^2 \to \mathbb{B}.</math>  In most contexts where <math>\Upsilon_1\!</math> is actually applied the reference to "1" is safely omitted, since the number of arguments indicates which type of operator is intended.  Thus, we have the following identities and equivalents:

{| align="center" cellpadding="8"

{| align="center" cellpadding="8"