12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Saturday October 19, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Functional Logic : Quantification Theory (view source)
Revision as of 22:40, 17 November 2008
, 22:40, 17 November 2008spacing
|-
|-
| ''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.
| || || || || || || ||
| || || || || || || ||
| || || || || || || ||
| || || || || || || ||
|}
|}<br>
===Umpire Operators===
===Umpire Operators===
| align=right width=36 | 2.
| align=right width=36 | 2.
| Υ<sub>''p''</sub> = Υ(''p'', __, Π) : ('''B'''<sup>''k''</sup> → '''B''') → '''B'''.
| Υ<sub>''p''</sub> = Υ(''p'', __, Π) : ('''B'''<sup>''k''</sup> → '''B''') → '''B'''.
|}
|}<br>
This means that Υ<sub>''p''</sub> ''q'' = 1 if and only if ''q'' holds for all models of ''p''. In propositional terms, this is tantamount to the assertion that ''p'' ⇒ ''q'', or that _(p (q))_ = 1.
This means that Υ<sub>''p''</sub> ''q'' = 1 if and only if ''q'' holds for all models of ''p''. In propositional terms, this is tantamount to the assertion that ''p'' ⇒ ''q'', or that _(p (q))_ = 1.
| align=right width=36 | 4.
| align=right width=36 | 4.
| Υ = Υ(1, __, Π) : ('''B'''<sup>''k''</sup> → '''B''') → '''B'''.
| Υ = Υ(1, __, Π) : ('''B'''<sup>''k''</sup> → '''B''') → '''B'''.
|}
|}<br>
This means that Υ''q'' = 1 if and only if ''q'' holds for the whole universe of discourse in question, that is, if and only ''q'' is the constantly true proposition '''1''' : '''B'''<sup>''k''</sup> → '''B'''. 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.
This means that Υ''q'' = 1 if and only if ''q'' holds for the whole universe of discourse in question, that is, if and only ''q'' is the constantly true proposition '''1''' : '''B'''<sup>''k''</sup> → '''B'''. 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.
| || || || || || || ||
| || || || || || || ||
| || || || || || || || 1
| || || || || || || || 1
|}
|}<br>
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.
| iff || ''f'' ⇒ 1,
| iff || ''f'' ⇒ 1,
| hence || β<sub>15</sub> ''f'' = 1 for all ''f''.
| hence || β<sub>15</sub> ''f'' = 1 for all ''f''.
|}
|}<br>
Thus, α<sub>0</sub> = β<sub>15</sub> is a totally indiscriminate measure, one that accepts all propositions ''f'' : '''B'''<sup>2</sup> → '''B''', whereas α<sub>15</sub> and β<sub>0</sub> are measures that value the constant propositions '''1''' : '''B'''<sup>2</sup> → '''B''' and '''0''' : '''B'''<sup>2</sup> → '''B''', respectively, above all others.
Thus, α<sub>0</sub> = β<sub>15</sub> is a totally indiscriminate measure, one that accepts all propositions ''f'' : '''B'''<sup>2</sup> → '''B''', whereas α<sub>15</sub> and β<sub>0</sub> are measures that value the constant propositions '''1''' : '''B'''<sup>2</sup> → '''B''' and '''0''' : '''B'''<sup>2</sup> → '''B''', respectively, above all others.
|-
|-
| || = || "f likes (x)(y)"
| || = || "f likes (x)(y)"
|}
|}<br>
<br>
{|
{|
|-
|-
| || = || "f likes (x) y "
| || = || "f likes (x) y "
|}
|}<br>
<br>
{|
{|
|-
|-
| || = || "f likes x (y)"
| || = || "f likes x (y)"
|}
|}<br>
<br>
{|
{|
|-
|-
| || = || "f likes x y"
| || = || "f likes x y"
|}
|}<br>
<br>
Intuitively, the ''L''<sub>''uv''</sub> operators may be thought of as qualifying propositions according to the elements of the universe of discourse that each proposition positively values. Taken together, these measures provide us with the means to express many useful observations about the propositions in ''X''° = [''x'', ''y''], and so they mediate a subtext [''L''<sub>00</sub>, ''L''<sub>01</sub>, ''L''<sub>10</sub>, ''L''<sub>11</sub>] that takes place within the higher order universe of discourse ''X''°2 = [''X''°] = <nowiki>[[</nowiki>''x'', ''y''<nowiki>]]</nowiki>. Figure 6 summarizes the action of the ''L''<sub>''uv''</sub> on the ''f''<sub>''i''</sub> within ''X''°2.
Intuitively, the ''L''<sub>''uv''</sub> operators may be thought of as qualifying propositions according to the elements of the universe of discourse that each proposition positively values. Taken together, these measures provide us with the means to express many useful observations about the propositions in ''X''° = [''x'', ''y''], and so they mediate a subtext [''L''<sub>00</sub>, ''L''<sub>01</sub>, ''L''<sub>10</sub>, ''L''<sub>11</sub>] that takes place within the higher order universe of discourse ''X''°2 = [''X''°] = <nowiki>[[</nowiki>''x'', ''y''<nowiki>]]</nowiki>. Figure 6 summarizes the action of the ''L''<sub>''uv''</sub> on the ''f''<sub>''i''</sub> within ''X''°2.
| x || is || (y)
| x || is || (y)
| align=left | Indicator of " x (y)" = 1
| align=left | Indicator of " x (y)" = 1
|}
|}<br>
Tables 8 and 9 develop these ideas in more detail.
Tables 8 and 9 develop these ideas in more detail.
| align=left | Some x is y
| align=left | Some x is y
| ''L''<sub>11</sub>
| ''L''<sub>11</sub>
|}
|}<br>
<br>
{| align="center" border="1" cellpadding="4" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%"
{| align="center" border="1" cellpadding="4" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%"
| ''f<sub>15</sub> || 1111 || (( ))
| ''f<sub>15</sub> || 1111 || (( ))
| 0 || 0 || 0 || 0 || 1 || 1 || 1 || 1
| 0 || 0 || 0 || 0 || 1 || 1 || 1 || 1
|}
|}<br>
==Document History==
==Document History==
