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_{\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.

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 : (\langle u, v \rangle \to \mathbb{B}) \to \mathbb{B}</math> and <math>\Upsilon : (\langle u, v \rangle \to \mathbb{B})^2 \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_{\mathbb{B}^2} \to \mathbb{B}</math> as arguments and reports the value 1 if the first implies the second, otherwise 0.

Given an ordered pair of propositions <math>p, q : \langle u, v \rangle \to \mathbb{B}</math> as arguments, the relative operator reports the value 1 if the first implies the second, otherwise 0.

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

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

| <math>\Upsilon (e, f) = 1\!</math>

| <math>\Upsilon (p, q) = 1\!</math>

| <math>\operatorname{if~and~only~if}</math>

| <math>\operatorname{if~and~only~if}</math>

| <math>e \Rightarrow f.\!</math>

| <math>p \Rightarrow q.\!</math>

|}

|}

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

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

| <math>\Upsilon (e, f) = 1\!</math>

| <math>\Upsilon (p, q) = 1\!</math>

| <math>\Leftrightarrow</math>

| <math>\Leftrightarrow</math>

| <math>\underline{(e (f))} = \underline{1}.</math>

| <math>\underline{(p (q))} = \underline{1}.</math>

|}

|}

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

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

| <math>\Upsilon (e, f) = 1 \in \mathbb{B}</math>

| <math>\Upsilon (p, q) = 1 \in \mathbb{B}</math>

| <math>\Leftrightarrow</math>

| <math>\Leftrightarrow</math>

| <math>\underline{(e (f))} = 1 : X \to \mathbb{B}.</math>

| <math>\underline{(p (q))} = 1 : \langle u, v \rangle \to \mathbb{B}.</math>

|}

|}

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

Writing types as subscripts and using the fact that <math>X = \langle u, v \rangle,</math> it is possible to express this a little more succinctly as follows:

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 (p) = \Upsilon (1, p).\!</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"

| <math>\Upsilon f = \Upsilon_1 \langle f \rangle = 1 \in \mathbb{B} \quad \Leftrightarrow \quad (1 (f)) = 1 \quad \Leftrightarrow \quad f = 1 : \mathbb{B}^2 \to \mathbb{B}.</math>

| <math>\Upsilon p = \Upsilon_1 (p) = 1 \in \mathbb{B} \quad \Leftrightarrow \quad (1 (p)) = 1 \quad \Leftrightarrow \quad p = 1 : \mathbb{B}^2 \to \mathbb{B}.</math>

|}

|}

The umpire measure is defined at the level of truth functions, but can also be understood in terms of its implied judgments at the syntactic level.  Interpreted this way, <math>\Upsilon_1\!</math> recognizes theorems of the propositional calculus over <math>[u, v],\!</math> giving a score of "1" to tautologies and a score of "0" to everything else, regarding all contingent statements as no better than falsehoods.

The umpire measure is defined at the level of truth functions, but can also be understood in terms of its implied judgments at the syntactic level.  Interpreted this way, <math>\Upsilon_1\!</math> recognizes theorems of the propositional calculus over <math>[u, v],\!</math> giving a score of "1" to tautologies and a score of "0" to everything else, regarding all contingent statements as no better than falsehoods.

One remark in passing for those who might prefer an alternative definition.  If we had originally taken <math>\Upsilon\!</math> to mean the absolute measure, then the relative vesrion could have been defined as <math>\Upsilon_e f = \Upsilon (e (f)).\!</math>

One remark in passing for those who might prefer an alternative definition.  If we had originally taken <math>\Upsilon\!</math> to mean the absolute measure, then the relative vesrion could have been defined as <math>\Upsilon_p q = \Upsilon (p (q)).\!</math>

====Option 2 : More General====

====Option 2 : More General====