12,080
edits
Changes
Directory:Jon Awbrey/Papers/Functional Logic : Quantification Theory (view source)
Revision as of 22:33, 17 November 2008
, 22:33, 17 November 2008HTML → TeX
|-
|-
| ''F<sub>3</sub> || 1 1 || 1 ||0||0||0||0||0||0||0||0||1||1||1||1||1||1||1||1
| ''F<sub>3</sub> || 1 1 || 1 ||0||0||0||0||0||0||0||0||1||1||1||1||1||1||1||1
|}<br>
|}
I am going to put off explaining Table 2, that presents a sample of what I call ''interpretive categories'' for higher order propositions, until after we get beyond the 1-dimensional case, since these lower dimensional cases tend to be a bit ''condensed'' or ''degenerate'' in their structures, and a lot of what is going on here will almost automatically become clearer as soon as we get even two logical variables into the mix.
I am going to put off explaining Table 2, that presents a sample of what I call ''interpretive categories'' for higher order propositions, until after we get beyond the 1-dimensional case, since these lower dimensional cases tend to be a bit ''condensed'' or ''degenerate'' in their structures, and a lot of what is going on here will almost automatically become clearer as soon as we get even two logical variables into the mix.
|-
|-
|''m''<sub>15</sub>||anything happens|| || || || ||
|''m''<sub>15</sub>||anything happens|| || || || ||
|}<br>
|}
====Higher Order Propositions and Logical Operators (''n'' = 2)====
====Higher Order Propositions and Logical Operators (''n'' = 2)====
|
|
| <math>X^\uparrow = (X \to \mathbb{B}) = \{ f : X \to \mathbb{B} \} \cong (\mathbb{B}^2 \to \mathbb{B}).</math>
| <math>X^\uparrow = (X \to \mathbb{B}) = \{ f : X \to \mathbb{B} \} \cong (\mathbb{B}^2 \to \mathbb{B}).</math>
|}<br>
|}
As always, it is frequently convenient to omit a few of the finer markings of distinctions among isomorphic structures, so long as one is aware of their presence and knows when it is crucial to call upon them again.
As always, it is frequently convenient to omit a few of the finer markings of distinctions among isomorphic structures, so long as one is aware of their presence and knows when it is crucial to call upon them again.
The next higher order universe of discourse that is built on <math>X^\circ</math> is <math>X^{\circ 2} = [X^\circ] = [[x, y]],</math> which may be developed in the following way. The propositions of <math>X^\circ</math> become the points of <math>X^{\circ 2},</math> and the mappings of the type <math>m : (X \to \mathbb{B}) \to \mathbb{B}</math> become the propositions of <math>X^{\circ 2}.</math> In addition, it is convenient to equip the discussion with a selected set of higher order operators on propositions, all of which have the form <math>w : (\mathbb{B}^2 \to \mathbb{B})^k \to \mathbb{B}.</math>
The next higher order universe of discourse that is built on <math>X^\circ</math> is <math>X^{\circ 2} = [X^\circ] = [[x, y]],</math> which may be developed in the following way. The propositions of <math>X^\circ</math> become the points of <math>X^{\circ 2},</math> and the mappings of the type <math>m : (X \to \mathbb{B}) \to \mathbb{B}</math> become the propositions of <math>X^{\circ 2}.</math> In addition, it is convenient to equip the discussion with a selected set of higher order operators on propositions, all of which have the form <math>w : (\mathbb{B}^2 \to \mathbb{B})^k \to \mathbb{B}.</math>
To save a few words in the remainder of this discussion, I will use the terms "measure" and "qualifier" to refer to all types of higher order propositions and operators. To describe the present setting in picturesque terms, the propositions of [''x'', ''y''] may be regarded as a gallery of sixteen venn diagrams, while the measures ''m'' : (''X'' → '''B''') → '''B''' are analogous to a body of judges or a panel of critical viewers, each of whom evaluates each of the pictures as a whole and reports the ones that find favor or not. In this way, each judge m_j partitions the gallery of pictures into two aesthetic portions, the pictures (''m''<sub>''j''</sub>)<sup>–1</sup>(1) that ''m''<sub>''j''</sub> likes and the pictures (''m''<sub>''j''</sub>)<sup>–1</sup>(0) that ''m''<sub>''j''</sub> dislikes.
To save a few words in the remainder of this discussion, I will use the terms ''measure'' and ''qualifier'' to refer to all types of higher order propositions and operators. To describe the present setting in picturesque terms, the propositions of <math>[x, y]\!</math> may be regarded as a gallery of sixteen venn diagrams, while the measures <math>m : (X \to \mathbb{B}) \to \mathbb{B}</math> are analogous to a body of judges or a panel of critical viewers, each of whom evaluates each of the pictures as a whole and reports the ones that find favor or not. In this way, each judge <math>m_j\!</math> partitions the gallery of pictures into two aesthetic portions, the pictures <math>m_j^{-1}(1)\!</math> that <math>m_j\!</math> likes and the pictures <math>m_j^{-1}(0)\!</math> that <math>m_j\!</math> dislikes.
There are 2<sup>16</sup> = 65536 measures of the type ''m'' : ('''B'''<sup>2</sup> → '''B''') → '''B'''. Table 3 introduces the first 24 of these measures in the fashion of the higher order truth table that I used before. The column headed "''m''<sub>''j''</sub>" shows the values of the measure ''m''<sub>''j''</sub> on each of the propositions ''f''<sub>''i''</sub> : '''B'''<sup>2</sup> → '''B''', for ''i'' = 0 to 23, with blank entries in the Table being optional for values of zero. The arrangement of measures that continues according to the plan indicated here is referred to as the "standard ordering" of these measures. In this scheme of things, the index ''j'' of the measure ''m''<sub>''j''</sub> is the decimal equivalent of the bit string that is associated with ''m''<sub>''j''</sub>'s functional values, which can be obtained in turn by reading the ''j''<sup>th</sup> column of binary digits in the Table as the corresponding range of boolean values, taking them up in the order from bottom to top.
There are 2<sup>16</sup> = 65536 measures of the type ''m'' : ('''B'''<sup>2</sup> → '''B''') → '''B'''. Table 3 introduces the first 24 of these measures in the fashion of the higher order truth table that I used before. The column headed "''m''<sub>''j''</sub>" shows the values of the measure ''m''<sub>''j''</sub> on each of the propositions ''f''<sub>''i''</sub> : '''B'''<sup>2</sup> → '''B''', for ''i'' = 0 to 23, with blank entries in the Table being optional for values of zero. The arrangement of measures that continues according to the plan indicated here is referred to as the "standard ordering" of these measures. In this scheme of things, the index ''j'' of the measure ''m''<sub>''j''</sub> is the decimal equivalent of the bit string that is associated with ''m''<sub>''j''</sub>'s functional values, which can be obtained in turn by reading the ''j''<sup>th</sup> column of binary digits in the Table as the corresponding range of boolean values, taking them up in the order from bottom to top.
| || || || || || || ||
| || || || || || || ||
|}
|}
===Umpire Operators===
===Umpire Operators===
| 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1
| 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1
| 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1
| 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1
|}
|}<br>
<br>
{| align="center" border="1" cellpadding="0" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%"
{| align="center" border="1" cellpadding="0" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%"
| || || || || || || || 1
| || || || || || || || 1
|}
|}
Applied to a given proposition ''f'', the qualifiers α<sub>''i''</sub> and β<sub>''i''</sub> tell whether ''f'' rests "above ''f''<sub>''i''</sub>" or "below ''f''<sub>''i''</sub>", respectively, in the implication ordering. By way of example, let us trace the effects of several such measures, namely, those that occupy the limiting positions of the Tables.
Applied to a given proposition ''f'', the qualifiers α<sub>''i''</sub> and β<sub>''i''</sub> tell whether ''f'' rests "above ''f''<sub>''i''</sub>" or "below ''f''<sub>''i''</sub>", respectively, in the implication ordering. By way of example, let us trace the effects of several such measures, namely, those that occupy the limiting positions of the Tables.
| align=left | Indicator of " x (y)" = 1
| align=left | Indicator of " x (y)" = 1
|}
|}
Tables 8 and 9 develop these ideas in more detail.
Tables 8 and 9 develop these ideas in more detail.
| 0 || 0 || 0 || 0 || 1 || 1 || 1 || 1
| 0 || 0 || 0 || 0 || 1 || 1 || 1 || 1
|}
|}
==Document History==
==Document History==