Difference between revisions of "Directory:Jon Awbrey/Papers/Functional Logic : Quantification Theory"
Jon Awbrey (talk | contribs) ({{DISPLAYTITLE:Functional Logic : Quantification Theory}}) |
Jon Awbrey (talk | contribs) (copy content) |
||
Line 1: | Line 1: | ||
{{DISPLAYTITLE:Functional Logic : Quantification Theory}} | {{DISPLAYTITLE:Functional Logic : Quantification Theory}} | ||
+ | ==Toward a Functional Conception of Quantificational Logic== | ||
+ | |||
+ | Up till now quantification theory has been based on the assumption of individual variables ranging over universal collections of perfectly determinate elements. Merely to write down quantified formulas like "∀<sub>''x''∈''X''</sub> ''Fx''" and "∃<sub>''x''∈''X''</sub> ''Fx''" involves a subscription to such notions, as shown by the membership relations invoked in their indices. Reflected on pragmatic and constructive principles, however, these ideas begin to appear as problematic hypotheses whose warrants are not beyond question, projects of exhaustive determination that overreach the powers of finite information and control to manage. Therefore, it is worth considering how we might shift the scene of quantification theory closer to familiar ground, toward the predicates themselves that represent our continuing acquaintance with phenomena. | ||
+ | |||
+ | ===Higher Order Propositional Expressions=== | ||
+ | |||
+ | By way of equipping this inquiry with a bit of concrete material, I begin with a consideration of "higher order propositional expressions" (HOPE's), in particular, those that stem from the propositions on 1 and 2 variables. | ||
+ | |||
+ | ====Higher Order Propositions and Logical Operators (''n'' <nowiki>=</nowiki> 1)==== | ||
+ | |||
+ | A "higher order proposition" is, very roughly speaking, a proposition about propositions. If the original order of propositions is a class of indicator functions {''F'' : ''X'' → '''B'''}, then the next higher order of propositions consists of maps of the type ''m'' : (''X'' → '''B''') → '''B''', where, as usual, '''B''' = {0, 1}. | ||
+ | |||
+ | For example, consider the case where ''X'' = '''B'''<sup>1</sup> = '''B'''. Then there are exactly four propositions of the form ''F'' : '''B''' → '''B''', and exactly sixteen higher order propositions, all of the type ''m'' : ('''B''' → '''B''') → '''B'''. Table 7 lists the sixteen higher order propositions about propositions on one boolean variable, organized in the following fashion: | ||
+ | |||
+ | Columns 1 and 2 form a truth table for the four ''F'' : '''B''' → '''B''', perhaps turned on its side from the way one is accustomed to see truth tables, with the row leaders in Column 1 displaying the names of the functions ''F''<sub>''i''</sub>, ''i'' = 1 to 4, while the entries in Column 2 give the values of each function for the argument values that are listed in the column head. Column 3 displays one of the usual expressions for the proposition in question. The last sixteen columns are topped by a set of conventional names for the higher order propositions, also known as the "measures" ''m''<sub>''j''</sub>, for ''j'' = 0 to 15, where the entries in the body of the Table record the values that each ''m''<sub>''j''</sub> assigns to each ''F''<sub>''i''</sub>. | ||
+ | |||
+ | {| align="center" border="1" cellpadding="4" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 7. Higher Order Propositions (n = 1)''' | ||
+ | |- style="background:paleturquoise" | ||
+ | | \ ''x'' || 1 0 || ''F'' | ||
+ | |''m''||''m''||''m''||''m''||''m''||''m''||''m''||''m'' | ||
+ | |''m''||''m''||''m''||''m''||''m''||''m''||''m''||''m'' | ||
+ | |- style="background:paleturquoise" | ||
+ | | ''F'' \ || || | ||
+ | |00||01||02||03||04||05||06||07||08||09||10||11||12||13||14||15 | ||
+ | |- | ||
+ | | ''F<sub>0</sub> || 0 0 || 0 ||0||1||0||1||0||1||0||1||0||1||0||1||0||1||0||1 | ||
+ | |- | ||
+ | | ''F<sub>1</sub> || 0 1 || (x) ||0||0||1||1||0||0||1||1||0||0||1||1||0||0||1||1 | ||
+ | |- | ||
+ | | ''F<sub>2</sub> || 1 0 || x ||0||0||0||0||1||1||1||1||0||0||0||0||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 8, 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. | ||
+ | |||
+ | {| align="center" border="1" cellpadding="4" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 8. Interpretive Categories for Higher Order Propositions (n = 1)''' | ||
+ | |- style="background:paleturquoise" | ||
+ | |Measure||Happening||Exactness||Existence||Linearity||Uniformity||Information | ||
+ | |- | ||
+ | |''m''<sub>0</sub>||nothing happens|| || || || || | ||
+ | |- | ||
+ | |''m''<sub>1</sub>|| ||just false||nothing exists|| || || | ||
+ | |- | ||
+ | |''m''<sub>2</sub>|| ||just not x|| || || || | ||
+ | |- | ||
+ | |''m''<sub>3</sub>|| || ||nothing is x|| || || | ||
+ | |- | ||
+ | |''m''<sub>4</sub>|| ||just x|| || || || | ||
+ | |- | ||
+ | |''m''<sub>5</sub>|| || ||everything is x||F is linear|| || | ||
+ | |- | ||
+ | |''m''<sub>6</sub>|| || || || ||F is not uniform||F is informed | ||
+ | |- | ||
+ | |''m''<sub>7</sub>|| ||not just true|| || || || | ||
+ | |- | ||
+ | |''m''<sub>8</sub>|| ||just true|| || || || | ||
+ | |- | ||
+ | |''m''<sub>9</sub>|| || || || ||F is uniform||F is not informed | ||
+ | |- | ||
+ | |''m''<sub>10</sub>|| || ||something is not x||F is not linear|| || | ||
+ | |- | ||
+ | |''m''<sub>11</sub>|| ||not just x|| || || || | ||
+ | |- | ||
+ | |''m''<sub>12</sub>|| || ||something is x|| || || | ||
+ | |- | ||
+ | |''m''<sub>13</sub>|| ||not just not x|| || || || | ||
+ | |- | ||
+ | |''m''<sub>14</sub>|| ||not just false||something exists|| || || | ||
+ | |- | ||
+ | |''m''<sub>15</sub>||anything happens|| || || || || | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | ====Higher Order Propositions and Logical Operators (n <nowiki>=</nowiki> 2)==== | ||
+ | |||
+ | By way of reviewing notation and preparing to extend it to higher order universes of discourse, let us first consider the universe of discourse ''X''° = [''X''] = [''x''<sub>1</sub>, ''x''<sub>2</sub>] = [''x'', ''y''], based on two logical features or boolean variables ''x'' and ''y''. | ||
+ | |||
+ | {| | ||
+ | | align=right width=36 | 1. | ||
+ | | The points of ''X''° are collected in the space: | ||
+ | |- | ||
+ | | | ||
+ | | ''X'' = <<''x'', ''y''>> = {<''x'', ''y''>} <u>≈</u> '''B'''<sup>2</sup>. | ||
+ | |- | ||
+ | | | ||
+ | |- | ||
+ | | | ||
+ | | In other words, written out in full: | ||
+ | |- | ||
+ | | | ||
+ | | ''X'' = {<"(''x'')", "(''y'')">, <"(''x'')", "''y''">, <"''x''", "(''y'')">, <"''x''", "''y''">} | ||
+ | |- | ||
+ | | | ||
+ | | ''X'' <u>≈</u> {<0, 0>, <0, 1>, <1, 0>, <1, 1>} | ||
+ | |- | ||
+ | | | ||
+ | |- | ||
+ | | align=right width=36 | 2. | ||
+ | | The propositions of ''X''° make up the space: | ||
+ | |- | ||
+ | | | ||
+ | | ''X''↑ = (''X'' → '''B''') = {''f'' : ''X'' → '''B'''} <u>≈</u> ('''B'''<sup>2</sup> → '''B'''). | ||
+ | |} | ||
+ | |||
+ | 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 ''X''° is ''X''°2 = [''X''°] = <nowiki>[[</nowiki>''x'', ''y''<nowiki>]]</nowiki>, which may be developed in the following way. The propositions of ''X''° become the points of ''X''°2, and the mappings of the type ''m'' : (''X'' → '''B''') → '''B''' become the propositions of ''X''°2. 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 ''w'' : ('''B'''<sup>2</sup> → '''B''')<sup>''k''</sup> → '''B'''. | ||
+ | |||
+ | 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. | ||
+ | |||
+ | There are 2<sup>16</sup> = 65536 measures of the type ''m'' : ('''B'''<sup>2</sup> → '''B''') → '''B'''. Table 9 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. | ||
+ | |||
+ | {| align="center" border="1" cellpadding="0" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 9. Higher Order Propositions (n = 2)''' | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''x'' : || 1100 || ''f'' | ||
+ | |''m''||''m''||''m''||''m''||''m''||''m''||''m''||''m'' | ||
+ | |''m''||''m''||''m''||''m''||''m''||''m''||''m''||''m'' | ||
+ | |''m''||''m''||''m''||''m''||''m''||''m''||''m''||''m'' | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''y'' : || 1010 || | ||
+ | |0||1||2||3||4||5||6||7||8||9||10||11||12 | ||
+ | |13||14||15||16||17||18||19||20||21||22||23 | ||
+ | |- | ||
+ | | ''f<sub>0</sub> || 0000 || ( ) | ||
+ | | 0 || 1 || 0 || 1 || 0 || 1 || 0 || 1 | ||
+ | | 0 || 1 || 0 || 1 || 0 || 1 || 0 || 1 | ||
+ | | 0 || 1 || 0 || 1 || 0 || 1 || 0 || 1 | ||
+ | |- | ||
+ | | ''f<sub>1</sub> || 0001 || (x)(y) | ||
+ | | || || 1 || 1 || 0 || 0 || 1 || 1 | ||
+ | | 0 || 0 || 1 || 1 || 0 || 0 || 1 || 1 | ||
+ | | 0 || 0 || 1 || 1 || 0 || 0 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>2</sub> || 0010 || (x) y | ||
+ | | || || || || 1 || 1 || 1 || 1 | ||
+ | | 0 || 0 || 0 || 0 || 1 || 1 || 1 || 1 | ||
+ | | 0 || 0 || 0 || 0 || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>3</sub> || 0011 || (x) | ||
+ | | || || || || || || || | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | | 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0 | ||
+ | |- | ||
+ | | ''f<sub>4</sub> || 0100 || x (y) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>5</sub> || 0101 || (y) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>6</sub> || 0110 || (x, y) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>7</sub> || 0111 || (x y) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>8</sub> || 1000 || x y | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>9</sub> || 1001 || ((x, y)) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>10</sub> || 1010 || y | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>11</sub> || 1011 || (x (y)) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>12</sub> || 1100 || x | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>13</sub> || 1101 || ((x) y) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>14</sub> || 1110 || ((x)(y)) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |- | ||
+ | | ''f<sub>15</sub> || 1111 || (( )) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | ===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 Υ, 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: | ||
+ | |||
+ | : <math>\Upsilon : \cup^{m = 1, 2, 3}((\mathbb{B}^k \to \mathbb{B})^m \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: | ||
+ | |||
+ | : Υ<sub>''p''</sub><sup>''r''</sup> ''q'' = Υ(''p'', ''q'', ''r'') | ||
+ | |||
+ | : Υ<sub>''p''</sub><sup>''r''</sup> : ('''B'''<sup>''k''</sup> → '''B''') → '''B''' | ||
+ | |||
+ | The intention of this operator is that we evaluate the proposition ''q'' on each model of the proposition ''p'' and combine the results according to the method indicated by the connective parameter ''r''. In principle, the index ''r'' might specify any connective on as many as 2<sup>''k''</sup> 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 ''p'', ''r'' is assigned a default value that is understood to be in force when the corresponding argument place is left blank, specifically, the constant proposition '''1''' : '''B'''<sup>''k''</sup> → '''B''' for the lower index ''p'', and the continued conjunction or continued product operation Π for the upper index ''r''. Taking the upper default value gives license to the following readings: | ||
+ | |||
+ | {| | ||
+ | | align=right width=36 | 1. | ||
+ | | Υ<sub>''p''</sub> ''q'' = Υ(''p'', ''q'') = Υ(''p'', ''q'', Π). | ||
+ | |- | ||
+ | | align=right width=36 | 2. | ||
+ | | Υ<sub>''p''</sub> = Υ(''p'', __, Π) : ('''B'''<sup>''k''</sup> → '''B''') → '''B'''. | ||
+ | |} | ||
+ | |||
+ | 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. | ||
+ | |||
+ | Throwing in the lower default value permits the following abbreviations: | ||
+ | |||
+ | {| | ||
+ | | align=right width=36 | 3. | ||
+ | | Υ''q'' = Υ(''q'') = Υ<sub>1</sub> ''q'' = Υ(1, ''q'', Π). | ||
+ | |- | ||
+ | | align=right width=36 | 4. | ||
+ | | Υ = Υ(1, __, Π) : ('''B'''<sup>''k''</sup> → '''B''') → '''B'''. | ||
+ | |} | ||
+ | |||
+ | 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. | ||
+ | |||
+ | ===Measure for Measure=== | ||
+ | |||
+ | An acquaintance with the functions of the umpire operator can be gained from Tables 10 and 11, where the 2-dimensional case is worked out in full. | ||
+ | |||
+ | The auxiliary notations: | ||
+ | |||
+ | : α<sub>''i''</sub> ''f'' = Υ(''f''<sub>''i''</sub>, ''f''), | ||
+ | |||
+ | : β<sub>''i''</sub> ''f'' = Υ(''f'', ''f''<sub>''i''</sub>), | ||
+ | |||
+ | define two series of measures: | ||
+ | |||
+ | : α<sub>''i''</sub>, β<sub>''i''</sub> : ('''B'''<sup>2</sup> → '''B''') → '''B''', | ||
+ | |||
+ | incidentally providing compact names for the column headings of the next two Tables. | ||
+ | |||
+ | {| align="center" border="1" cellpadding="0" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 10. Qualifiers of Implication Ordering: α<sub>''i'' </sub>''f'' = Υ(''f''<sub>''i''</sub> ⇒ ''f'')''' | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''x'' : || 1100 || ''f'' | ||
+ | |α||α||α||α||α||α||α||α | ||
+ | |α||α||α||α||α||α||α||α | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''y'' : || 1010 || | ||
+ | |15||14||13||12||11||10||9||8||7||6||5||4||3||2||1||0 | ||
+ | |- | ||
+ | | ''f<sub>0</sub> || 0000 || ( ) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || 1 | ||
+ | |- | ||
+ | | ''f<sub>1</sub> || 0001 || (x)(y) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>2</sub> || 0010 || (x) y | ||
+ | | || || || || || || || | ||
+ | | || || || || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>3</sub> || 0011 || (x) | ||
+ | | || || || || || || || | ||
+ | | || || || || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>4</sub> || 0100 || x (y) | ||
+ | | || || || || || || || | ||
+ | | || || || 1 || || || || 1 | ||
+ | |- | ||
+ | | ''f<sub>5</sub> || 0101 || (y) | ||
+ | | || || || || || || || | ||
+ | | || || 1 || 1 || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>6</sub> || 0110 || (x, y) | ||
+ | | || || || || || || || | ||
+ | | || 1 || || 1 || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>7</sub> || 0111 || (x y) | ||
+ | | || || || || || || || | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>8</sub> || 1000 || x y | ||
+ | | || || || || || || || 1 | ||
+ | | || || || || || || || 1 | ||
+ | |- | ||
+ | | ''f<sub>9</sub> || 1001 || ((x, y)) | ||
+ | | || || || || || || 1 || 1 | ||
+ | | || || || || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>10</sub> || 1010 || y | ||
+ | | || || || || || 1 || || 1 | ||
+ | | || || || || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>11</sub> || 1011 || (x (y)) | ||
+ | | || || || || 1 || 1 || 1 || 1 | ||
+ | | || || || || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>12</sub> || 1100 || x | ||
+ | | || || || 1 || || || || 1 | ||
+ | | || || || 1 || || || || 1 | ||
+ | |- | ||
+ | | ''f<sub>13</sub> || 1101 || ((x) y) | ||
+ | | || || 1 || 1 || || || 1 || 1 | ||
+ | | || || 1 || 1 || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>14</sub> || 1110 || ((x)(y)) | ||
+ | | || 1 || || 1 || || 1 || || 1 | ||
+ | | || 1 || || 1 || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>15</sub> || 1111 || (( )) | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | {| align="center" border="1" cellpadding="0" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 11. Qualifiers of Implication Ordering: β<sub>''i'' </sub>''f'' = Υ(''f'' ⇒ ''f''<sub>''i''</sub>)''' | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''x'' : || 1100 || ''f'' | ||
+ | |β||β||β||β||β||β||β||β | ||
+ | |β||β||β||β||β||β||β||β | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''y'' : || 1010 || | ||
+ | |0||1||2||3||4||5||6||7||8||9||10||11||12||13||14||15 | ||
+ | |- | ||
+ | | ''f<sub>0</sub> || 0000 || ( ) | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>1</sub> || 0001 || (x)(y) | ||
+ | | || 1 || || 1 || || 1 || || 1 | ||
+ | | || 1 || || 1 || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>2</sub> || 0010 || (x) y | ||
+ | | || || 1 || 1 || || || 1 || 1 | ||
+ | | || || 1 || 1 || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>3</sub> || 0011 || (x) | ||
+ | | || || || 1 || || || || 1 | ||
+ | | || || || 1 || || || || 1 | ||
+ | |- | ||
+ | | ''f<sub>4</sub> || 0100 || x (y) | ||
+ | | || || || || 1 || 1 || 1 || 1 | ||
+ | | || || || || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>5</sub> || 0101 || (y) | ||
+ | | || || || || || 1 || || 1 | ||
+ | | || || || || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>6</sub> || 0110 || (x, y) | ||
+ | | || || || || || || 1 || 1 | ||
+ | | || || || || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>7</sub> || 0111 || (x y) | ||
+ | | || || || || || || || 1 | ||
+ | | || || || || || || || 1 | ||
+ | |- | ||
+ | | ''f<sub>8</sub> || 1000 || x y | ||
+ | | || || || || || || || | ||
+ | | 1 || 1 || 1 || 1 || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>9</sub> || 1001 || ((x, y)) | ||
+ | | || || || || || || || | ||
+ | | || 1 || || 1 || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>10</sub> || 1010 || y | ||
+ | | || || || || || || || | ||
+ | | || || 1 || 1 || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>11</sub> || 1011 || (x (y)) | ||
+ | | || || || || || || || | ||
+ | | || || || 1 || || || || 1 | ||
+ | |- | ||
+ | | ''f<sub>12</sub> || 1100 || x | ||
+ | | || || || || || || || | ||
+ | | || || || || 1 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>13</sub> || 1101 || ((x) y) | ||
+ | | || || || || || || || | ||
+ | | || || || || || 1 || || 1 | ||
+ | |- | ||
+ | | ''f<sub>14</sub> || 1110 || ((x)(y)) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>15</sub> || 1111 || (( )) | ||
+ | | || || || || || || || | ||
+ | | || || || || || || || 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. | ||
+ | |||
+ | {| cellpadding=2 | ||
+ | | width=36 | | ||
+ | | α<sub>00</sub> ''f'' = 1 | ||
+ | | iff || ''f''<sub>00</sub> ⇒ ''f'', | ||
+ | | iff || 0 ⇒ ''f'', | ||
+ | | hence || α<sub>00</sub> ''f'' = 1 for all ''f''. | ||
+ | |- | ||
+ | | | ||
+ | | α<sub>15</sub> ''f'' = 1 | ||
+ | | iff || ''f''<sub>15</sub> ⇒ f, | ||
+ | | iff || 1 ⇒ ''f'', | ||
+ | | hence || α<sub>15</sub> ''f'' = 1 ⇒ ''f'' = 1. | ||
+ | |- | ||
+ | | | ||
+ | | β<sub>00</sub> ''f'' = 1 | ||
+ | | iff || ''f'' ⇒ f<sub>00</sub>, | ||
+ | | iff || ''f'' ⇒ 0, | ||
+ | | hence || β<sub>00</sub> ''f'' = 1 ⇒ f = 0. | ||
+ | |- | ||
+ | | | ||
+ | | β<sub>15</sub> ''f'' = 1 | ||
+ | | iff || ''f'' ⇒ f<sub>15</sub>, | ||
+ | | iff || ''f'' ⇒ 1, | ||
+ | | hence || β<sub>15</sub> ''f'' = 1 for all ''f''. | ||
+ | |} | ||
+ | |||
+ | 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. | ||
+ | |||
+ | Finally, in conformity with the use of the fiber notation to indicate sets of models, it is natural to use notations like: | ||
+ | |||
+ | : [| α<sub>''i''</sub> |] = (α<sub>''i''</sub>)<sup>(–1)</sup>(1), | ||
+ | |||
+ | : [| β<sub>''i''</sub> |] = (β<sub>''i''</sub>)<sup>(–1)</sup>(1), | ||
+ | |||
+ | : [| Υ<sub>''p''</sub> |] = (Υ<sub>''p''</sub>)<sup>(–1)</sup>(1), | ||
+ | |||
+ | to denote sets of propositions that satisfy the umpires in question. | ||
+ | |||
+ | ===Extending the Existential Interpretation to Quantificational Logic=== | ||
+ | |||
+ | Previously I introduced a calculus for propositional logic, fixing its meaning according to what C.S. Peirce called the "existential interpretation". As far as it concerns propositional calculus this interpretation settles the meanings that are associated with merely the most basic symbols and logical connectives. Now we must extend and refine the existential interpretation to comprehend the analysis of "quantifications", that is, quantified propositions. In doing so we recognize two additional aspects of logic that need to be developed, over and above the material of propositional logic. At the formal extreme there is the aspect of higher order functional types, into which we have already ventured a little above. At the level of the fundamental content of the available propositions we have to introduce a different interpretation for what we may call "elemental" or "singular" propositions. | ||
+ | |||
+ | Let us return to the 2-dimensional case ''X''° = [''x'', ''y'']. In order to provide a bridge between propositions and quantifications it serves to define a set of qualifiers ''L''<sub>''uv''</sub> : ('''B'''<sup>2</sup> → '''B''') → '''B''' that have the following characters: | ||
+ | |||
+ | {| | ||
+ | | width=36 | || ''L''<sub>00</sub> ''f'' | ||
+ | |- | ||
+ | | || = || ''L''<sub>"(x)(y)"</sub> ''f'' | ||
+ | |- | ||
+ | | || = || α<sub>1</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"(x)(y)"</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"(x)(y) ⇒ f"</sub> | ||
+ | |- | ||
+ | | || = || "f likes (x)(y)" | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | {| | ||
+ | | width=36 | || ''L''<sub>01</sub> ''f'' | ||
+ | |- | ||
+ | | || = || ''L''<sub>"(x) y "</sub> ''f'' | ||
+ | |- | ||
+ | | || = || α<sub>2</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"(x) y "</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"(x) y ⇒ f"</sub> | ||
+ | |- | ||
+ | | || = || "f likes (x) y " | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | {| | ||
+ | | width=36 | || ''L''<sub>10</sub> ''f'' | ||
+ | |- | ||
+ | | || = || ''L''<sub>" x (y)"</sub> ''f'' | ||
+ | |- | ||
+ | | || = || α<sub>4</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"x (y)"</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"x (y) ⇒ f"</sub> | ||
+ | |- | ||
+ | | || = || "f likes x (y)" | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | {| | ||
+ | | width=36 | || ''L''<sub>11</sub> ''f'' | ||
+ | |- | ||
+ | | || = || ''L''<sub>" x y"</sub> ''f'' | ||
+ | |- | ||
+ | | || = || α<sub>8</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"x y"</sub> ''f'' | ||
+ | |- | ||
+ | | || = || Υ<sub>"x y ⇒ f"</sub> | ||
+ | |- | ||
+ | | || = || "f likes x y" | ||
+ | |} | ||
+ | <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 12 summarizes the action of the ''L''<sub>''uv''</sub> on the ''f''<sub>''i''</sub> within ''X''°2. | ||
+ | |||
+ | <pre> | ||
+ | o-----------------------------------------------------------o | ||
+ | | | | ||
+ | | o | | ||
+ | | / \ | | ||
+ | | / \ | | ||
+ | | /x y\ | | ||
+ | | / o---o \ | | ||
+ | | o \ / o | | ||
+ | | / \ o / \ | | ||
+ | | / \ | / \ | | ||
+ | | / \ @ / \ | | ||
+ | | / x y \ / x y \ | | ||
+ | | o o---o o o---o o | | ||
+ | | / \ \ / \ / / \ | | ||
+ | | / \ @ / \ @ / \ | | ||
+ | | / \ / \ / \ | | ||
+ | | / y \ / \ / y \ | | ||
+ | | o @ o @ o o o | | ||
+ | | / \ / \ / \ | / \ | | ||
+ | | / \ / \ / \ @ / \ | | ||
+ | | / \ /x y\ / \ / \ | | ||
+ | | / x y \ / o o \ / x y \ / x y \ | | ||
+ | | o @ o \ / o o o o o o | | ||
+ | | |\ / \ o / \ | / \ \ / /| | | ||
+ | | | \ / \ | / \ @ / \ @ / | | | ||
+ | | | \ / \ @ / \ / \ / | | | ||
+ | | | \ / x \ / x y \ / x \ / | | | ||
+ | | | o @ o o---o o o o | | | ||
+ | | | |\ / \ \ / / \ | /| | | | ||
+ | | | | \ / \ @ / \ @ / | | | | ||
+ | | | | \ / \ / \ / | | | | ||
+ | | |L_11| \ / o y \ / x o \ / |L_00| | | ||
+ | | o---------o | o | o---------o | | ||
+ | | | \ x @ / \ @ y / | | | ||
+ | | | \ / \ / | | | ||
+ | | | \ / \ / | | | ||
+ | | |L_10 \ / o \ / L_01| | | ||
+ | | o---------o | o---------o | | ||
+ | | \ @ / | | ||
+ | | \ / | | ||
+ | | \ / | | ||
+ | | \ / | | ||
+ | | o | | ||
+ | | | | ||
+ | o-----------------------------------------------------------o | ||
+ | Figure 12. Higher Order Universe of Discourse [L_uv] c [[x, y]] | ||
+ | </pre> | ||
+ | |||
+ | ===Application of Higher Order Propositions to Quantification Theory=== | ||
+ | |||
+ | Our excursion into the vastening landscape of higher order propositions has finally come round to the stage where we can bring its returns to bear on opening up new perspectives for quantificational logic. | ||
+ | |||
+ | There is a question arising next that is still experimental in my mind. Whether it makes much difference from a purely formal point of view is not a question I can answer yet, but it does seem to aid the intuition to invent a slightly different interpretation for the two-valued space that we use as the target of our basic indicator functions. Therefore, let us declare a type of "existential-valued" functions ''f'' : '''B'''<sup>''k''</sup> → <font face="lucida calligraphy">E</font>, where <font face="lucida calligraphy">E</font> = {–e, +e} = {"empty", "exist"} is a couple of values that we interpret as indicating whether of not anything exists in the cells of the underlying universe of discourse, venn diagram, or other domain. As usual, let us not be too strict about the coding of these functions, reverting to binary codes whenever the interpretation is clear enough. | ||
+ | |||
+ | With this interpretation in mind we note the following correspondences between classical quantifications and higher order indicator functions: | ||
+ | |||
+ | {| align="center" border="1" cellpadding="6" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 13. Syllogistic Premisses as Higher Order Indicator Functions''' | ||
+ | | A | ||
+ | | align=left | Universal Affirmative | ||
+ | | align=left | All | ||
+ | | x || is || y | ||
+ | | align=left | Indicator of " x (y)" = 0 | ||
+ | |- | ||
+ | | E | ||
+ | | align=left | Universal Negative | ||
+ | | align=left | All | ||
+ | | x || is || (y) | ||
+ | | align=left | Indicator of " x y " = 0 | ||
+ | |- | ||
+ | | I | ||
+ | | align=left | Particular Affirmative | ||
+ | | align=left | Some | ||
+ | | x || is || y | ||
+ | | align=left | Indicator of " x y " = 1 | ||
+ | |- | ||
+ | | O | ||
+ | | align=left | Particular Negative | ||
+ | | align=left | Some | ||
+ | | x || is || (y) | ||
+ | | align=left | Indicator of " x (y)" = 1 | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | Tables 14 and 15 develop these ideas in more detail. | ||
+ | |||
+ | {| align="center" border="1" cellpadding="6" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 14. Relation of Quantifiers to Higher Order Propositions''' | ||
+ | |- style="background:paleturquoise" | ||
+ | |Mnemonic||Category||Classical Form||Alternate Form||Symmetric Form||Operator | ||
+ | |- | ||
+ | | E<br>Exclusive | ||
+ | | Universal<br>Negative | ||
+ | | align=left | All x is (y) | ||
+ | | align=left | | ||
+ | | align=left | No x is y | ||
+ | | (''L''<sub>11</sub>) | ||
+ | |- | ||
+ | | A<br>Absolute | ||
+ | | Universal<br>Affirmative | ||
+ | | align=left | All x is y | ||
+ | | align=left | | ||
+ | | align=left | No x is (y) | ||
+ | | (''L''<sub>10</sub>) | ||
+ | |- | ||
+ | | | ||
+ | | | ||
+ | | align=left | All y is x | ||
+ | | align=left | No y is (x) | ||
+ | | align=left | No (x) is y | ||
+ | | (''L''<sub>01</sub>) | ||
+ | |- | ||
+ | | | ||
+ | | | ||
+ | | align=left | All (y) is x | ||
+ | | align=left | No (y) is (x) | ||
+ | | align=left | No (x) is (y) | ||
+ | | (''L''<sub>00</sub>) | ||
+ | |- | ||
+ | | | ||
+ | | | ||
+ | | align=left | Some (x) is (y) | ||
+ | | align=left | | ||
+ | | align=left | Some (x) is (y) | ||
+ | | ''L''<sub>00</sub> | ||
+ | |- | ||
+ | | | ||
+ | | | ||
+ | | align=left | Some (x) is y | ||
+ | | align=left | | ||
+ | | align=left | Some (x) is y | ||
+ | | ''L''<sub>01</sub> | ||
+ | |- | ||
+ | | O<br>Obtrusive | ||
+ | | Particular<br>Negative | ||
+ | | align=left | Some x is (y) | ||
+ | | align=left | | ||
+ | | align=left | Some x is (y) | ||
+ | | ''L''<sub>10</sub> | ||
+ | |- | ||
+ | | I<br>Indefinite | ||
+ | | Particular<br>Affirmative | ||
+ | | align=left | Some x is y | ||
+ | | align=left | | ||
+ | | align=left | Some x is y | ||
+ | | ''L''<sub>11</sub> | ||
+ | |} | ||
+ | <br> | ||
+ | |||
+ | {| align="center" border="1" cellpadding="4" cellspacing="0" style="background:lightcyan; font-weight:bold; text-align:center; width:90%" | ||
+ | |+ '''Table 15. Simple Qualifiers of Propositions (n = 2)''' | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''x'' : || 1100 || ''f'' | ||
+ | | (''L''<sub>11</sub>) | ||
+ | | (''L''<sub>10</sub>) | ||
+ | | (''L''<sub>01</sub>) | ||
+ | | (''L''<sub>00</sub>) | ||
+ | | ''L''<sub>00</sub> | ||
+ | | ''L''<sub>01</sub> | ||
+ | | ''L''<sub>10</sub> | ||
+ | | ''L''<sub>11</sub> | ||
+ | |- style="background:paleturquoise" | ||
+ | | align=right | ''y'' : || 1010 || | ||
+ | | align=left | no x <br> is y | ||
+ | | align=left | no x <br> is (y) | ||
+ | | align=left | no (x) <br> is y | ||
+ | | align=left | no (x) <br> is (y) | ||
+ | | align=left | some (x) <br> is (y) | ||
+ | | align=left | some (x) <br> is y | ||
+ | | align=left | some x <br> is (y) | ||
+ | | align=left | some x <br> is y | ||
+ | |- | ||
+ | | ''f<sub>0</sub> || 0000 || ( ) | ||
+ | | 1 || 1 || 1 || 1 || 0 || 0 || 0 || 0 | ||
+ | |- | ||
+ | | ''f<sub>1</sub> || 0001 || (x)(y) | ||
+ | | 1 || 1 || 1 || 0 || 1 || 0 || 0 || 0 | ||
+ | |- | ||
+ | | ''f<sub>2</sub> || 0010 || (x) y | ||
+ | | 1 || 1 || 0 || 1 || 0 || 1 || 0 || 0 | ||
+ | |- | ||
+ | | ''f<sub>3</sub> || 0011 || (x) | ||
+ | | 1 || 1 || 0 || 0 || 1 || 1 || 0 || 0 | ||
+ | |- | ||
+ | | ''f<sub>4</sub> || 0100 || x (y) | ||
+ | | 1 || 0 || 1 || 1 || 0 || 0 || 1 || 0 | ||
+ | |- | ||
+ | | ''f<sub>5</sub> || 0101 || (y) | ||
+ | | 1 || 0 || 1 || 0 || 1 || 0 || 1 || 0 | ||
+ | |- | ||
+ | | ''f<sub>6</sub> || 0110 || (x, y) | ||
+ | | 1 || 0 || 0 || 1 || 0 || 1 || 1 || 0 | ||
+ | |- | ||
+ | | ''f<sub>7</sub> || 0111 || (x y) | ||
+ | | 1 || 0 || 0 || 0 || 1 || 1 || 1 || 0 | ||
+ | |- | ||
+ | | ''f<sub>8</sub> || 1000 || x y | ||
+ | | 0 || 1 || 1 || 1 || 0 || 0 || 0 || 1 | ||
+ | |- | ||
+ | | ''f<sub>9</sub> || 1001 || ((x, y)) | ||
+ | | 0 || 1 || 1 || 0 || 1 || 0 || 0 || 1 | ||
+ | |- | ||
+ | | ''f<sub>10</sub> || 1010 || y | ||
+ | | 0 || 1 || 0 || 1 || 0 || 1 || 0 || 1 | ||
+ | |- | ||
+ | | ''f<sub>11</sub> || 1011 || (x (y)) | ||
+ | | 0 || 1 || 0 || 0 || 1 || 1 || 0 || 1 | ||
+ | |- | ||
+ | | ''f<sub>12</sub> || 1100 || x | ||
+ | | 0 || 0 || 1 || 1 || 0 || 0 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>13</sub> || 1101 || ((x) y) | ||
+ | | 0 || 0 || 1 || 0 || 1 || 0 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>14</sub> || 1110 || ((x)(y)) | ||
+ | | 0 || 0 || 0 || 1 || 0 || 1 || 1 || 1 | ||
+ | |- | ||
+ | | ''f<sub>15</sub> || 1111 || (( )) | ||
+ | | 0 || 0 || 0 || 0 || 1 || 1 || 1 || 1 | ||
+ | |} | ||
+ | <br> |
Revision as of 03:18, 17 November 2008
Toward a Functional Conception of Quantificational Logic
Up till now quantification theory has been based on the assumption of individual variables ranging over universal collections of perfectly determinate elements. Merely to write down quantified formulas like "∀x∈X Fx" and "∃x∈X Fx" involves a subscription to such notions, as shown by the membership relations invoked in their indices. Reflected on pragmatic and constructive principles, however, these ideas begin to appear as problematic hypotheses whose warrants are not beyond question, projects of exhaustive determination that overreach the powers of finite information and control to manage. Therefore, it is worth considering how we might shift the scene of quantification theory closer to familiar ground, toward the predicates themselves that represent our continuing acquaintance with phenomena.
Higher Order Propositional Expressions
By way of equipping this inquiry with a bit of concrete material, I begin with a consideration of "higher order propositional expressions" (HOPE's), in particular, those that stem from the propositions on 1 and 2 variables.
Higher Order Propositions and Logical Operators (n = 1)
A "higher order proposition" is, very roughly speaking, a proposition about propositions. If the original order of propositions is a class of indicator functions {F : X → B}, then the next higher order of propositions consists of maps of the type m : (X → B) → B, where, as usual, B = {0, 1}.
For example, consider the case where X = B1 = B. Then there are exactly four propositions of the form F : B → B, and exactly sixteen higher order propositions, all of the type m : (B → B) → B. Table 7 lists the sixteen higher order propositions about propositions on one boolean variable, organized in the following fashion:
Columns 1 and 2 form a truth table for the four F : B → B, perhaps turned on its side from the way one is accustomed to see truth tables, with the row leaders in Column 1 displaying the names of the functions Fi, i = 1 to 4, while the entries in Column 2 give the values of each function for the argument values that are listed in the column head. Column 3 displays one of the usual expressions for the proposition in question. The last sixteen columns are topped by a set of conventional names for the higher order propositions, also known as the "measures" mj, for j = 0 to 15, where the entries in the body of the Table record the values that each mj assigns to each Fi.
\ x | 1 0 | F | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m |
F \ | 00 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 | 10 | 11 | 12 | 13 | 14 | 15 | ||
F0 | 0 0 | 0 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 |
F1 | 0 1 | (x) | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 |
F2 | 1 0 | x | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 |
F3 | 1 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
I am going to put off explaining Table 8, 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.
Measure | Happening | Exactness | Existence | Linearity | Uniformity | Information |
m0 | nothing happens | |||||
m1 | just false | nothing exists | ||||
m2 | just not x | |||||
m3 | nothing is x | |||||
m4 | just x | |||||
m5 | everything is x | F is linear | ||||
m6 | F is not uniform | F is informed | ||||
m7 | not just true | |||||
m8 | just true | |||||
m9 | F is uniform | F is not informed | ||||
m10 | something is not x | F is not linear | ||||
m11 | not just x | |||||
m12 | something is x | |||||
m13 | not just not x | |||||
m14 | not just false | something exists | ||||
m15 | anything happens |
Higher Order Propositions and Logical Operators (n = 2)
By way of reviewing notation and preparing to extend it to higher order universes of discourse, let us first consider the universe of discourse X° = [X] = [x1, x2] = [x, y], based on two logical features or boolean variables x and y.
1. | The points of X° are collected in the space: |
X = <<x, y>> = {<x, y>} ≈ B2. | |
In other words, written out in full: | |
X = {<"(x)", "(y)">, <"(x)", "y">, <"x", "(y)">, <"x", "y">} | |
X ≈ {<0, 0>, <0, 1>, <1, 0>, <1, 1>} | |
2. | The propositions of X° make up the space: |
X↑ = (X → B) = {f : X → B} ≈ (B2 → B). |
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 X° is X°2 = [X°] = [[x, y]], which may be developed in the following way. The propositions of X° become the points of X°2, and the mappings of the type m : (X → B) → B become the propositions of X°2. 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 w : (B2 → B)k → B.
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 (mj)–1(1) that mj likes and the pictures (mj)–1(0) that mj dislikes.
There are 216 = 65536 measures of the type m : (B2 → B) → B. Table 9 introduces the first 24 of these measures in the fashion of the higher order truth table that I used before. The column headed "mj" shows the values of the measure mj on each of the propositions fi : B2 → 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 mj is the decimal equivalent of the bit string that is associated with mj's functional values, which can be obtained in turn by reading the jth column of binary digits in the Table as the corresponding range of boolean values, taking them up in the order from bottom to top.
x : | 1100 | f | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m | m |
y : | 1010 | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | 22 | 23 | |
f0 | 0000 | ( ) | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 |
f1 | 0001 | (x)(y) | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | ||
f2 | 0010 | (x) y | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | ||||
f3 | 0011 | (x) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | ||||||||
f4 | 0100 | x (y) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||||||||||
f5 | 0101 | (y) | ||||||||||||||||||||||||
f6 | 0110 | (x, y) | ||||||||||||||||||||||||
f7 | 0111 | (x y) | ||||||||||||||||||||||||
f8 | 1000 | x y | ||||||||||||||||||||||||
f9 | 1001 | ((x, y)) | ||||||||||||||||||||||||
f10 | 1010 | y | ||||||||||||||||||||||||
f11 | 1011 | (x (y)) | ||||||||||||||||||||||||
f12 | 1100 | x | ||||||||||||||||||||||||
f13 | 1101 | ((x) y) | ||||||||||||||||||||||||
f14 | 1110 | ((x)(y)) | ||||||||||||||||||||||||
f15 | 1111 | (( )) |
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 Υ, 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 \(\Upsilon\!\) can be expressed as a union of function types, in the following manner:
\[\Upsilon : \cup^{m = 1, 2, 3}((\mathbb{B}^k \to \mathbb{B})^m \to \mathbb{B}).\]
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:
- Υpr q = Υ(p, q, r)
- Υpr : (Bk → B) → B
The intention of this operator is that we evaluate the proposition q on each model of the proposition p and combine the results according to the method indicated by the connective parameter r. In principle, the index r might specify any connective on as many as 2k 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 p, r is assigned a default value that is understood to be in force when the corresponding argument place is left blank, specifically, the constant proposition 1 : Bk → B for the lower index p, and the continued conjunction or continued product operation Π for the upper index r. Taking the upper default value gives license to the following readings:
1. | Υp q = Υ(p, q) = Υ(p, q, Π). |
2. | Υp = Υ(p, __, Π) : (Bk → B) → B. |
This means that Υp 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.
Throwing in the lower default value permits the following abbreviations:
3. | Υq = Υ(q) = Υ1 q = Υ(1, q, Π). |
4. | Υ = Υ(1, __, Π) : (Bk → B) → B. |
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 : Bk → 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.
Measure for Measure
An acquaintance with the functions of the umpire operator can be gained from Tables 10 and 11, where the 2-dimensional case is worked out in full.
The auxiliary notations:
- αi f = Υ(fi, f),
- βi f = Υ(f, fi),
define two series of measures:
- αi, βi : (B2 → B) → B,
incidentally providing compact names for the column headings of the next two Tables.
x : | 1100 | f | α | α | α | α | α | α | α | α | α | α | α | α | α | α | α | α |
y : | 1010 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 | |
f0 | 0000 | ( ) | 1 | |||||||||||||||
f1 | 0001 | (x)(y) | 1 | 1 | ||||||||||||||
f2 | 0010 | (x) y | 1 | 1 | ||||||||||||||
f3 | 0011 | (x) | 1 | 1 | 1 | 1 | ||||||||||||
f4 | 0100 | x (y) | 1 | 1 | ||||||||||||||
f5 | 0101 | (y) | 1 | 1 | 1 | 1 | ||||||||||||
f6 | 0110 | (x, y) | 1 | 1 | 1 | 1 | ||||||||||||
f7 | 0111 | (x y) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f8 | 1000 | x y | 1 | 1 | ||||||||||||||
f9 | 1001 | ((x, y)) | 1 | 1 | 1 | 1 | ||||||||||||
f10 | 1010 | y | 1 | 1 | 1 | 1 | ||||||||||||
f11 | 1011 | (x (y)) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f12 | 1100 | x | 1 | 1 | 1 | 1 | ||||||||||||
f13 | 1101 | ((x) y) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f14 | 1110 | ((x)(y)) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f15 | 1111 | (( )) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
x : | 1100 | f | β | β | β | β | β | β | β | β | β | β | β | β | β | β | β | β |
y : | 1010 | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | |
f0 | 0000 | ( ) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
f1 | 0001 | (x)(y) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f2 | 0010 | (x) y | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f3 | 0011 | (x) | 1 | 1 | 1 | 1 | ||||||||||||
f4 | 0100 | x (y) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f5 | 0101 | (y) | 1 | 1 | 1 | 1 | ||||||||||||
f6 | 0110 | (x, y) | 1 | 1 | 1 | 1 | ||||||||||||
f7 | 0111 | (x y) | 1 | 1 | ||||||||||||||
f8 | 1000 | x y | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | ||||||||
f9 | 1001 | ((x, y)) | 1 | 1 | 1 | 1 | ||||||||||||
f10 | 1010 | y | 1 | 1 | 1 | 1 | ||||||||||||
f11 | 1011 | (x (y)) | 1 | 1 | ||||||||||||||
f12 | 1100 | x | 1 | 1 | 1 | 1 | ||||||||||||
f13 | 1101 | ((x) y) | 1 | 1 | ||||||||||||||
f14 | 1110 | ((x)(y)) | 1 | 1 | ||||||||||||||
f15 | 1111 | (( )) | 1 |
Applied to a given proposition f, the qualifiers αi and βi tell whether f rests "above fi" or "below fi", 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.
α00 f = 1 | iff | f00 ⇒ f, | iff | 0 ⇒ f, | hence | α00 f = 1 for all f. | |
α15 f = 1 | iff | f15 ⇒ f, | iff | 1 ⇒ f, | hence | α15 f = 1 ⇒ f = 1. | |
β00 f = 1 | iff | f ⇒ f00, | iff | f ⇒ 0, | hence | β00 f = 1 ⇒ f = 0. | |
β15 f = 1 | iff | f ⇒ f15, | iff | f ⇒ 1, | hence | β15 f = 1 for all f. |
Thus, α0 = β15 is a totally indiscriminate measure, one that accepts all propositions f : B2 → B, whereas α15 and β0 are measures that value the constant propositions 1 : B2 → B and 0 : B2 → B, respectively, above all others.
Finally, in conformity with the use of the fiber notation to indicate sets of models, it is natural to use notations like:
- [| αi |] = (αi)(–1)(1),
- [| βi |] = (βi)(–1)(1),
- [| Υp |] = (Υp)(–1)(1),
to denote sets of propositions that satisfy the umpires in question.
Extending the Existential Interpretation to Quantificational Logic
Previously I introduced a calculus for propositional logic, fixing its meaning according to what C.S. Peirce called the "existential interpretation". As far as it concerns propositional calculus this interpretation settles the meanings that are associated with merely the most basic symbols and logical connectives. Now we must extend and refine the existential interpretation to comprehend the analysis of "quantifications", that is, quantified propositions. In doing so we recognize two additional aspects of logic that need to be developed, over and above the material of propositional logic. At the formal extreme there is the aspect of higher order functional types, into which we have already ventured a little above. At the level of the fundamental content of the available propositions we have to introduce a different interpretation for what we may call "elemental" or "singular" propositions.
Let us return to the 2-dimensional case X° = [x, y]. In order to provide a bridge between propositions and quantifications it serves to define a set of qualifiers Luv : (B2 → B) → B that have the following characters:
L00 f | ||
= | L"(x)(y)" f | |
= | α1 f | |
= | Υ"(x)(y)" f | |
= | Υ"(x)(y) ⇒ f" | |
= | "f likes (x)(y)" |
L01 f | ||
= | L"(x) y " f | |
= | α2 f | |
= | Υ"(x) y " f | |
= | Υ"(x) y ⇒ f" | |
= | "f likes (x) y " |
L10 f | ||
= | L" x (y)" f | |
= | α4 f | |
= | Υ"x (y)" f | |
= | Υ"x (y) ⇒ f" | |
= | "f likes x (y)" |
L11 f | ||
= | L" x y" f | |
= | α8 f | |
= | Υ"x y" f | |
= | Υ"x y ⇒ f" | |
= | "f likes x y" |
Intuitively, the Luv 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 [L00, L01, L10, L11] that takes place within the higher order universe of discourse X°2 = [X°] = [[x, y]]. Figure 12 summarizes the action of the Luv on the fi within X°2.
o-----------------------------------------------------------o | | | o | | / \ | | / \ | | /x y\ | | / o---o \ | | o \ / o | | / \ o / \ | | / \ | / \ | | / \ @ / \ | | / x y \ / x y \ | | o o---o o o---o o | | / \ \ / \ / / \ | | / \ @ / \ @ / \ | | / \ / \ / \ | | / y \ / \ / y \ | | o @ o @ o o o | | / \ / \ / \ | / \ | | / \ / \ / \ @ / \ | | / \ /x y\ / \ / \ | | / x y \ / o o \ / x y \ / x y \ | | o @ o \ / o o o o o o | | |\ / \ o / \ | / \ \ / /| | | | \ / \ | / \ @ / \ @ / | | | | \ / \ @ / \ / \ / | | | | \ / x \ / x y \ / x \ / | | | | o @ o o---o o o o | | | | |\ / \ \ / / \ | /| | | | | | \ / \ @ / \ @ / | | | | | | \ / \ / \ / | | | | |L_11| \ / o y \ / x o \ / |L_00| | | o---------o | o | o---------o | | | \ x @ / \ @ y / | | | | \ / \ / | | | | \ / \ / | | | |L_10 \ / o \ / L_01| | | o---------o | o---------o | | \ @ / | | \ / | | \ / | | \ / | | o | | | o-----------------------------------------------------------o Figure 12. Higher Order Universe of Discourse [L_uv] c [[x, y]]
Application of Higher Order Propositions to Quantification Theory
Our excursion into the vastening landscape of higher order propositions has finally come round to the stage where we can bring its returns to bear on opening up new perspectives for quantificational logic.
There is a question arising next that is still experimental in my mind. Whether it makes much difference from a purely formal point of view is not a question I can answer yet, but it does seem to aid the intuition to invent a slightly different interpretation for the two-valued space that we use as the target of our basic indicator functions. Therefore, let us declare a type of "existential-valued" functions f : Bk → E, where E = {–e, +e} = {"empty", "exist"} is a couple of values that we interpret as indicating whether of not anything exists in the cells of the underlying universe of discourse, venn diagram, or other domain. As usual, let us not be too strict about the coding of these functions, reverting to binary codes whenever the interpretation is clear enough.
With this interpretation in mind we note the following correspondences between classical quantifications and higher order indicator functions:
A | Universal Affirmative | All | x | is | y | Indicator of " x (y)" = 0 |
E | Universal Negative | All | x | is | (y) | Indicator of " x y " = 0 |
I | Particular Affirmative | Some | x | is | y | Indicator of " x y " = 1 |
O | Particular Negative | Some | x | is | (y) | Indicator of " x (y)" = 1 |
Tables 14 and 15 develop these ideas in more detail.
Mnemonic | Category | Classical Form | Alternate Form | Symmetric Form | Operator |
E Exclusive |
Universal Negative |
All x is (y) | No x is y | (L11) | |
A Absolute |
Universal Affirmative |
All x is y | No x is (y) | (L10) | |
All y is x | No y is (x) | No (x) is y | (L01) | ||
All (y) is x | No (y) is (x) | No (x) is (y) | (L00) | ||
Some (x) is (y) | Some (x) is (y) | L00 | |||
Some (x) is y | Some (x) is y | L01 | |||
O Obtrusive |
Particular Negative |
Some x is (y) | Some x is (y) | L10 | |
I Indefinite |
Particular Affirmative |
Some x is y | Some x is y | L11 |
x : | 1100 | f | (L11) | (L10) | (L01) | (L00) | L00 | L01 | L10 | L11 |
y : | 1010 | no x is y |
no x is (y) |
no (x) is y |
no (x) is (y) |
some (x) is (y) |
some (x) is y |
some x is (y) |
some x is y | |
f0 | 0000 | ( ) | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 |
f1 | 0001 | (x)(y) | 1 | 1 | 1 | 0 | 1 | 0 | 0 | 0 |
f2 | 0010 | (x) y | 1 | 1 | 0 | 1 | 0 | 1 | 0 | 0 |
f3 | 0011 | (x) | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 |
f4 | 0100 | x (y) | 1 | 0 | 1 | 1 | 0 | 0 | 1 | 0 |
f5 | 0101 | (y) | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 |
f6 | 0110 | (x, y) | 1 | 0 | 0 | 1 | 0 | 1 | 1 | 0 |
f7 | 0111 | (x y) | 1 | 0 | 0 | 0 | 1 | 1 | 1 | 0 |
f8 | 1000 | x y | 0 | 1 | 1 | 1 | 0 | 0 | 0 | 1 |
f9 | 1001 | ((x, y)) | 0 | 1 | 1 | 0 | 1 | 0 | 0 | 1 |
f10 | 1010 | y | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 |
f11 | 1011 | (x (y)) | 0 | 1 | 0 | 0 | 1 | 1 | 0 | 1 |
f12 | 1100 | x | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 |
f13 | 1101 | ((x) y) | 0 | 0 | 1 | 0 | 1 | 0 | 1 | 1 |
f14 | 1110 | ((x)(y)) | 0 | 0 | 0 | 1 | 0 | 1 | 1 | 1 |
f15 | 1111 | (( )) | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 |