12,080
edits
Changes
Directory:Jon Awbrey/Papers/Functional Logic : Quantification Theory (view source)
Revision as of 13:40, 9 December 2008
, 13:40, 9 December 2008→Umpire Operators: restoring section on option 1 : less general approach from original document ...
===Umpire Operators===
===Umpire Operators===
====Option 1 : Less General Approach====
====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.
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.
====Option 2 : More General Approach====
The relative operator takes two propositions as arguments and reports the value "true" if the first implies the second, otherwise "false".
<center>
<math>\Upsilon \langle e, f \rangle = 1 \quad \operatorname{iff} \quad e \Rightarrow f.</math>
</center>
Expressing it another way, we may also write:
<center>
<math>\Upsilon \langle e, f \rangle = 1 \quad \Leftrightarrow \quad (e (f)) = 1.</math>
</center>
====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: