12,080
edits
Changes
Directory:Jon Awbrey/Papers/Functional Logic : Quantification Theory (view source)
Revision as of 11:17, 15 December 2008
, 11:17, 15 December 2008move generalized umpire operators to appendix for now
===Umpire Operators===
===Umpire Operators===
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.
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.
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 version could have been defined as <math>\Upsilon_e f = \Upsilon \underline{(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 version could have been defined as <math>\Upsilon_e f = \Upsilon \underline{(e (f))}.\!</math>
====Option 2 : More General====
===Measure for Measure===
Define two families of measures:
{| align="center" cellpadding="8" style="text-align:center"
{| align="center" cellpadding="8"
| <math>\Upsilon : \bigcup_{\ell = 1, 2, 3} ((\mathbb{B}^k \to \mathbb{B})^\ell \to \mathbb{B}).</math>
| <math>\alpha_i, \beta_i : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}, i = 0 \ldots 15,</math>
|}
|}
by means of the following formulas:
{| align="center" cellpadding="8" style="text-align:center"
{| align="center" cellpadding="8"
| <math>\Upsilon_p^r q = \Upsilon (p, q, r)\!</math>
| <math>\alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f),</math>
|-
|-
| <math>\Upsilon_p^r : (\mathbb{B}^k \to \mathbb{B}) \to \mathbb{B}</math>
| <math>\beta_i f = \Upsilon (f, f_i) = \Upsilon (f \Rightarrow f_i).</math>
|}
|}
The intention of this operator is that we evaluate the proposition <math>q\!</math> on each model of the proposition <math>p\!</math> and combine the results according to the method indicated by the connective parameter <math>r.\!</math> In principle, the index <math>r\!</math> might specify any connective on as many as <math>2^k\!</math> arguments, but usually we have in mind a much simpler form of combination, most often either collective products or collective sums. By convention, each of the accessory indices <math>p, r\!</math> is assigned a default value that is understood to be in force when the corresponding argument place is left blank, specifically, the constant proposition <math>1 : \mathbb{B}^k \to \mathbb{B}</math> for the lower index <math>p,\!</math> and the continued conjunction or continued product operation <math>\textstyle\prod</math> for the upper index <math>r.\!</math> Taking the upper default value gives license to the following readings:
The values of the sixteen <math>\alpha_i\!</math> on each of the sixteen boolean functions <math>f : \mathbb{B}^2 \to \mathbb{B}</math> are shown in Table 4. Expressed in terms of the implication ordering on the sixteen functions, <math>\alpha_i f = 1\!</math> says that <math>f\!</math> is ''above or identical to'' <math>f_i\!</math> in the implication lattice, that is, <math>\ge f_i\!</math> in the implication ordering.
{| align="center" cellpadding="8" style="text-align:center"
{| align="center" border="1" cellpadding="1" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
| <math>\Upsilon_p (q) = \Upsilon (p, q) = \Upsilon (p, q, \textstyle\prod).</math>
|+ '''Table 4. Qualifiers of Implication Ordering: <math>\alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f)</math>'''
|-
|- style="background:ghostwhite"
| <math>\Upsilon_p = \Upsilon (p, \underline{~~}, \textstyle\prod) : (\mathbb{B}^k \to \mathbb{B}) \to \mathbb{B}.</math>
| align="right" | <math>u:</math><br><math>v:</math>
|}
| 1100<br>1010
| <math>f\!</math>
| <math>\alpha_0</math>
| <math>\alpha_1</math>
| <math>\alpha_2</math>
| <math>\alpha_3</math>
{| align="center" cellpadding="8" style="text-align:center"
| <math>\alpha_4</math>
| <math>\Upsilon q = \Upsilon (q) = \Upsilon_1 (q) = \Upsilon (1, q, \textstyle\prod).</math>
| <math>\alpha_5</math>
| <math>\alpha_6</math>
| <math>\alpha_7</math>
| <math>\alpha_8</math>
| <math>\alpha_9</math>
| <math>\alpha_{10}</math>
| <math>\alpha_{11}</math>
| <math>\alpha_{12}</math>
| <math>\alpha_{13}</math>
| <math>\alpha_{14}</math>
| <math>\alpha_{15}</math>
|-
|-
| <math>\Upsilon = \Upsilon (1, \underline{~~}, \textstyle\prod)) : (\mathbb{B}^k\ \to \mathbb{B}) \to \mathbb{B}.</math>
| <math>f_0</math>
|}
| 0000
| <math>(~)</math>
| style="background:black; color:white" | 1
| style="background:white; color:black" | 0
===Measure for Measure===
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| <math>\alpha_i, \beta_i : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}, i = 0 \ldots 15,</math>
| style="background:white; color:black" | 0
|}
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| <math>\alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f),</math>
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
|-
|-
| <math>\beta_i f = \Upsilon (f, f_i) = \Upsilon (f \Rightarrow f_i).</math>
| <math>f_1</math>
|}
| 0001
| <math>(u)(v)\!</math>
| style="background:black; color:white" | 1
| style="background:black; color:white" | 1
| style="background:white; color:black" | 0
|+ '''Table 4. Qualifiers of Implication Ordering: <math>\alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f)</math>'''
| style="background:white; color:black" | 0
|- style="background:ghostwhite"
| style="background:white; color:black" | 0
| align="right" | <math>u:</math><br><math>v:</math>
| 1100<br>1010
| style="background:black; color:white" | 1
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
| style="background:white; color:black" | 0
|-
|-
| <math>f_2</math>
| <math>f_2</math>
| 0010
| 0010
| <math>\ell_{11}\!</math>
| <math>\ell_{11}\!</math>
|}<br>
|}<br>
==Appendix : Generalized Umpire Operators==
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:
{| align="center" cellpadding="8" style="text-align:center"
| <math>\Upsilon : \bigcup_{\ell = 1, 2, 3} ((\mathbb{B}^k \to \mathbb{B})^\ell \to \mathbb{B}).</math>
|}
In contexts of application the intended sense can be discerned by the number of arguments that actually appear in the argument list. Often, the first and last arguments appear as indices, the one in the middle being treated as the main argument while the other two arguments serve to modify the sense of the operation in question. Thus, we have the following forms:
{| align="center" cellpadding="8" style="text-align:center"
| <math>\Upsilon_p^r q = \Upsilon (p, q, r)\!</math>
|-
| <math>\Upsilon_p^r : (\mathbb{B}^k \to \mathbb{B}) \to \mathbb{B}</math>
|}
The intention of this operator is that we evaluate the proposition <math>q\!</math> on each model of the proposition <math>p\!</math> and combine the results according to the method indicated by the connective parameter <math>r.\!</math> In principle, the index <math>r\!</math> might specify any connective on as many as <math>2^k\!</math> arguments, but usually we have in mind a much simpler form of combination, most often either collective products or collective sums. By convention, each of the accessory indices <math>p, r\!</math> is assigned a default value that is understood to be in force when the corresponding argument place is left blank, specifically, the constant proposition <math>1 : \mathbb{B}^k \to \mathbb{B}</math> for the lower index <math>p,\!</math> and the continued conjunction or continued product operation <math>\textstyle\prod</math> for the upper index <math>r.\!</math> Taking the upper default value gives license to the following readings:
{| align="center" cellpadding="8" style="text-align:center"
| <math>\Upsilon_p (q) = \Upsilon (p, q) = \Upsilon (p, q, \textstyle\prod).</math>
|-
| <math>\Upsilon_p = \Upsilon (p, \underline{~~}, \textstyle\prod) : (\mathbb{B}^k \to \mathbb{B}) \to \mathbb{B}.</math>
|}
This means that <math>\Upsilon_p (q) = 1\!</math> if and only if <math>q\!</math> holds for all models of <math>p.\!</math> In propositional terms, this is tantamount to the assertion that <math>p \Rightarrow q,</math> or that <math>\underline{(p (q))} = \underline{1}.</math>
Throwing in the lower default value permits the following abbreviations:
{| align="center" cellpadding="8" style="text-align:center"
| <math>\Upsilon q = \Upsilon (q) = \Upsilon_1 (q) = \Upsilon (1, q, \textstyle\prod).</math>
|-
| <math>\Upsilon = \Upsilon (1, \underline{~~}, \textstyle\prod)) : (\mathbb{B}^k\ \to \mathbb{B}) \to \mathbb{B}.</math>
|}
This means that <math>\Upsilon q = 1\!</math> if and only if <math>q\!</math> holds for the whole universe of discourse in question, that is, if and only <math>q\!</math> is the constantly true proposition <math>1 : \mathbb{B}^k \to \mathbb{B}.</math> The ambiguities of this usage are not a problem so long as we distinguish the context of definition from the context of application and restrict all shorthand notations to the latter.
==Readings==
==Readings==