12,080
edits
Changes
Directory:Jon Awbrey/Papers/Functional Logic : Inquiry and Analogy (view source)
Revision as of 01:36, 10 December 2008
, 01:36, 10 December 2008→Umpire Operators: restore omitted section
===Umpire Operators===
===Umpire Operators===
====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 : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}</math> and <math>\Upsilon : (\mathbb{B}^2 \to \mathbb{B}) \times (\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 as arguments and reports the value "true" if the first implies the second, otherwise "false".
<br>
<center>
<math>\Upsilon \langle e, f \rangle = 1 \quad \operatorname{iff} \quad e \Rightarrow f.</math>
</center>
<br>
Expressing it another way, we may also write:
<br>
<center>
<math>\Upsilon \langle e, f \rangle = 1 \quad \Leftrightarrow \quad (e (f)) = 1.</math>
</center>
<br>
In writing this, however, it is important to notice that the 1's appearing on the left and right have different meanings. Filling in the details, we have:
<br>
<center>
<math>\Upsilon \langle e, f \rangle = 1 \in \mathbb{B} \quad \Leftrightarrow \quad (e (f)) = 1 : \mathbb{B}^2 \to \mathbb{B}.</math>
</center>
<br>
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>
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:
<br>
<center>
<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>
</center>
<br>
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>[x, y],\!</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>
====Option 2 : More General====
In order to get a handle on the space of higher order propositions and eventually to carry out a functional approach to quantification theory, it serves to construct some specialized tools. Specifically, I define a higher order operator <math>\Upsilon,\!</math> called the ''umpire operator'', which takes up to three propositions as arguments and returns a single truth value as the result. Formally, this so-called ''multi-grade'' property of <math>\Upsilon\!</math> can be expressed as a union of function types, in the following manner:
In order to get a handle on the space of higher order propositions and eventually to carry out a functional approach to quantification theory, it serves to construct some specialized tools. Specifically, I define a higher order operator <math>\Upsilon,\!</math> called the ''umpire operator'', which takes up to three propositions as arguments and returns a single truth value as the result. Formally, this so-called ''multi-grade'' property of <math>\Upsilon\!</math> can be expressed as a union of function types, in the following manner: