Difference between revisions of "Directory:Jon Awbrey/Papers/Functional Logic : Quantification Theory"

MyWikiBiz, Author Your Legacy — Friday November 22, 2024
Jump to navigationJump to search
(→‎Higher Order Propositions and Logical Operators (''n'' = 2): used bold code font for cactus language)
(table captions)
 
(29 intermediate revisions by the same user not shown)
Line 2: Line 2:
 
==Toward a Functional Conception of Quantificational Logic==
 
==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 <math>\forall_{x \in X} f(x)</math> and <math>\exists_{x \in X} f(x)</math> 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.
+
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 <math>\forall_{x \in X} f(x)\!</math> and <math>\exists_{x \in X} f(x)\!</math> 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===
 
===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.
+
By way of equipping this inquiry with a bit of concrete material, I begin with a consideration of ''higher order propositional expressions'', in particular, those that stem from the propositions on 1 and 2 variables.
 +
 
 +
'''Note on notation.'''  The discussion that follows uses [[minimal negation operation]]s, expressed as bracketed tuples of the form <math>\texttt{(} e_1 \texttt{,} \ldots \texttt{,} e_k \texttt{)},\!</math> and logical conjunctions, expressed as concatenated tuples of the form <math>e_1 ~\ldots~ e_k,\!</math> as the sole expression-forming operations of a calculus for [[boolean-valued functions]] or "propositions".  The expressions of this calculus parse into data structures whose underlying graphs are called ''cacti'' by graph theorists.  Hence the name ''[[cactus language]]'' for this dialect of propositional calculus.
  
 
====Higher Order Propositions and Logical Operators (''n'' = 1)====
 
====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 <math>f : X \to \mathbb{B},</math> then the next higher order of propositions consists of maps of the type <math>m : (X \to \mathbb{B}) \to \mathbb{B}.</math>
+
A ''higher order proposition'' is, very roughly speaking, a proposition about propositions.  If the original order of propositions is a class of indicator functions <math>f : X \to \mathbb{B},\!</math> then the next higher order of propositions consists of maps of the type <math>m : (X \to \mathbb{B}) \to \mathbb{B}.\!</math>
 +
 
 +
For example, consider the case where <math>X = \mathbb{B}.\!</math>  Then there are exactly four propositions <math>f : \mathbb{B} \to \mathbb{B},\!</math> and exactly sixteen higher order propositions that are based on this set, all bearing the type <math>m : (\mathbb{B} \to \mathbb{B}) \to \mathbb{B}.\!</math>
  
For example, consider the case where <math>X = \mathbb{B}.</math> Then there are exactly four propositions <math>f : \mathbb{B} \to \mathbb{B},</math> and exactly sixteen higher order propositions that are based on this set, all bearing the type <math>m : (\mathbb{B} \to \mathbb{B}) \to \mathbb{B}.</math>
+
Table&nbsp;1 lists the sixteen higher order propositions about propositions on one boolean variable, organized in the following fashion: Columns&nbsp;1 and 2 form a truth table for the four <math>f : \mathbb{B} \to \mathbb{B},\!</math> turned on its side from the way that one is most likely accustomed to see truth tables, with the row leaders in Column&nbsp;1 displaying the names of the functions <math>f_i,\!</math> for <math>i\!</math> = 1 to 4, while the entries in Column&nbsp;2 give the values of each function for the argument values that are listed in the corresponding column head.  Column&nbsp;3 displays one of the more usual expressions for the proposition in question.  The last sixteen columns are topped by a collection of conventional names for the higher order propositions, also known as the ''measures'' <math>m_j,\!</math> for <math>j\!</math> = 0 to 15, where the entries in the body of the Table record the values that each <math>m_j\!</math> assigns to each <math>f_i.\!</math>
  
Table&nbsp;1 lists the sixteen higher order propositions about propositions on one boolean variable, organized in the following fashion:  Columns&nbsp;1 and 2 form a truth table for the four <math>f : \mathbb{B} \to \mathbb{B},</math> turned on its side from the way that one is most likely accustomed to see truth tables, with the row leaders in Column&nbsp;1 displaying the names of the functions <math>f_i,\!</math> for <math>i\!</math> = 1 to 4, while the entries in Column&nbsp;2 give the values of each function for the argument values that are listed in the corresponding column head.  Column&nbsp;3 displays one of the more usual expressions for the proposition in question.  The last sixteen columns are topped by a collection of conventional names for the higher order propositions, also known as the ''measures'' <math>m_j,\!</math> for <math>j\!</math> = 0 to 15, where the entries in the body of the Table record the values that each <math>m_j\!</math> assigns to each <math>f_i.\!</math>
+
<br>
  
 
{| align="center" border="1" cellpadding="4" cellspacing="0" style="background:white; color:black; font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="4" cellspacing="0" style="background:white; color:black; font-weight:bold; text-align:center; width:96%"
|+ '''Table 1. Higher Order Propositions (''n'' = 1)'''
+
|+ style="height:30px" |
 +
<math>\text{Table 1.} ~~ \text{Higher Order Propositions} ~~ (n = 1)\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
| align="right" | <math>x:</math>
+
| align="right" | <math>x:\!</math>
 
| 1 0
 
| 1 0
 
| <math>f\!</math>
 
| <math>f\!</math>
| <math>m_0</math>
+
| <math>m_0\!</math>
| <math>m_1</math>
+
| <math>m_1\!</math>
| <math>m_2</math>
+
| <math>m_2\!</math>
| <math>m_3</math>
+
| <math>m_3\!</math>
| <math>m_4</math>
+
| <math>m_4\!</math>
| <math>m_5</math>
+
| <math>m_5\!</math>
| <math>m_6</math>
+
| <math>m_6\!</math>
| <math>m_7</math>
+
| <math>m_7\!</math>
| <math>m_8</math>
+
| <math>m_8\!</math>
| <math>m_9</math>
+
| <math>m_9\!</math>
| <math>m_{10}</math>
+
| <math>m_{10}\!</math>
| <math>m_{11}</math>
+
| <math>m_{11}\!</math>
| <math>m_{12}</math>
+
| <math>m_{12}\!</math>
| <math>m_{13}</math>
+
| <math>m_{13}\!</math>
| <math>m_{14}</math>
+
| <math>m_{14}\!</math>
| <math>m_{15}</math>
+
| <math>m_{15}\!</math>
 
|-
 
|-
| <math>f_0</math>
+
| <math>f_0\!</math>
 
| 0 0
 
| 0 0
 
| <math>0\!</math>
 
| <math>0\!</math>
Line 51: Line 56:
 
| 0 || style="background:black; color:white" | 1
 
| 0 || style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_1</math>
+
| <math>f_1\!</math>
 
| 0 1
 
| 0 1
 
| <math>(x)\!</math>
 
| <math>(x)\!</math>
Line 67: Line 72:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_2</math>
+
| <math>f_2\!</math>
 
| 1 0
 
| 1 0
 
| <math>x\!</math>
 
| <math>x\!</math>
Line 81: Line 86:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_3</math>
+
| <math>f_3\!</math>
 
| 1 1
 
| 1 1
 
| <math>1\!</math>
 
| <math>1\!</math>
Line 93: Line 98:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
|}<br>
+
|}
 +
 
 +
<br>
  
 
I am going to put off explaining Table&nbsp;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&nbsp;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.
 +
 +
<br>
  
 
{| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|+ '''Table 2. Interpretive Categories for Higher Order Propositions (''n'' = 1)'''
+
|+ style="height:30px" |
 +
<math>\text{Table 2.} ~~ \text{Interpretive Categories for Higher Order Propositions} ~~ (n = 1)\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
 
| Measure
 
| Measure
Line 235: Line 245:
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
|}<br>
+
|}
 +
 
 +
<br>
  
 
====Higher Order Propositions and Logical Operators (''n'' = 2)====
 
====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 <math>X^\circ = [\mathcal{X}] = [x_1, x_2] = [u, v],</math> based on two logical features or boolean variables <math>u\!</math> and <math>v.\!</math>
+
By way of reviewing notation and preparing to extend it to higher order universes of discourse, let us first consider the universe of discourse <math>X^\Box = [\mathcal{X}] = [x_1, x_2] = [u, v],\!</math> based on two logical features or boolean variables <math>u\!</math> and <math>v.\!</math>
  
The universe of discourse <math>X^\circ\!</math> consists of two parts, a set of ''points'' and a set of ''propositions''.
+
The universe of discourse <math>X^\Box\!</math> consists of two parts, a set of ''points'' and a set of ''propositions''.
  
: The points of <math>X^\circ</math> form the space:
+
The points of <math>X^\Box\!</math> form the space:
  
:: <math>X = \langle \mathcal{X} \rangle = \langle u, v \rangle = \{ (u, v) \} \cong \mathbb{B}^2.</math>
+
{| align="center" cellpadding="8"
 +
| <math>X \quad = \quad \langle \mathcal{X} \rangle \quad = \quad \langle u, v \rangle \quad = \quad \{ (u, v) \} \quad \cong \quad \mathbb{B}^2.\!</math>
 +
|}
  
: Each point in <math>X\!</math> may be described by means of a ''singular proposition'', that is, a proposition that describes it uniquely.  This form of representation leads to the following enumeration of points:
+
Each point in <math>X\!</math> may be indicated by means of a ''singular proposition'', that is, a proposition that describes it uniquely.  This form of representation leads to the following enumeration of points, presented in two different styles of typography that are used in this text:
  
:: '''<math>X = \{\!</math>&nbsp;<code>(u)(v)</code>&nbsp;,&nbsp;<code>(u)v</code>&nbsp;,&nbsp; <code>u(v)</code>&nbsp;,&nbsp;<code>uv</code>&nbsp;<math>\} \cong \mathbb{B}^2.</math>'''
+
{| align="center" cellpadding="8" style="text-align:center"
 +
| <math>X\!</math>
 +
| <math>=\!</math>
 +
| <math>\{\!</math>'''<font size="+1">&nbsp;<code>(u)(v)</code>,&nbsp;&nbsp;<code>(u)v</code>,&nbsp;&nbsp;<code>u(v)</code>,&nbsp;&nbsp;<code>uv</code>&nbsp;</font>'''<math>\}\!</math>
 +
| <math>\cong\!</math>
 +
| <math>\mathbb{B}^2,\!</math>
 +
|-
 +
| <math>X\!</math>
 +
| <math>=\!</math>
 +
| <math>\{\ \underline{(u)(v)},\ \underline{(u)v},\ \underline{u(v)},\ \underline{uv}\ \}\!</math>
 +
| <math>\cong\!</math>
 +
| <math>\mathbb{B}^2.\!</math>
 +
|}
  
: Each point in <math>X\!</math> may also be described by means of its ''coordinates'', that is, by the ordered pair of values in <math>\mathbb{B}</math> that the coordinate propositions <math>u\!</math> and <math>v\!</math> take on that point.  This form of representation leads to the following enumeration of points:
+
Each point in <math>X\!</math> may also be described by means of its ''coordinates'', that is, by the ordered pair of values in <math>\mathbb{B}\!</math> that the coordinate propositions <math>u\!</math> and <math>v\!</math> take on that point.  This form of representation leads to the following enumeration of points:
  
:: <math>X = \{\ (0, 0),\ (0, 1),\ (1, 0),\ (1, 1)\ \} \cong \mathbb{B}^2.</math>
+
{| align="center" cellpadding="8" style="text-align:center"
 +
| <math>X\!</math>
 +
| <math>=\!</math>
 +
| <math>\{\ (0, 0),\ (0, 1),\ (1, 0),\ (1, 1)\ \}\!</math>
 +
| <math>\cong\!</math>
 +
| <math>\mathbb{B}^2.\!</math>
 +
|}
  
: The propositions of <math>X^\circ</math> form the space:
+
The propositions of <math>X^\Box\!</math> form the space:
  
:: <math>X^\uparrow = (X \to \mathbb{B}) = \{ f : X \to \mathbb{B} \} \cong (\mathbb{B}^2 \to \mathbb{B}).</math>
+
{| align="center" cellpadding="8"
 +
| <math>X^\uparrow \quad = \quad (X \to \mathbb{B}) \quad = \quad \{ f : X \to \mathbb{B} \} \quad \cong \quad (\mathbb{B}^2 \to \mathbb{B}).\!</math>
 +
|}
  
 
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] = [[u, v]],</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^\Box\!</math> is <math>X^{\Box\,2} = [X^\Box] = [[u, v]],\!</math> which may be developed in the following way.  The propositions of <math>X^\Box\!</math> become the points of <math>X^{\Box\,2},\!</math> and the mappings of the type <math>m : (X \to \mathbb{B}) \to \mathbb{B}\!</math> become the propositions of <math>X^{\Box\,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 <math>[u, v]\!</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.
+
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>[u, v]\!</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 <math>2^{16} = 65536\!</math> measures of the type <math>m : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}.</math>  Table&nbsp;3 introduces the first 24 of these measures in the fashion of the higher order truth table that I used before.  The column headed <math>m_j\!</math> shows the values of the measure <math>m_j\!</math> on each of the propositions <math>f_i : \mathbb{B}^2 \to \mathbb{B},</math> for <math>i\!</math> = 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 <math>j\!</math> of the measure <math>m_j\!</math> is the decimal equivalent of the bit string that is associated with <math>m_j\!</math>'s functional values, which can be obtained in turn by reading the <math>j^\mathrm{th}\!</math> 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 <math>2^{16} = 65536\!</math> measures of the type <math>m : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}.\!</math>  Table&nbsp;3 introduces the first 24 of these measures in the fashion of the higher order truth table that I used before.  The column headed <math>m_j\!</math> shows the values of the measure <math>m_j\!</math> on each of the propositions <math>f_i : \mathbb{B}^2 \to \mathbb{B},\!</math> for <math>i\!</math> = 0 to 15, 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 <math>j\!</math> of the measure <math>m_j\!</math> is the decimal equivalent of the bit string that is associated with <math>m_j\!</math>'s functional values, which can be obtained in turn by reading the <math>j^\mathrm{th}\!</math> column of binary digits in the Table as the corresponding range of boolean values, taking them up in the order from bottom to top.
 +
 
 +
<br>
  
 
{| align="center" border="1" cellpadding="0" cellspacing="0" style="background:white; color:black; font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="0" cellspacing="0" style="background:white; color:black; font-weight:bold; text-align:center; width:96%"
|+ '''Table 3. Higher Order Propositions (''n'' = 2)'''
+
|+ style="height:30px" |
 +
<math>\text{Table 3.} ~~ \text{Higher Order Propositions} ~~ (n = 2)\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
| align="right" | <math>u:</math><br><math>v:</math>
+
| align="right" | <math>u\!:</math><br><math>v\!:</math>
 
| 1100<br>1010
 
| 1100<br>1010
 
| <math>f\!</math>
 
| <math>f\!</math>
| <math>m_0</math>
+
| <math>m_0\!</math>
| <math>m_1</math>
+
| <math>m_1\!</math>
| <math>m_2</math>
+
| <math>m_2\!</math>
| <math>m_3</math>
+
| <math>m_3\!</math>
| <math>m_4</math>
+
| <math>m_4\!</math>
| <math>m_5</math>
+
| <math>m_5\!</math>
| <math>m_6</math>
+
| <math>m_6\!</math>
| <math>m_7</math>
+
| <math>m_7\!</math>
| <math>m_8</math>
+
| <math>m_8\!</math>
| <math>m_9</math>
+
| <math>m_9\!</math>
| <math>m_{10}</math>
+
| <math>m_{10}\!</math>
| <math>m_{11}</math>
+
| <math>m_{11}\!</math>
| <math>m_{12}</math>
+
| <math>m_{12}\!</math>
| <math>m_{13}</math>
+
| <math>m_{13}\!</math>
| <math>m_{14}</math>
+
| <math>m_{14}\!</math>
| <math>m_{15}</math>
+
| <math>m_{15}\!</math>
| <math>m_{16}</math>
+
| <math>m_{16}\!</math>
| <math>m_{17}</math>
+
| <math>m_{17}\!</math>
| <math>m_{18}</math>
+
| <math>m_{18}\!</math>
| <math>m_{19}</math>
+
| <math>m_{19}\!</math>
| <math>m_{20}</math>
+
| <math>m_{20}\!</math>
| <math>m_{21}</math>
+
| <math>m_{21}\!</math>
| <math>m_{22}</math>
+
| <math>m_{22}\!</math>
| <math>m_{23}</math>
+
| <math>m_{23}\!</math>
|-
+
|-
| <math>f_0</math>
+
| <math>f_0\!</math>
| 0000
+
| 0000
| <math>(~)</math>
+
| <math>(~)\!</math>
| 0 || style="background:black; color:white" | 1
+
| 0 || style="background:black; color:white" | 1
| 0 || style="background:black; color:white" | 1
+
| 0 || style="background:black; color:white" | 1
| 0 || style="background:black; color:white" | 1
+
| 0 || style="background:black; color:white" | 1
| 0 || style="background:black; color:white" | 1
+
| 0 || style="background:black; color:white" | 1
| 0 || style="background:black; color:white" | 1
+
| 0 || style="background:black; color:white" | 1
 
| 0 || style="background:black; color:white" | 1
 
| 0 || style="background:black; color:white" | 1
 
| 0 || style="background:black; color:white" | 1
 
| 0 || style="background:black; color:white" | 1
Line 314: Line 351:
 
| 0 || style="background:black; color:white" | 1
 
| 0 || style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_1</math>
+
| <math>f_1\!</math>
 
| 0001
 
| 0001
 
| <math>(u)(v)\!</math>
 
| <math>(u)(v)\!</math>
Line 336: Line 373:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_2</math>
+
| <math>f_2\!</math>
 
| 0010
 
| 0010
 
| <math>(u) v\!</math>
 
| <math>(u) v\!</math>
Line 355: Line 392:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_3</math>
+
| <math>f_3\!</math>
 
| 0011
 
| 0011
| <math>(u)\!</math>
+
| <math>(u)~\!</math>
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 369: Line 406:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_4</math>
+
| <math>f_4\!</math>
 
| 0100
 
| 0100
 
| <math>u (v)\!</math>
 
| <math>u (v)\!</math>
Line 383: Line 420:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_5</math>
+
| <math>f_5\!</math>
 
| 0101
 
| 0101
 
| <math>(v)\!</math>
 
| <math>(v)\!</math>
Line 390: Line 427:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_6</math>
+
| <math>f_6\!</math>
 
| 0110
 
| 0110
 
| <math>(u, v)\!</math>
 
| <math>(u, v)\!</math>
Line 397: Line 434:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_7</math>
+
| <math>f_7\!</math>
 
| 0111
 
| 0111
 
| <math>(u v)\!</math>
 
| <math>(u v)\!</math>
Line 404: Line 441:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_8</math>
+
| <math>f_8\!</math>
 
| 1000
 
| 1000
 
| <math>u v\!</math>
 
| <math>u v\!</math>
Line 411: Line 448:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_9</math>
+
| <math>f_9\!</math>
 
| 1001
 
| 1001
 
| <math>((u, v))\!</math>
 
| <math>((u, v))\!</math>
Line 418: Line 455:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_{10}</math>
+
| <math>f_{10}\!</math>
 
| 1010
 
| 1010
 
| <math>v\!</math>
 
| <math>v\!</math>
Line 425: Line 462:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_{11}</math>
+
| <math>f_{11}\!</math>
 
| 1011
 
| 1011
 
| <math>(u (v))\!</math>
 
| <math>(u (v))\!</math>
Line 432: Line 469:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_{12}</math>
+
| <math>f_{12}\!</math>
 
| 1100
 
| 1100
 
| <math>u\!</math>
 
| <math>u\!</math>
Line 439: Line 476:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_{13}</math>
+
| <math>f_{13}\!</math>
 
| 1101
 
| 1101
 
| <math>((u) v)\!</math>
 
| <math>((u) v)\!</math>
Line 446: Line 483:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_{14}</math>
+
| <math>f_{14}\!</math>
 
| 1110
 
| 1110
| <math>((u)(v))\!</math>
+
| <math>((u)(v))~\!</math>
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
|-
 
|-
| <math>f_{15}</math>
+
| <math>f_{15}\!</math>
 
| 1111
 
| 1111
 
| <math>((~))\!</math>
 
| <math>((~))\!</math>
Line 459: Line 496:
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
 
| 0 || 0 || 0 || 0 || 0 || 0 || 0 || 0
|}<br>
+
|}
 +
 
 +
<br>
  
 
===Umpire Operators===
 
===Umpire Operators===
  
====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 : (\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 : (\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.
+
Given an ordered pair of propositions <math>e, f : \langle u, v \rangle \to \mathbb{B}\!</math> as arguments, the relative operator reports the value 1 if the first implies the second, otherwise 0.
  
The relative operator takes two propositions as arguments and reports the value "true" if the first implies the second, otherwise "false".
+
{| align="center" cellpadding="8" style="text-align:center"
 
+
| <math>\Upsilon (e, f) = 1\!</math>
<br>
+
| <math>\operatorname{if~and~only~if}\!</math>
<center>
+
| <math>e \Rightarrow f.\!</math>
<math>\Upsilon \langle e, f \rangle = 1 \quad \operatorname{iff} \quad e \Rightarrow f.</math>
+
|}
</center>
 
<br>
 
  
 
Expressing it another way, we may also write:
 
Expressing it another way, we may also write:
  
<br>
+
{| align="center" cellpadding="8" style="text-align:center"
<center>
+
| <math>\Upsilon (e, f) = 1\!</math>
<math>\Upsilon \langle e, f \rangle = 1 \quad \Leftrightarrow \quad (e (f)) = 1.</math>
+
| <math>\Leftrightarrow\!</math>
</center>
+
| <math>\underline{(e (f))} = \underline{1}.\!</math>
<br>
+
|}
  
 
In writing this, however, it is important to notice that the 1's appearing on the left and right have different meanings.  Filling in the details, we have:
 
In writing this, however, it is important to notice that the 1's appearing on the left and right have different meanings.  Filling in the details, we have:
  
<br>
+
{| align="center" cellpadding="8" style="text-align:center"
<center>
+
| <math>\Upsilon (e, f) = 1 \in \mathbb{B}\!</math>
<math>\Upsilon \langle e, f \rangle = 1 \in \mathbb{B} \quad \Leftrightarrow \quad (e (f)) = 1 : \mathbb{B}^2 \to \mathbb{B}.</math>
+
| <math>\Leftrightarrow\!</math>
</center>
+
| <math>\underline{(e (f))} = 1 : \langle u, v \rangle \to \mathbb{B}.\!</math>
<br>
+
|}
  
Finally, it is often convenient to write the first argument as a subscript, hence <math>\Upsilon_e \langle f \rangle = \Upsilon \langle e, f \rangle.</math>
+
Writing types as subscripts and using the fact that <math>X = \langle u, v \rangle,\!</math> it is possible to express this a little more succinctly as follows:
  
As a special application of this operator, we next define the absolute umpire operator, also called the "umpire measure".  This is a higher order proposition <math>\Upsilon_1 : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}</math> which is given by the relation <math>\Upsilon_1 \langle f \rangle = \Upsilon \langle 1, f \rangle.</math> Here, the subscript "1" on the left and the argument "1" on the right both refer to the constant proposition <math>1 : \mathbb{B}^2 \to \mathbb{B}.</math>  In most contexts where <math>\Upsilon_1\!</math> is actually applied the reference to "1" is safely omitted, since the number of arguments indicates which type of operator is intended.  Thus, we have the following identities and equivalents:
+
{| align="center" cellpadding="8" style="text-align:center"
 +
| <math>\Upsilon (e, f) = 1_\mathbb{B}\!</math>
 +
| <math>\Leftrightarrow\!</math>
 +
| <math>\underline{(e (f))} = 1_{X \to \mathbb{B}}.\!</math>
 +
|}
  
<br>
+
Finally, it is often convenient to write the first argument as a subscript, hence <math>\Upsilon_e (f) = \Upsilon (e, f).\!</math>
<center>
 
<math>\Upsilon f = \Upsilon_1 \langle f \rangle = 1 \in \mathbb{B} \quad \Leftrightarrow \quad (1 (f)) = 1 \quad \Leftrightarrow \quad f = 1 : \mathbb{B}^2 \to \mathbb{B}.</math>
 
</center>
 
<br>
 
  
The umpire measure is defined at the level of truth functions, but can also be understood in terms of its implied judgments at the syntactic levelInterpreted this way, <math>\Upsilon_1\!</math> recognizes theorems of the propositional calculus over <math>[u, v],\!</math> giving a score of "1" to tautologies and a score of "0" to everything else, regarding all contingent statements as no better than falsehoods.
+
As a special application of this operator, we next define the absolute umpire operator, also called the ''umpire measure''This is a higher order proposition <math>\Upsilon_1 : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}\!</math> which is given by the relation <math>\Upsilon_1 (f) = \Upsilon (1, f).\!</math> Here, the subscript 1 on the left and the argument 1 on the right both refer to the constant proposition <math>1 : \mathbb{B}^2 \to \mathbb{B}.\!</math>  In most contexts where <math>\Upsilon_1\!</math> is actually applied the subscript 1 is safely omitted, since the number of arguments indicates which type of operator is intended. Thus, we have the following identities and equivalents:
  
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 vesrion could have been defined as <math>\Upsilon_e f = \Upsilon (e (f)).\!</math>
+
{| align="center" cellpadding="10" style="text-align:center"
 +
| <math>\Upsilon f = \Upsilon_1 (f) = 1 \in \mathbb{B}\!</math>
 +
| <math>\Leftrightarrow\!</math>
 +
| <math>\underline{(1~(f))} = \underline{1}\!</math>
 +
| <math>\Leftrightarrow\!</math>
 +
| <math>f = 1 : \mathbb{B}^2 \to \mathbb{B}.\!</math>
 +
|}
  
====Option 2 : More General====
+
The umpire measure is defined at the level of truth functions, but can also be understood in terms of its implied judgments at the syntactic levelInterpreted this way, <math>\Upsilon_1\!</math> recognizes theorems of the propositional calculus over <math>[u, v],\!</math> giving a score of "1" to tautologies and a score of "0" to everything else, regarding all contingent statements as no better than falsehoods.
 
 
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 toolsSpecifically, 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:
 
 
 
: <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 questionThus, we have the following forms:
+
One remark in passing for those who might prefer an alternative definitionIf 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>
 
 
: <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:
 
 
 
{| cellpadding="4"
 
| align="right" width="36" | 1.
 
| <math>\Upsilon_p q = \Upsilon (p, q) = \Upsilon (p, q, \textstyle\prod).</math>
 
|-
 
| align="right" width="36" | 2.
 
| <math>\Upsilon_p = \Upsilon (p, \underline{~~}, \textstyle\prod) : (\mathbb{B}^k \to \mathbb{B}) \to \mathbb{B}.</math>
 
|}<br>
 
 
 
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>(\!| p (\!| q |\!) |\!) = 1.</math>
 
 
 
Throwing in the lower default value permits the following abbreviations:
 
 
 
{| cellpadding="4"
 
| align="right" width="36" | 3.
 
| <math>\Upsilon  q  = \Upsilon (q) = \Upsilon_1 q = \Upsilon (1, q, \textstyle\prod).</math>
 
|-
 
| align="right" width="36" | 4.
 
| <math>\Upsilon = \Upsilon (1, \underline{~~}, \textstyle\prod)) : (\mathbb{B}^k\ \to \mathbb{B}) \to \mathbb{B}.</math>
 
|}<br>
 
 
 
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.
 
  
 
===Measure for Measure===
 
===Measure for Measure===
Line 546: Line 557:
  
 
{| align="center" cellpadding="8"
 
{| align="center" cellpadding="8"
| <math>\alpha_i, \beta_i : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}, i = 0 \ldots 15,</math>
+
| <math>\alpha_i, \beta_i : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}, i = 0 \ldots 15,\!</math>
 
|}
 
|}
  
Line 552: Line 563:
  
 
{| align="center" cellpadding="8"
 
{| align="center" cellpadding="8"
| <math>\alpha_i f = \Upsilon \langle f_i, f \rangle = \Upsilon \langle f_i \Rightarrow f \rangle,</math>
+
| <math>\alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f),\!</math>
 
|-
 
|-
| <math>\beta_i f = \Upsilon \langle f, f_i \rangle = \Upsilon \langle f \Rightarrow f_i \rangle.</math>
+
| <math>\beta_i f = \Upsilon (f, f_i) = \Upsilon (f \Rightarrow f_i).\!</math>
 
|}
 
|}
  
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&nbsp;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.
+
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&nbsp;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.
 +
 
 +
<br>
  
 
{| align="center" border="1" cellpadding="1" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="1" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|+ '''Table 4. Qualifiers of Implication Ordering:&nbsp; <math>\alpha_i f = \Upsilon \langle f_i, f \rangle = \Upsilon \langle f_i \Rightarrow f \rangle</math>'''
+
|+ style="height:30px" |
 +
<math>\text{Table 4.} ~~ \text{Qualifiers of Implication Ordering:} ~~ \alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f)\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
| align="right" | <math>u:</math><br><math>v:</math>
+
| align="right" | <math>u\colon\!</math><br><math>v\colon\!</math>
 
| 1100<br>1010
 
| 1100<br>1010
 
| <math>f\!</math>
 
| <math>f\!</math>
| <math>\alpha_0</math>
+
| <math>\alpha_0~\!</math>
| <math>\alpha_1</math>
+
| <math>\alpha_1\!</math>
| <math>\alpha_2</math>
+
| <math>\alpha_2\!</math>
| <math>\alpha_3</math>
+
| <math>\alpha_3\!</math>
| <math>\alpha_4</math>
+
| <math>\alpha_4\!</math>
| <math>\alpha_5</math>
+
| <math>\alpha_5\!</math>
| <math>\alpha_6</math>
+
| <math>\alpha_6\!</math>
| <math>\alpha_7</math>
+
| <math>\alpha_7\!</math>
| <math>\alpha_8</math>
+
| <math>\alpha_8\!</math>
| <math>\alpha_9</math>
+
| <math>\alpha_9\!</math>
| <math>\alpha_{10}</math>
+
| <math>\alpha_{10}\!</math>
| <math>\alpha_{11}</math>
+
| <math>\alpha_{11}\!</math>
| <math>\alpha_{12}</math>
+
| <math>\alpha_{12}\!</math>
| <math>\alpha_{13}</math>
+
| <math>\alpha_{13}~\!</math>
| <math>\alpha_{14}</math>
+
| <math>\alpha_{14}\!</math>
| <math>\alpha_{15}</math>
+
| <math>\alpha_{15}\!</math>
 
|-
 
|-
| <math>f_0</math>
+
| <math>f_0\!</math>
 
| 0000
 
| 0000
| <math>(~)</math>
+
| <math>(~)\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
Line 602: Line 616:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_1</math>
+
| <math>f_1\!</math>
 
| 0001
 
| 0001
 
| <math>(u)(v)\!</math>
 
| <math>(u)(v)\!</math>
Line 622: Line 636:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_2</math>
+
| <math>f_2\!</math>
 
| 0010
 
| 0010
 
| <math>(u) v\!</math>
 
| <math>(u) v\!</math>
Line 642: Line 656:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_3</math>
+
| <math>f_3\!</math>
 
| 0011
 
| 0011
| <math>(u)\!</math>
+
| <math>(u)~\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 662: Line 676:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_4</math>
+
| <math>f_4\!</math>
 
| 0100
 
| 0100
 
| <math>u (v)\!</math>
 
| <math>u (v)\!</math>
Line 682: Line 696:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_5</math>
+
| <math>f_5\!</math>
 
| 0101
 
| 0101
 
| <math>(v)\!</math>
 
| <math>(v)\!</math>
Line 702: Line 716:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_6</math>
+
| <math>f_6\!</math>
 
| 0110
 
| 0110
 
| <math>(u, v)\!</math>
 
| <math>(u, v)\!</math>
Line 722: Line 736:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_7</math>
+
| <math>f_7\!</math>
 
| 0111
 
| 0111
 
| <math>(u v)\!</math>
 
| <math>(u v)\!</math>
Line 742: Line 756:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_8</math>
+
| <math>f_8\!</math>
 
| 1000
 
| 1000
 
| <math>u v\!</math>
 
| <math>u v\!</math>
Line 762: Line 776:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_9</math>
+
| <math>f_9\!</math>
 
| 1001
 
| 1001
 
| <math>((u, v))\!</math>
 
| <math>((u, v))\!</math>
Line 782: Line 796:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{10}</math>
+
| <math>f_{10}\!</math>
 
| 1010
 
| 1010
 
| <math>v\!</math>
 
| <math>v\!</math>
Line 802: Line 816:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{11}</math>
+
| <math>f_{11}\!</math>
 
| 1011
 
| 1011
 
| <math>(u (v))\!</math>
 
| <math>(u (v))\!</math>
Line 822: Line 836:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{12}</math>
+
| <math>f_{12}\!</math>
 
| 1100
 
| 1100
 
| <math>u\!</math>
 
| <math>u\!</math>
Line 842: Line 856:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{13}</math>
+
| <math>f_{13}\!</math>
 
| 1101
 
| 1101
 
| <math>((u) v)\!</math>
 
| <math>((u) v)\!</math>
Line 862: Line 876:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{14}</math>
+
| <math>f_{14}\!</math>
 
| 1110
 
| 1110
| <math>((u)(v))\!</math>
+
| <math>((u)(v))~\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
Line 882: Line 896:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{15}</math>
+
| <math>f_{15}\!</math>
 
| 1111
 
| 1111
| <math>((~))</math>
+
| <math>((~))\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 901: Line 915:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
|}<br>
+
|}
  
The values of the sixteen <math>\beta_i\!</math> on each of the sixteen boolean functions <math>f : \mathbb{B}^2 \to \mathbb{B}</math> are shown in Table&nbsp;5.  Expressed in terms of the implication ordering on the sixteen functions, <math>\beta_i f = 1\!</math> says that <math>f\!</math> is ''below or identical to'' <math>f_i\!</math> in the implication lattice, that is, <math>\le f_i\!</math> in the implication ordering.
+
<br>
 +
 
 +
The values of the sixteen <math>\beta_i\!</math> on each of the sixteen boolean functions <math>{f : \mathbb{B}^2 \to \mathbb{B}}\!</math> are shown in Table&nbsp;5.  Expressed in terms of the implication ordering on the sixteen functions, <math>{\beta_i f = 1}\!</math> says that <math>f\!</math> is ''below or identical to'' <math>f_i\!</math> in the implication lattice, that is, <math>\le f_i\!</math> in the implication ordering.
 +
 
 +
<br>
  
 
{| align="center" border="1" cellpadding="1" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="1" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|+ '''Table 5. Qualifiers of Implication Ordering:&nbsp; <math>\beta_i f = \Upsilon \langle f, f_i \rangle = \Upsilon \langle f \Rightarrow f_i \rangle</math>'''
+
|+ style="height:30px" |
 +
<math>\text{Table 5.} ~~ \text{Qualifiers of Implication Ordering:} ~~ \beta_i f = \Upsilon (f, f_i) = \Upsilon (f \Rightarrow f_i)\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
| align="right" | <math>u:</math><br><math>v:</math>
+
| align="right" | <math>u\colon\!</math><br><math>v\colon\!</math>
 
| 1100<br>1010
 
| 1100<br>1010
 
| <math>f\!</math>
 
| <math>f\!</math>
| <math>\beta_0</math>
+
| <math>\beta_0\!</math>
| <math>\beta_1</math>
+
| <math>\beta_1\!</math>
| <math>\beta_2</math>
+
| <math>\beta_2\!</math>
| <math>\beta_3</math>
+
| <math>\beta_3\!</math>
| <math>\beta_4</math>
+
| <math>\beta_4\!</math>
| <math>\beta_5</math>
+
| <math>\beta_5\!</math>
| <math>\beta_6</math>
+
| <math>\beta_6\!</math>
| <math>\beta_7</math>
+
| <math>\beta_7\!</math>
| <math>\beta_8</math>
+
| <math>\beta_8\!</math>
| <math>\beta_9</math>
+
| <math>\beta_9\!</math>
| <math>\beta_{10}</math>
+
| <math>\beta_{10}\!</math>
| <math>\beta_{11}</math>
+
| <math>\beta_{11}\!</math>
| <math>\beta_{12}</math>
+
| <math>\beta_{12}\!</math>
| <math>\beta_{13}</math>
+
| <math>\beta_{13}\!</math>
| <math>\beta_{14}</math>
+
| <math>\beta_{14}\!</math>
| <math>\beta_{15}</math>
+
| <math>\beta_{15}\!</math>
 
|-
 
|-
| <math>f_0</math>
+
| <math>f_0\!</math>
 
| 0000
 
| 0000
| <math>(~)</math>
+
| <math>(~)\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 948: Line 967:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_1</math>
+
| <math>f_1\!</math>
 
| 0001
 
| 0001
 
| <math>(u)(v)\!</math>
 
| <math>(u)(v)\!</math>
Line 968: Line 987:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_2</math>
+
| <math>f_2\!</math>
 
| 0010
 
| 0010
 
| <math>(u) v\!</math>
 
| <math>(u) v\!</math>
Line 988: Line 1,007:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_3</math>
+
| <math>f_3\!</math>
 
| 0011
 
| 0011
| <math>(u)\!</math>
+
| <math>(u)~\!</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
Line 1,008: Line 1,027:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_4</math>
+
| <math>f_4\!</math>
 
| 0100
 
| 0100
 
| <math>u (v)\!</math>
 
| <math>u (v)\!</math>
Line 1,028: Line 1,047:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_5</math>
+
| <math>f_5\!</math>
 
| 0101
 
| 0101
 
| <math>(v)\!</math>
 
| <math>(v)\!</math>
Line 1,048: Line 1,067:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_6</math>
+
| <math>f_6\!</math>
 
| 0110
 
| 0110
 
| <math>(u, v)\!</math>
 
| <math>(u, v)\!</math>
Line 1,068: Line 1,087:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_7</math>
+
| <math>f_7\!</math>
 
| 0111
 
| 0111
 
| <math>(u v)\!</math>
 
| <math>(u v)\!</math>
Line 1,088: Line 1,107:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_8</math>
+
| <math>f_8\!</math>
 
| 1000
 
| 1000
 
| <math>u v\!</math>
 
| <math>u v\!</math>
Line 1,108: Line 1,127:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_9</math>
+
| <math>f_9\!</math>
 
| 1001
 
| 1001
 
| <math>((u, v))\!</math>
 
| <math>((u, v))\!</math>
Line 1,128: Line 1,147:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{10}</math>
+
| <math>f_{10}\!</math>
 
| 1010
 
| 1010
 
| <math>v\!</math>
 
| <math>v\!</math>
Line 1,148: Line 1,167:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{11}</math>
+
| <math>f_{11}\!</math>
 
| 1011
 
| 1011
 
| <math>(u (v))\!</math>
 
| <math>(u (v))\!</math>
Line 1,168: Line 1,187:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{12}</math>
+
| <math>f_{12}\!</math>
 
| 1100
 
| 1100
 
| <math>u\!</math>
 
| <math>u\!</math>
Line 1,188: Line 1,207:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{13}</math>
+
| <math>f_{13}\!</math>
 
| 1101
 
| 1101
 
| <math>((u) v)\!</math>
 
| <math>((u) v)\!</math>
Line 1,208: Line 1,227:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{14}</math>
+
| <math>f_{14}\!</math>
 
| 1110
 
| 1110
| <math>((u)(v))\!</math>
+
| <math>((u)(v))~\!</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
Line 1,228: Line 1,247:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{15}</math>
+
| <math>f_{15}\!</math>
 
| 1111
 
| 1111
 
| <math>((~))\!</math>
 
| <math>((~))\!</math>
Line 1,247: Line 1,266:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
|}<br>
+
|}
  
Applied to a given proposition <math>f,\!</math> the qualifiers <math>\alpha_i\!</math> and <math>\beta_i\!</math> tell whether <math>f\!</math> rests <math>\operatorname{above}\ f_i</math> or <math>\operatorname{below}\ f_i,</math> 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.
+
<br>
 +
 
 +
Applied to a given proposition <math>f,\!</math> the qualifiers <math>\alpha_i\!</math> and <math>\beta_i\!</math> tell whether <math>f\!</math> rests <math>\operatorname{above}\ f_i\!</math> or <math>\operatorname{below}\ f_i,\!</math> 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.
  
 
<center><math>\begin{matrix}
 
<center><math>\begin{matrix}
Line 1,284: Line 1,305:
 
\beta_{15} f = 1          &
 
\beta_{15} f = 1          &
 
\operatorname{for~all}\ f. \\
 
\operatorname{for~all}\ f. \\
\end{matrix}</math></center>
+
\end{matrix}\!</math></center>
 
<br>
 
<br>
  
Thus, <math>\alpha_0 = \beta_{15}\!</math> is a totally indiscriminate measure, one that accepts all propositions <math>f : \mathbb{B}^2 \to \mathbb{B},</math> whereas <math>\alpha_{15}\!</math> and <math>\beta_0\!</math> are measures that value the constant propositions <math>1 : \mathbb{B}^2 \to \mathbb{B}</math> and <math>0 : \mathbb{B}^2 \to \mathbb{B},</math> respectively, above all others.
+
Thus, <math>\alpha_0 = \beta_{15}\!</math> is a totally indiscriminate measure, one that accepts all propositions <math>{f : \mathbb{B}^2 \to \mathbb{B}},\!</math> whereas <math>\alpha_{15}\!</math> and <math>\beta_0\!</math> are measures that value the constant propositions <math>1 : \mathbb{B}^2 \to \mathbb{B}\!</math> and <math>0 : \mathbb{B}^2 \to \mathbb{B},\!</math> 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:
 
Finally, in conformity with the use of the fiber notation to indicate sets of models, it is natural to use notations like:
Line 1,311: Line 1,332:
 
Previously I introduced a calculus for propositional logic, fixing its meaning according to what C.S.&nbsp;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.
 
Previously I introduced a calculus for propositional logic, fixing its meaning according to what C.S.&nbsp;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 <math>X^\circ = [u, v].</math>  In order to provide a bridge between propositions and quantifications it serves to define a set of qualifiers <math>\ell_{ij} : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}</math> that have the following characters:
+
Let us return to the 2-dimensional case <math>X^\Box = [u, v].\!</math>  In order to provide a bridge between propositions and quantifications it serves to define a set of qualifiers <math>\ell_{ij} : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}\!</math> that have the following characters:
  
 
<center><math>\begin{array}{llllll}
 
<center><math>\begin{array}{llllll}
Line 1,338: Line 1,359:
 
\Upsilon_{u v\ \Rightarrow f}    & =
 
\Upsilon_{u v\ \Rightarrow f}    & =
 
f\ \operatorname{likes}\ u v    \\
 
f\ \operatorname{likes}\ u v    \\
\end{array}</math></center>
+
\end{array}\!</math></center>
  
Intuitively, the <math>\ell_{ij}\!</math> 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 <math>X^\circ = [u, v],</math> and so they mediate a subtext <math>[\ell_{00}, \ell_{01}, \ell_{10}, \ell_{11}]\!</math> that takes place within the higher order universe of discourse <math>X^{\circ 2} = [X^\circ] = [[u, v]].\!</math>  Figure&nbsp;6 summarizes the action of the <math>\ell_{ij}\!</math> operators on the <math>f_i\!</math> within <math>X^{\circ 2}.\!</math>
+
Intuitively, the <math>\ell_{ij}\!</math> 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 <math>X^\Box = [u, v],\!</math> and so they mediate a subtext <math>[\ell_{00}, \ell_{01}, \ell_{10}, \ell_{11}]\!</math> that takes place within the higher order universe of discourse <math>X^{\Box\,2} = [X^\Box] = [[u, v]].\!</math>  Figure&nbsp;6 summarizes the action of the <math>\ell_{ij}\!</math> operators on the <math>f_i\!</math> within <math>X^{\Box\,2}.\!</math>
  
<pre>
+
{| align="center" cellpadding="10" style="text-align:center"
o-----------------------------------------------------------o
+
| [[Image:Venn Diagram 4 Dimensions UV Cacti 8 Inch.png]]
|                                                          |
+
|-
|                            o                            |
+
| <math>\text{Figure 6.} ~~ \text{Higher Order Universe of Discourse} ~ \left[ \ell_{00}, \ell_{01}, \ell_{10}, \ell_{11} \right] \subseteq \left[\left[ u, v \right]\right]\!</math>
|                            / \                            |
+
|}
|                          /  \                          |
 
|                         /u  v\                          |
 
|                        / o---o \                        |
 
|                       o  \ /  o                        |
 
|                       / \  o  / \                      |
 
|                      /  \  |  /  \                      |
 
|                    /    \ @ /    \                    |
 
|                    / u  v \ / u  v \                    |
 
|                  o  o---o  o  o---o  o                  |
 
|                 / \  \    / \    /  / \                  |
 
|                /  \  @  /  \  @  /  \                |
 
|                /    \  /    \  /    \                |
 
|              /  v  \ /      \ /  v  \              |
 
|              o    @    o    @    o    o    o              |
 
|            / \      / \      / \  |  / \            |
 
|            /  \    /  \    /  \  @  /  \            |
 
|          /    \  /u  v\  /    \  /    \          |
 
|          /  u v  \ / o  o \ /  u v  \ / u  v \          |
 
|        o    @    o  \ /  o    o    o  o  o  o        |
 
|        |\      / \  o  / \  |  / \  \ /  /|        |
 
|        | \    /  \  |  /  \  @  /  \  @  / |        |
 
|        |  \  /    \ @ /    \  /    \  /  |        |
 
|        |  \ /  u  \ / u  v \ /  u  \ /  |        |
 
|        |    o    @    o  o---o  o    o    o    |        |
 
|        |    |\      / \  \ /  / \  |  /|    |        |
 
|        |    | \    /  \  @  /  \  @  / |    |        |
 
|        |    |  \  /    \  /    \  /  |    |        |
 
|        |L_11|  \ /  o v \ / u o  \ /  |L_00|        |
 
|        o---------o    |    o    |    o---------o        |
 
|              |    \ u @  / \  @ v /    |              |
 
|              |      \    /  \    /      |              |
 
|              |      \  /    \  /      |              |
 
|              |L_10    \ /  o  \ /    L_01|              |
 
|              o---------o    |    o---------o              |
 
|                        \  @  /                        |
 
|                          \    /                          |
 
|                          \  /                          |
 
|                            \ /                            |
 
|                            o                            |
 
|                                                          |
 
o-----------------------------------------------------------o
 
Figure 6. Higher Order Universe of Discourse [L_ij] c [[u, v]]
 
</pre>
 
  
 
===Application of Higher Order Propositions to Quantification Theory===
 
===Application of Higher Order Propositions to Quantification Theory===
Line 1,395: Line 1,373:
 
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.
 
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 <math>f : \mathbb{B}^k \to \mathbb{E},</math> where <math>\mathbb{E} = \{ -e, +e \} = \{ \operatorname{empty}, \operatorname{exist} \}</math> 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.
+
It's hard to tell if it makes any difference from a purely formal point of view, but it serves intuition to devise a slightly different interpretation for the two-valued space that we use as the target of our basic indicator functions.  Therefore, let us declare the type of ''existential-valued functions'' <math>f : \mathbb{B}^k \to \mathbb{E},\!</math> where <math>\mathbb{E} = \{ -e, +e \} = \{ \operatorname{empty}, \operatorname{exist} \}\!</math> is a pair of values that indicate whether or not anything exists in the cells of the underlying universe of discourse.  As usual, let's not be too fussy about the coding of these functions, reverting to binary codes whenever the intended interpretation is clear enough.
 +
 
 +
With these qualifications in mind we note the following correspondences between classical quantifications and higher order indicator functions:
  
With this interpretation in mind we note the following correspondences between classical quantifications and higher order indicator functions:
+
<br>
  
{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; width:96%"
+
{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|+ '''Table 7. Syllogistic Premisses as Higher Order Indicator Functions'''
+
|+ style="height:30px" |
 +
<math>\text{Table 7.} ~~ \text{Syllogistic Premisses as Higher Order Indicator Functions}\!</math>
 
|
 
|
 
<math>\begin{array}{clcl}
 
<math>\begin{array}{clcl}
Line 1,419: Line 1,400:
 
\mathrm{Some}\ u\ \mathrm{is}\ (v)  &
 
\mathrm{Some}\ u\ \mathrm{is}\ (v)  &
 
\mathrm{Indicator~of}\ u (v) = 1    \\
 
\mathrm{Indicator~of}\ u (v) = 1    \\
\end{array}</math>
+
\end{array}\!</math>
|}<br>
+
|}
 +
 
 +
<br>
  
 
The following Tables develop these ideas in more detail.
 
The following Tables develop these ideas in more detail.
 +
 +
<br>
  
 
{| align="center" border="1" cellpadding="2" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="2" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|+ '''Table 8. Simple Qualifiers of Propositions (Version 1)'''
+
|+ style="height:30px" |
 +
<math>\text{Table 8.} ~~ \text{Simple Qualifiers of Propositions (Version 1)}\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
| align="right" | <math>u:</math><br><math>v:</math>
+
| align="right" | <math>u\colon\!</math><br><math>v\colon\!</math>
 
| 1100<br>1010
 
| 1100<br>1010
 
| <math>f\!</math>
 
| <math>f\!</math>
| <math>(\ell_{11})</math><br><math>\text{No } u </math><br><math>\text{is } v </math>
+
| <math>(\ell_{11})\!</math><br><math>\text{No}~ u \!</math><br><math>\text{is}~ v \!</math>
| <math>(\ell_{10})</math><br><math>\text{No } u </math><br><math>\text{is }(v)</math>
+
| <math>(\ell_{10})\!</math><br><math>\text{No}~ u \!</math><br><math>\text{is}~(v)\!</math>
| <math>(\ell_{01})</math><br><math>\text{No }(u)</math><br><math>\text{is } v </math>
+
| <math>(\ell_{01})\!</math><br><math>\text{No}~(u)\!</math><br><math>\text{is}~ v \!</math>
| <math>(\ell_{00})</math><br><math>\text{No }(u)</math><br><math>\text{is }(v)</math>
+
| <math>(\ell_{00})\!</math><br><math>\text{No}~(u)\!</math><br><math>\text{is}~(v)\!</math>
| <math> \ell_{00} </math><br><math>\text{Some }(u)</math><br><math>\text{is }(v)</math>
+
| <math> \ell_{00} \!</math><br><math>\text{Some}~(u)\!</math><br><math>\text{is}~(v)\!</math>
| <math> \ell_{01} </math><br><math>\text{Some }(u)</math><br><math>\text{is } v </math>
+
| <math> \ell_{01} \!</math><br><math>\text{Some}~(u)\!</math><br><math>\text{is}~ v \!</math>
| <math> \ell_{10} </math><br><math>\text{Some } u </math><br><math>\text{is }(v)</math>
+
| <math> \ell_{10}~\!</math><br><math>\text{Some}~ u \!</math><br><math>\text{is}~(v)\!</math>
| <math> \ell_{11} </math><br><math>\text{Some } u </math><br><math>\text{is } v </math>
+
| <math> \ell_{11} \!</math><br><math>\text{Some}~ u \!</math><br><math>\text{is}~ v \!</math>
 
|-
 
|-
| <math>f_0</math>
+
| <math>f_0\!</math>
 
| 0000
 
| 0000
| <math>(~)</math>
+
| <math>(~)\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 1,451: Line 1,437:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_1</math>
+
| <math>f_1\!</math>
 
| 0001
 
| 0001
 
| <math>(u)(v)\!</math>
 
| <math>(u)(v)\!</math>
Line 1,463: Line 1,449:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_2</math>
+
| <math>f_2\!</math>
 
| 0010
 
| 0010
 
| <math>(u) v\!</math>
 
| <math>(u) v\!</math>
Line 1,475: Line 1,461:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_3</math>
+
| <math>f_3\!</math>
 
| 0011
 
| 0011
| <math>(u)\!</math>
+
| <math>(u)~\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 1,487: Line 1,473:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_4</math>
+
| <math>f_4\!</math>
 
| 0100
 
| 0100
 
| <math>u (v)\!</math>
 
| <math>u (v)\!</math>
Line 1,499: Line 1,485:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_5</math>
+
| <math>f_5\!</math>
 
| 0101
 
| 0101
 
| <math>(v)\!</math>
 
| <math>(v)\!</math>
Line 1,511: Line 1,497:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_6</math>
+
| <math>f_6\!</math>
 
| 0110
 
| 0110
 
| <math>(u, v)\!</math>
 
| <math>(u, v)\!</math>
Line 1,523: Line 1,509:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_7</math>
+
| <math>f_7\!</math>
 
| 0111
 
| 0111
 
| <math>(u v)\!</math>
 
| <math>(u v)\!</math>
Line 1,535: Line 1,521:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_8</math>
+
| <math>f_8\!</math>
 
| 1000
 
| 1000
 
| <math>u v\!</math>
 
| <math>u v\!</math>
Line 1,547: Line 1,533:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_9</math>
+
| <math>f_9\!</math>
 
| 1001
 
| 1001
 
| <math>((u, v))\!</math>
 
| <math>((u, v))\!</math>
Line 1,559: Line 1,545:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{10}</math>
+
| <math>f_{10}\!</math>
 
| 1010
 
| 1010
 
| <math>v\!</math>
 
| <math>v\!</math>
Line 1,571: Line 1,557:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{11}</math>
+
| <math>f_{11}\!</math>
 
| 1011
 
| 1011
 
| <math>(u (v))\!</math>
 
| <math>(u (v))\!</math>
Line 1,583: Line 1,569:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{12}</math>
+
| <math>f_{12}\!</math>
 
| 1100
 
| 1100
 
| <math>u\!</math>
 
| <math>u\!</math>
Line 1,595: Line 1,581:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{13}</math>
+
| <math>f_{13}\!</math>
 
| 1101
 
| 1101
 
| <math>((u) v)\!</math>
 
| <math>((u) v)\!</math>
Line 1,607: Line 1,593:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{14}</math>
+
| <math>f_{14}\!</math>
 
| 1110
 
| 1110
| <math>((u)(v))\!</math>
+
| <math>((u)(v))~\!</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
Line 1,619: Line 1,605:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{15}</math>
+
| <math>f_{15}\!</math>
 
| 1111
 
| 1111
| <math>((~))</math>
+
| <math>((~))\!</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
Line 1,630: Line 1,616:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
|}<br>
+
|}
 +
 
 +
<br>
  
 
{| align="center" border="1" cellpadding="2" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="2" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|+ '''Table 9. Simple Qualifiers of Propositions (Version 2)'''
+
|+ style="height:30px" |
 +
<math>\text{Table 9.} ~~ \text{Simple Qualifiers of Propositions (Version 2)}\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
| align="right" | <math>u:</math><br><math>v:</math>
+
| align="right" | <math>u\colon\!</math><br><math>v\colon\!</math>
 
| 1100<br>1010
 
| 1100<br>1010
 
| <math>f\!</math>
 
| <math>f\!</math>
| <math>(\ell_{11})</math><br><math>\text{No } u </math><br><math>\text{is } v </math>
+
| <math>(\ell_{11})\!</math><br><math>\text{No } u \!</math><br><math>\text{is } v \!</math>
| <math>(\ell_{10})</math><br><math>\text{No } u </math><br><math>\text{is }(v)</math>
+
| <math>(\ell_{10})\!</math><br><math>\text{No } u \!</math><br><math>\text{is }(v)\!</math>
| <math>(\ell_{01})</math><br><math>\text{No }(u)</math><br><math>\text{is } v </math>
+
| <math>(\ell_{01})\!</math><br><math>\text{No }(u)\!</math><br><math>\text{is } v \!</math>
| <math>(\ell_{00})</math><br><math>\text{No }(u)</math><br><math>\text{is }(v)</math>
+
| <math>(\ell_{00})\!</math><br><math>\text{No }(u)\!</math><br><math>\text{is }(v)\!</math>
| <math> \ell_{00} </math><br><math>\text{Some }(u)</math><br><math>\text{is }(v)</math>
+
| <math> \ell_{00} \!</math><br><math>\text{Some }(u)\!</math><br><math>\text{is }(v)\!</math>
| <math> \ell_{01} </math><br><math>\text{Some }(u)</math><br><math>\text{is } v </math>
+
| <math> \ell_{01} \!</math><br><math>\text{Some }(u)\!</math><br><math>\text{is } v \!</math>
| <math> \ell_{10} </math><br><math>\text{Some } u </math><br><math>\text{is }(v)</math>
+
| <math> \ell_{10}~\!</math><br><math>\text{Some } u \!</math><br><math>\text{is }(v)\!</math>
| <math> \ell_{11} </math><br><math>\text{Some } u </math><br><math>\text{is } v </math>
+
| <math> \ell_{11} \!</math><br><math>\text{Some } u \!</math><br><math>\text{is } v \!</math>
 
|-
 
|-
| <math>f_0</math>
+
| <math>f_0\!</math>
 
| 0000
 
| 0000
| <math>(~)</math>
+
| <math>(~)\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 1,659: Line 1,648:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_1</math>
+
| <math>f_1\!</math>
 
| 0001
 
| 0001
 
| <math>(u)(v)\!</math>
 
| <math>(u)(v)\!</math>
Line 1,671: Line 1,660:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_2</math>
+
| <math>f_2\!</math>
 
| 0010
 
| 0010
 
| <math>(u) v\!</math>
 
| <math>(u) v\!</math>
Line 1,683: Line 1,672:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_4</math>
+
| <math>f_4\!</math>
 
| 0100
 
| 0100
 
| <math>u (v)\!</math>
 
| <math>u (v)\!</math>
Line 1,695: Line 1,684:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_8</math>
+
| <math>f_8\!</math>
 
| 1000
 
| 1000
 
| <math>u v\!</math>
 
| <math>u v\!</math>
Line 1,707: Line 1,696:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_3</math>
+
| <math>f_3\!</math>
 
| 0011
 
| 0011
| <math>(u)\!</math>
+
| <math>(u)~\!</math>
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
Line 1,719: Line 1,708:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{12}</math>
+
| <math>f_{12}\!</math>
 
| 1100
 
| 1100
 
| <math>u\!</math>
 
| <math>u\!</math>
Line 1,731: Line 1,720:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_6</math>
+
| <math>f_6\!</math>
 
| 0110
 
| 0110
 
| <math>(u, v)\!</math>
 
| <math>(u, v)\!</math>
Line 1,743: Line 1,732:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_9</math>
+
| <math>f_9\!</math>
 
| 1001
 
| 1001
 
| <math>((u, v))\!</math>
 
| <math>((u, v))\!</math>
Line 1,755: Line 1,744:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_5</math>
+
| <math>f_5\!</math>
 
| 0101
 
| 0101
 
| <math>(v)\!</math>
 
| <math>(v)\!</math>
Line 1,767: Line 1,756:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{10}</math>
+
| <math>f_{10}\!</math>
 
| 1010
 
| 1010
 
| <math>v\!</math>
 
| <math>v\!</math>
Line 1,779: Line 1,768:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_7</math>
+
| <math>f_7\!</math>
 
| 0111
 
| 0111
 
| <math>(u v)\!</math>
 
| <math>(u v)\!</math>
Line 1,791: Line 1,780:
 
| style="background:white; color:black" | 0
 
| style="background:white; color:black" | 0
 
|-
 
|-
| <math>f_{11}</math>
+
| <math>f_{11}\!</math>
 
| 1011
 
| 1011
 
| <math>(u (v))\!</math>
 
| <math>(u (v))\!</math>
Line 1,803: Line 1,792:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{13}</math>
+
| <math>f_{13}\!</math>
 
| 1101
 
| 1101
 
| <math>((u) v)\!</math>
 
| <math>((u) v)\!</math>
Line 1,815: Line 1,804:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{14}</math>
+
| <math>f_{14}\!</math>
 
| 1110
 
| 1110
| <math>((u)(v))\!</math>
+
| <math>((u)(v))~\!</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
Line 1,827: Line 1,816:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
|-
 
|-
| <math>f_{15}</math>
+
| <math>f_{15}\!</math>
 
| 1111
 
| 1111
| <math>((~))</math>
+
| <math>((~))\!</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
Line 1,838: Line 1,827:
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
 
| style="background:black; color:white" | 1
|}<br>
+
|}
 +
 
 +
<br>
  
 
{| align="center" border="1" cellpadding="2" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
 
{| align="center" border="1" cellpadding="2" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
|+ '''Table 10. Relation of Quantifiers to Higher Order Propositions'''
+
|+ style="height:30px" |
 +
<math>\text{Table 10.} ~~ \text{Relation of Quantifiers to Higher Order Propositions}\!</math>
 
|- style="background:ghostwhite"
 
|- style="background:ghostwhite"
| <math>\text{Mnemonic}</math>
+
| <math>\text{Mnemonic}\!</math>
| <math>\text{Category}</math>
+
| <math>\text{Category}\!</math>
| <math>\text{Classical Form}</math>
+
| <math>\text{Classical Form}\!</math>
| <math>\text{Alternate Form}</math>
+
| <math>\text{Alternate Form}\!</math>
| <math>\text{Symmetric Form}</math>
+
| <math>\text{Symmetric Form}\!</math>
| <math>\text{Operator}</math>
+
| <math>\text{Operator}\!</math>
 
|-
 
|-
| <math>\text{E}\!</math><br><math>\text{Exclusive}</math>
+
| <math>\text{E}\!</math><br><math>\text{Exclusive}\!</math>
| <math>\text{Universal}</math><br><math>\text{Negative}</math>
+
| <math>\text{Universal}\!</math><br><math>\text{Negative}\!</math>
| <math>\text{All}\ u\ \text{is}\ (v)</math>
+
| <math>\text{All}\ u\ \text{is}\ (v)\!</math>
 
| &nbsp;
 
| &nbsp;
| <math>\text{No}\  u\ \text{is}\  v </math>
+
| <math>\text{No}\  u\ \text{is}\  v \!</math>
| <math>(\ell_{11})</math>
+
| <math>(\ell_{11})\!</math>
 
|-
 
|-
| <math>\text{A}\!</math><br><math>\text{Absolute}</math>
+
| <math>\text{A}\!</math><br><math>\text{Absolute}~\!</math>
| <math>\text{Universal}</math><br><math>\text{Affirmative}</math>
+
| <math>\text{Universal}\!</math><br><math>\text{Affirmative}\!</math>
| <math>\text{All}\ u\ \text{is}\  v </math>
+
| <math>\text{All}\ u\ \text{is}\  v \!</math>
 
| &nbsp;
 
| &nbsp;
| <math>\text{No}\  u\ \text{is}\ (v)</math>
+
| <math>\text{No}\  u\ \text{is}\ (v)\!</math>
| <math>(\ell_{10})</math>
+
| <math>(\ell_{10})\!</math>
 
|-
 
|-
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
| <math>\text{All}\ v\  \text{is}\  u </math>
+
| <math>\text{All}\ v\  \text{is}\  u \!</math>
| <math>\text{No}\  v\  \text{is}\ (u)</math>
+
| <math>\text{No}\  v\  \text{is}\ (u)\!</math>
| <math>\text{No}\ (u)\ \text{is}\  v </math>
+
| <math>\text{No}\ (u)\ \text{is}\  v \!</math>
| <math>(\ell_{01})</math>
+
| <math>(\ell_{01})\!</math>
 
|-
 
|-
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
| <math>\text{All}\ (v)\ \text{is}\  u </math>
+
| <math>\text{All}\ (v)\ \text{is}\  u \!</math>
| <math>\text{No}\  (v)\ \text{is}\ (u)</math>
+
| <math>\text{No}\  (v)\ \text{is}\ (u)\!</math>
| <math>\text{No}\  (u)\ \text{is}\ (v)</math>
+
| <math>\text{No}\  (u)\ \text{is}\ (v)\!</math>
| <math>(\ell_{00})</math>
+
| <math>(\ell_{00})\!</math>
 
|-
 
|-
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
| <math>\text{Some}\ (u)\ \text{is}\ (v)</math>
+
| <math>\text{Some}\ (u)\ \text{is}\ (v)\!</math>
 
| &nbsp;
 
| &nbsp;
| <math>\text{Some}\ (u)\ \text{is}\ (v)</math>
+
| <math>\text{Some}\ (u)\ \text{is}\ (v)\!</math>
 
| <math>\ell_{00}\!</math>
 
| <math>\ell_{00}\!</math>
 
|-
 
|-
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
 
| &nbsp;
| <math>\text{Some}\ (u)\ \text{is}\ v</math>
+
| <math>\text{Some}\ (u)\ \text{is}\ v\!</math>
 
| &nbsp;
 
| &nbsp;
| <math>\text{Some}\ (u)\ \text{is}\ v</math>
+
| <math>\text{Some}\ (u)\ \text{is}\ v\!</math>
 
| <math>\ell_{01}\!</math>
 
| <math>\ell_{01}\!</math>
 
|-
 
|-
| <math>\text{O}\!</math><br><math>\text{Obtrusive}</math>
+
| <math>\text{O}\!</math><br><math>\text{Obtrusive}\!</math>
| <math>\text{Particular}</math><br><math>\text{Negative}</math>
+
| <math>\text{Particular}\!</math><br><math>\text{Negative}\!</math>
| <math>\text{Some}\ u\ \text{is}\ (v)</math>
+
| <math>\text{Some}\ u\ \text{is}\ (v)\!</math>
 
| &nbsp;
 
| &nbsp;
| <math>\text{Some}\ u\ \text{is}\ (v)</math>
+
| <math>\text{Some}\ u\ \text{is}\ (v)\!</math>
| <math>\ell_{10}\!</math>
+
| <math>\ell_{10}~\!</math>
 
|-
 
|-
| <math>\text{I}\!</math><br><math>\text{Indefinite}</math>
+
| <math>\text{I}\!</math><br><math>\text{Indefinite}\!</math>
| <math>\text{Particular}</math><br><math>\text{Affirmative}</math>
+
| <math>\text{Particular}\!</math><br><math>\text{Affirmative}\!</math>
| <math>\text{Some}\ u\ \text{is}\ v</math>
+
| <math>\text{Some}\ u\ \text{is}\ v\!</math>
 
| &nbsp;
 
| &nbsp;
| <math>\text{Some}\ u\ \text{is}\ v</math>
+
| <math>\text{Some}\ u\ \text{is}\ v\!</math>
 
| <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==
  
<math>\ldots</math>
+
* Quine, W.V. (1969/1981), "On the Limits of Decision", ''Akten des XIV. Internationalen Kongresses für Philosophie'', vol. 3 (1969).  Reprinted, pp. 156&ndash;163 in Quine (ed., 1981), ''Theories and Things'', Harvard University Press, Cambridge, MA.
  
 
==Document History==
 
==Document History==
  
'''Note.'''  The above material is excerpted from a project report on [[Charles Sanders Peirce]]'s conceptions of inquiry and analogy.  Online formatting of the original document and continuation of the initial project are currently in progress under the title ''[[Directory:Jon_Awbrey/Papers/Functional_Logic_:_Inquiry_and_Analogy|Functional Logic : Inquiry and Analogy]]''.
+
'''Note.'''  The above material is excerpted from a project report on [[Charles Sanders Peirce]]'s conceptions of inquiry and analogy.  Online formatting of the original document and continuation of the initial project are currently in progress under the title ''[[Functional Logic : Inquiry and Analogy]]''.
  
 
===Inquiry and Analogy===
 
===Inquiry and Analogy===
Line 1,960: Line 1,990:
 
# http://stderr.org/pipermail/inquiry/2004-March/001260.html
 
# http://stderr.org/pipermail/inquiry/2004-March/001260.html
 
# http://stderr.org/pipermail/inquiry/2004-March/001261.html
 
# http://stderr.org/pipermail/inquiry/2004-March/001261.html
 +
 +
====NKS Forum====
 +
 +
* http://forum.wolframscience.com/showthread.php?threadid=254
 +
* http://forum.wolframscience.com/showthread.php?threadid=598
 +
# http://forum.wolframscience.com/showthread.php?postid=1957#post1957
 +
# http://forum.wolframscience.com/showthread.php?postid=1960#post1960
 +
# http://forum.wolframscience.com/showthread.php?postid=1961#post1961
 +
# http://forum.wolframscience.com/showthread.php?postid=1962#post1962
 +
# http://forum.wolframscience.com/showthread.php?postid=1964#post1964
 +
# http://forum.wolframscience.com/showthread.php?postid=1966#post1966
 +
# http://forum.wolframscience.com/showthread.php?postid=1968#post1968
  
 
[[Category:Adaptive Systems]]
 
[[Category:Adaptive Systems]]

Latest revision as of 02:22, 5 July 2013

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 \(\forall_{x \in X} f(x)\!\) and \(\exists_{x \in X} f(x)\!\) 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, in particular, those that stem from the propositions on 1 and 2 variables.

Note on notation. The discussion that follows uses minimal negation operations, expressed as bracketed tuples of the form \(\texttt{(} e_1 \texttt{,} \ldots \texttt{,} e_k \texttt{)},\!\) and logical conjunctions, expressed as concatenated tuples of the form \(e_1 ~\ldots~ e_k,\!\) as the sole expression-forming operations of a calculus for boolean-valued functions or "propositions". The expressions of this calculus parse into data structures whose underlying graphs are called cacti by graph theorists. Hence the name cactus language for this dialect of propositional calculus.

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 \to \mathbb{B},\!\) then the next higher order of propositions consists of maps of the type \(m : (X \to \mathbb{B}) \to \mathbb{B}.\!\)

For example, consider the case where \(X = \mathbb{B}.\!\) Then there are exactly four propositions \(f : \mathbb{B} \to \mathbb{B},\!\) and exactly sixteen higher order propositions that are based on this set, all bearing the type \(m : (\mathbb{B} \to \mathbb{B}) \to \mathbb{B}.\!\)

Table 1 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 : \mathbb{B} \to \mathbb{B},\!\) turned on its side from the way that one is most likely accustomed to see truth tables, with the row leaders in Column 1 displaying the names of the functions \(f_i,\!\) for \(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 corresponding column head. Column 3 displays one of the more usual expressions for the proposition in question. The last sixteen columns are topped by a collection of conventional names for the higher order propositions, also known as the measures \(m_j,\!\) for \(j\!\) = 0 to 15, where the entries in the body of the Table record the values that each \(m_j\!\) assigns to each \(f_i.\!\)


\(\text{Table 1.} ~~ \text{Higher Order Propositions} ~~ (n = 1)\!\)
\(x:\!\) 1 0 \(f\!\) \(m_0\!\) \(m_1\!\) \(m_2\!\) \(m_3\!\) \(m_4\!\) \(m_5\!\) \(m_6\!\) \(m_7\!\) \(m_8\!\) \(m_9\!\) \(m_{10}\!\) \(m_{11}\!\) \(m_{12}\!\) \(m_{13}\!\) \(m_{14}\!\) \(m_{15}\!\)
\(f_0\!\) 0 0 \(0\!\) 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
\(f_1\!\) 0 1 \((x)\!\) 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1
\(f_2\!\) 1 0 \(x\!\) 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1
\(f_3\!\) 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 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.


\(\text{Table 2.} ~~ \text{Interpretive Categories for Higher Order Propositions} ~~ (n = 1)\!\)
Measure Happening Exactness Existence Linearity Uniformity Information
\(m_0\!\) Nothing happens          
\(m_1\!\)   Just false Nothing exists      
\(m_2\!\)   Just not \(x\!\)        
\(m_3\!\)     Nothing is \(x\!\)      
\(m_4\!\)   Just \(x\!\)        
\(m_5\!\)     Everything is \(x\!\) \(f\!\) is linear    
\(m_6\!\)         \(f\!\) is not uniform \(f\!\) is informed
\(m_7\!\)   Not just true        
\(m_8\!\)   Just true        
\(m_9\!\)         \(f\!\) is uniform \(f\!\) is not informed
\(m_{10}\!\)     Something is not \(x\!\) \(f\!\) is not linear    
\(m_{11}\!\)   Not just \(x\!\)        
\(m_{12}\!\)     Something is \(x\!\)      
\(m_{13}\!\)   Not just not \(x\!\)        
\(m_{14}\!\)   Not just false Something exists      
\(m_{15}\!\) 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^\Box = [\mathcal{X}] = [x_1, x_2] = [u, v],\!\) based on two logical features or boolean variables \(u\!\) and \(v.\!\)

The universe of discourse \(X^\Box\!\) consists of two parts, a set of points and a set of propositions.

The points of \(X^\Box\!\) form the space:

\(X \quad = \quad \langle \mathcal{X} \rangle \quad = \quad \langle u, v \rangle \quad = \quad \{ (u, v) \} \quad \cong \quad \mathbb{B}^2.\!\)

Each point in \(X\!\) may be indicated by means of a singular proposition, that is, a proposition that describes it uniquely. This form of representation leads to the following enumeration of points, presented in two different styles of typography that are used in this text:

\(X\!\) \(=\!\) \(\{\!\) (u)(v),  (u)v,  u(v),  uv \(\}\!\) \(\cong\!\) \(\mathbb{B}^2,\!\)
\(X\!\) \(=\!\) \(\{\ \underline{(u)(v)},\ \underline{(u)v},\ \underline{u(v)},\ \underline{uv}\ \}\!\) \(\cong\!\) \(\mathbb{B}^2.\!\)

Each point in \(X\!\) may also be described by means of its coordinates, that is, by the ordered pair of values in \(\mathbb{B}\!\) that the coordinate propositions \(u\!\) and \(v\!\) take on that point. This form of representation leads to the following enumeration of points:

\(X\!\) \(=\!\) \(\{\ (0, 0),\ (0, 1),\ (1, 0),\ (1, 1)\ \}\!\) \(\cong\!\) \(\mathbb{B}^2.\!\)

The propositions of \(X^\Box\!\) form the space:

\(X^\uparrow \quad = \quad (X \to \mathbb{B}) \quad = \quad \{ f : X \to \mathbb{B} \} \quad \cong \quad (\mathbb{B}^2 \to \mathbb{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^\Box\!\) is \(X^{\Box\,2} = [X^\Box] = [[u, v]],\!\) which may be developed in the following way. The propositions of \(X^\Box\!\) become the points of \(X^{\Box\,2},\!\) and the mappings of the type \(m : (X \to \mathbb{B}) \to \mathbb{B}\!\) become the propositions of \(X^{\Box\,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 : (\mathbb{B}^2 \to \mathbb{B})^k \to \mathbb{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 \([u, v]\!\) may be regarded as a gallery of sixteen venn diagrams, while the measures \(m : (X \to \mathbb{B}) \to \mathbb{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_j^{-1}(1)\!\) that \(m_j\!\) likes and the pictures \(m_j^{-1}(0)\!\) that \(m_j\!\) dislikes.

There are \(2^{16} = 65536\!\) measures of the type \(m : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{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_j\!\) shows the values of the measure \(m_j\!\) on each of the propositions \(f_i : \mathbb{B}^2 \to \mathbb{B},\!\) for \(i\!\) = 0 to 15, 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_j\!\) is the decimal equivalent of the bit string that is associated with \(m_j\!\)'s functional values, which can be obtained in turn by reading the \(j^\mathrm{th}\!\) column of binary digits in the Table as the corresponding range of boolean values, taking them up in the order from bottom to top.


\(\text{Table 3.} ~~ \text{Higher Order Propositions} ~~ (n = 2)\!\)
\(u\!:\)
\(v\!:\)
1100
1010
\(f\!\) \(m_0\!\) \(m_1\!\) \(m_2\!\) \(m_3\!\) \(m_4\!\) \(m_5\!\) \(m_6\!\) \(m_7\!\) \(m_8\!\) \(m_9\!\) \(m_{10}\!\) \(m_{11}\!\) \(m_{12}\!\) \(m_{13}\!\) \(m_{14}\!\) \(m_{15}\!\) \(m_{16}\!\) \(m_{17}\!\) \(m_{18}\!\) \(m_{19}\!\) \(m_{20}\!\) \(m_{21}\!\) \(m_{22}\!\) \(m_{23}\!\)
\(f_0\!\) 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_1\!\) 0001 \((u)(v)\!\) 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1
\(f_2\!\) 0010 \((u) v\!\) 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1
\(f_3\!\) 0011 \((u)~\!\) 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0
\(f_4\!\) 0100 \(u (v)\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1
\(f_5\!\) 0101 \((v)\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_6\!\) 0110 \((u, v)\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_7\!\) 0111 \((u v)\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_8\!\) 1000 \(u v\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_9\!\) 1001 \(((u, v))\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_{10}\!\) 1010 \(v\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_{11}\!\) 1011 \((u (v))\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_{12}\!\) 1100 \(u\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_{13}\!\) 1101 \(((u) v)\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_{14}\!\) 1110 \(((u)(v))~\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_{15}\!\) 1111 \(((~))\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0


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, \(\Upsilon_1 : (\langle u, v \rangle \to \mathbb{B}) \to \mathbb{B}\!\) and \(\Upsilon : (\langle u, v \rangle \to \mathbb{B})^2 \to \mathbb{B},\!\) 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.

Given an ordered pair of propositions \(e, f : \langle u, v \rangle \to \mathbb{B}\!\) as arguments, the relative operator reports the value 1 if the first implies the second, otherwise 0.

\(\Upsilon (e, f) = 1\!\) \(\operatorname{if~and~only~if}\!\) \(e \Rightarrow f.\!\)

Expressing it another way, we may also write:

\(\Upsilon (e, f) = 1\!\) \(\Leftrightarrow\!\) \(\underline{(e (f))} = \underline{1}.\!\)

In writing this, however, it is important to notice that the 1's appearing on the left and right have different meanings. Filling in the details, we have:

\(\Upsilon (e, f) = 1 \in \mathbb{B}\!\) \(\Leftrightarrow\!\) \(\underline{(e (f))} = 1 : \langle u, v \rangle \to \mathbb{B}.\!\)

Writing types as subscripts and using the fact that \(X = \langle u, v \rangle,\!\) it is possible to express this a little more succinctly as follows:

\(\Upsilon (e, f) = 1_\mathbb{B}\!\) \(\Leftrightarrow\!\) \(\underline{(e (f))} = 1_{X \to \mathbb{B}}.\!\)

Finally, it is often convenient to write the first argument as a subscript, hence \(\Upsilon_e (f) = \Upsilon (e, f).\!\)

As a special application of this operator, we next define the absolute umpire operator, also called the umpire measure. This is a higher order proposition \(\Upsilon_1 : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}\!\) which is given by the relation \(\Upsilon_1 (f) = \Upsilon (1, f).\!\) Here, the subscript 1 on the left and the argument 1 on the right both refer to the constant proposition \(1 : \mathbb{B}^2 \to \mathbb{B}.\!\) In most contexts where \(\Upsilon_1\!\) is actually applied the subscript 1 is safely omitted, since the number of arguments indicates which type of operator is intended. Thus, we have the following identities and equivalents:

\(\Upsilon f = \Upsilon_1 (f) = 1 \in \mathbb{B}\!\) \(\Leftrightarrow\!\) \(\underline{(1~(f))} = \underline{1}\!\) \(\Leftrightarrow\!\) \(f = 1 : \mathbb{B}^2 \to \mathbb{B}.\!\)

The umpire measure is defined at the level of truth functions, but can also be understood in terms of its implied judgments at the syntactic level. Interpreted this way, \(\Upsilon_1\!\) recognizes theorems of the propositional calculus over \([u, v],\!\) giving a score of "1" to tautologies and a score of "0" to everything else, regarding all contingent statements as no better than falsehoods.

One remark in passing for those who might prefer an alternative definition. If we had originally taken \(\Upsilon\!\) to mean the absolute measure, then the relative version could have been defined as \(\Upsilon_e f = \Upsilon \underline{(e (f))}.\!\)

Measure for Measure

Define two families of measures:

\(\alpha_i, \beta_i : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}, i = 0 \ldots 15,\!\)

by means of the following formulas:

\(\alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f),\!\)
\(\beta_i f = \Upsilon (f, f_i) = \Upsilon (f \Rightarrow f_i).\!\)

The values of the sixteen \(\alpha_i\!\) on each of the sixteen boolean functions \(f : \mathbb{B}^2 \to \mathbb{B}\!\) are shown in Table 4. Expressed in terms of the implication ordering on the sixteen functions, \(\alpha_i f = 1\!\) says that \(f\!\) is above or identical to \(f_i\!\) in the implication lattice, that is, \(\ge f_i\!\) in the implication ordering.


\(\text{Table 4.} ~~ \text{Qualifiers of Implication Ordering:} ~~ \alpha_i f = \Upsilon (f_i, f) = \Upsilon (f_i \Rightarrow f)\!\)
\(u\colon\!\)
\(v\colon\!\)
1100
1010
\(f\!\) \(\alpha_0~\!\) \(\alpha_1\!\) \(\alpha_2\!\) \(\alpha_3\!\) \(\alpha_4\!\) \(\alpha_5\!\) \(\alpha_6\!\) \(\alpha_7\!\) \(\alpha_8\!\) \(\alpha_9\!\) \(\alpha_{10}\!\) \(\alpha_{11}\!\) \(\alpha_{12}\!\) \(\alpha_{13}~\!\) \(\alpha_{14}\!\) \(\alpha_{15}\!\)
\(f_0\!\) 0000 \((~)\!\) 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_1\!\) 0001 \((u)(v)\!\) 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_2\!\) 0010 \((u) v\!\) 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0
\(f_3\!\) 0011 \((u)~\!\) 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0
\(f_4\!\) 0100 \(u (v)\!\) 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0
\(f_5\!\) 0101 \((v)\!\) 1 1 0 0 1 1 0 0 0 0 0 0 0 0 0 0
\(f_6\!\) 0110 \((u, v)\!\) 1 0 1 0 1 0 1 0 0 0 0 0 0 0 0 0
\(f_7\!\) 0111 \((u v)\!\) 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0
\(f_8\!\) 1000 \(u v\!\) 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0
\(f_9\!\) 1001 \(((u, v))\!\) 1 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0
\(f_{10}\!\) 1010 \(v\!\) 1 0 1 0 0 0 0 0 1 0 1 0 0 0 0 0
\(f_{11}\!\) 1011 \((u (v))\!\) 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0
\(f_{12}\!\) 1100 \(u\!\) 1 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0
\(f_{13}\!\) 1101 \(((u) v)\!\) 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0
\(f_{14}\!\) 1110 \(((u)(v))~\!\) 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0
\(f_{15}\!\) 1111 \(((~))\!\) 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1


The values of the sixteen \(\beta_i\!\) on each of the sixteen boolean functions \({f : \mathbb{B}^2 \to \mathbb{B}}\!\) are shown in Table 5. Expressed in terms of the implication ordering on the sixteen functions, \({\beta_i f = 1}\!\) says that \(f\!\) is below or identical to \(f_i\!\) in the implication lattice, that is, \(\le f_i\!\) in the implication ordering.


\(\text{Table 5.} ~~ \text{Qualifiers of Implication Ordering:} ~~ \beta_i f = \Upsilon (f, f_i) = \Upsilon (f \Rightarrow f_i)\!\)
\(u\colon\!\)
\(v\colon\!\)
1100
1010
\(f\!\) \(\beta_0\!\) \(\beta_1\!\) \(\beta_2\!\) \(\beta_3\!\) \(\beta_4\!\) \(\beta_5\!\) \(\beta_6\!\) \(\beta_7\!\) \(\beta_8\!\) \(\beta_9\!\) \(\beta_{10}\!\) \(\beta_{11}\!\) \(\beta_{12}\!\) \(\beta_{13}\!\) \(\beta_{14}\!\) \(\beta_{15}\!\)
\(f_0\!\) 0000 \((~)\!\) 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
\(f_1\!\) 0001 \((u)(v)\!\) 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
\(f_2\!\) 0010 \((u) v\!\) 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1
\(f_3\!\) 0011 \((u)~\!\) 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 1
\(f_4\!\) 0100 \(u (v)\!\) 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1
\(f_5\!\) 0101 \((v)\!\) 0 0 0 0 0 1 0 1 0 0 0 0 0 1 0 1
\(f_6\!\) 0110 \((u, v)\!\) 0 0 0 0 0 0 1 1 0 0 0 0 0 0 1 1
\(f_7\!\) 0111 \((u v)\!\) 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1
\(f_8\!\) 1000 \(u v\!\) 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1
\(f_9\!\) 1001 \(((u, v))\!\) 0 0 0 0 0 0 0 0 0 1 0 1 0 1 0 1
\(f_{10}\!\) 1010 \(v\!\) 0 0 0 0 0 0 0 0 0 0 1 1 0 0 1 1
\(f_{11}\!\) 1011 \((u (v))\!\) 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1
\(f_{12}\!\) 1100 \(u\!\) 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1
\(f_{13}\!\) 1101 \(((u) v)\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1
\(f_{14}\!\) 1110 \(((u)(v))~\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1
\(f_{15}\!\) 1111 \(((~))\!\) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1


Applied to a given proposition \(f,\!\) the qualifiers \(\alpha_i\!\) and \(\beta_i\!\) tell whether \(f\!\) rests \(\operatorname{above}\ f_i\!\) or \(\operatorname{below}\ f_i,\!\) 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.

\(\begin{matrix} \alpha_0 f = 1 & \mathrm{iff} & f_0 \Rightarrow f & \mathrm{iff} & 0 \Rightarrow f. & \therefore & \alpha_0 f = 1 & \operatorname{for~all}\ f. \\ \alpha_{15} f = 1 & \mathrm{iff} & f_{15} \Rightarrow f & \mathrm{iff} & 1 \Rightarrow f. & \therefore & \alpha_{15} f = 1 & \mathrm{iff} f = 1. \\ \beta_0 f = 1 & \mathrm{iff} & f \Rightarrow f_0 & \mathrm{iff} & f \Rightarrow 0. & \therefore & \beta_0 f = 1 & \mathrm{iff} f = 0. \\ \beta_{15} f = 1 & \mathrm{iff} & f \Rightarrow f_{15} & \mathrm{iff} & f \Rightarrow 1. & \therefore & \beta_{15} f = 1 & \operatorname{for~all}\ f. \\ \end{matrix}\!\)


Thus, \(\alpha_0 = \beta_{15}\!\) is a totally indiscriminate measure, one that accepts all propositions \({f : \mathbb{B}^2 \to \mathbb{B}},\!\) whereas \(\alpha_{15}\!\) and \(\beta_0\!\) are measures that value the constant propositions \(1 : \mathbb{B}^2 \to \mathbb{B}\!\) and \(0 : \mathbb{B}^2 \to \mathbb{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:

\([| \alpha_i |]\!\) \(=\!\) \((\alpha_i)^{-1}(1),\!\)
\([| \beta_i |]\!\) \(=\!\) \((\beta_i)^{-1}(1),\!\)
\([| \Upsilon_p |]\!\) \(=\!\) \((\Upsilon_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^\Box = [u, v].\!\) In order to provide a bridge between propositions and quantifications it serves to define a set of qualifiers \(\ell_{ij} : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}\!\) that have the following characters:

\(\begin{array}{llllll} \ell_{00} f & = \ell_{(u)(v)} f & = \alpha_1 f & = \Upsilon_{(u)(v)} f & = \Upsilon_{(u)(v)\ \Rightarrow f} & = f\ \operatorname{likes}\ (u)(v) \\ \ell_{01} f & = \ell_{(u) v} f & = \alpha_2 f & = \Upsilon_{(u) v} f & = \Upsilon_{(u) v\ \Rightarrow f} & = f\ \operatorname{likes}\ (u) v \\ \ell_{10} f & = \ell_{u (v)} f & = \alpha_4 f & = \Upsilon_{u (v)} f & = \Upsilon_{u (v)\ \Rightarrow f} & = f\ \operatorname{likes}\ u (v) \\ \ell_{11} f & = \ell_{u v} f & = \alpha_8 f & = \Upsilon_{u v} f & = \Upsilon_{u v\ \Rightarrow f} & = f\ \operatorname{likes}\ u v \\ \end{array}\!\)

Intuitively, the \(\ell_{ij}\!\) 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^\Box = [u, v],\!\) and so they mediate a subtext \([\ell_{00}, \ell_{01}, \ell_{10}, \ell_{11}]\!\) that takes place within the higher order universe of discourse \(X^{\Box\,2} = [X^\Box] = [[u, v]].\!\) Figure 6 summarizes the action of the \(\ell_{ij}\!\) operators on the \(f_i\!\) within \(X^{\Box\,2}.\!\)

Venn Diagram 4 Dimensions UV Cacti 8 Inch.png
\(\text{Figure 6.} ~~ \text{Higher Order Universe of Discourse} ~ \left[ \ell_{00}, \ell_{01}, \ell_{10}, \ell_{11} \right] \subseteq \left[\left[ u, v \right]\right]\!\)

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.

It's hard to tell if it makes any difference from a purely formal point of view, but it serves intuition to devise a slightly different interpretation for the two-valued space that we use as the target of our basic indicator functions. Therefore, let us declare the type of existential-valued functions \(f : \mathbb{B}^k \to \mathbb{E},\!\) where \(\mathbb{E} = \{ -e, +e \} = \{ \operatorname{empty}, \operatorname{exist} \}\!\) is a pair of values that indicate whether or not anything exists in the cells of the underlying universe of discourse. As usual, let's not be too fussy about the coding of these functions, reverting to binary codes whenever the intended interpretation is clear enough.

With these qualifications in mind we note the following correspondences between classical quantifications and higher order indicator functions:


\(\text{Table 7.} ~~ \text{Syllogistic Premisses as Higher Order Indicator Functions}\!\)

\(\begin{array}{clcl} \mathrm{A} & \mathrm{Universal~Affirmative} & \mathrm{All}\ u\ \mathrm{is}\ v & \mathrm{Indicator~of}\ u (v) = 0 \\ \mathrm{E} & \mathrm{Universal~Negative} & \mathrm{All}\ u\ \mathrm{is}\ (v) & \mathrm{Indicator~of}\ u \cdot v = 0 \\ \mathrm{I} & \mathrm{Particular~Affirmative} & \mathrm{Some}\ u\ \mathrm{is}\ v & \mathrm{Indicator~of}\ u \cdot v = 1 \\ \mathrm{O} & \mathrm{Particular~Negative} & \mathrm{Some}\ u\ \mathrm{is}\ (v) & \mathrm{Indicator~of}\ u (v) = 1 \\ \end{array}\!\)


The following Tables develop these ideas in more detail.


\(\text{Table 8.} ~~ \text{Simple Qualifiers of Propositions (Version 1)}\!\)
\(u\colon\!\)
\(v\colon\!\)
1100
1010
\(f\!\) \((\ell_{11})\!\)
\(\text{No}~ u \!\)
\(\text{is}~ v \!\)
\((\ell_{10})\!\)
\(\text{No}~ u \!\)
\(\text{is}~(v)\!\)
\((\ell_{01})\!\)
\(\text{No}~(u)\!\)
\(\text{is}~ v \!\)
\((\ell_{00})\!\)
\(\text{No}~(u)\!\)
\(\text{is}~(v)\!\)
\( \ell_{00} \!\)
\(\text{Some}~(u)\!\)
\(\text{is}~(v)\!\)
\( \ell_{01} \!\)
\(\text{Some}~(u)\!\)
\(\text{is}~ v \!\)
\( \ell_{10}~\!\)
\(\text{Some}~ u \!\)
\(\text{is}~(v)\!\)
\( \ell_{11} \!\)
\(\text{Some}~ u \!\)
\(\text{is}~ v \!\)
\(f_0\!\) 0000 \((~)\!\) 1 1 1 1 0 0 0 0
\(f_1\!\) 0001 \((u)(v)\!\) 1 1 1 0 1 0 0 0
\(f_2\!\) 0010 \((u) v\!\) 1 1 0 1 0 1 0 0
\(f_3\!\) 0011 \((u)~\!\) 1 1 0 0 1 1 0 0
\(f_4\!\) 0100 \(u (v)\!\) 1 0 1 1 0 0 1 0
\(f_5\!\) 0101 \((v)\!\) 1 0 1 0 1 0 1 0
\(f_6\!\) 0110 \((u, v)\!\) 1 0 0 1 0 1 1 0
\(f_7\!\) 0111 \((u v)\!\) 1 0 0 0 1 1 1 0
\(f_8\!\) 1000 \(u v\!\) 0 1 1 1 0 0 0 1
\(f_9\!\) 1001 \(((u, v))\!\) 0 1 1 0 1 0 0 1
\(f_{10}\!\) 1010 \(v\!\) 0 1 0 1 0 1 0 1
\(f_{11}\!\) 1011 \((u (v))\!\) 0 1 0 0 1 1 0 1
\(f_{12}\!\) 1100 \(u\!\) 0 0 1 1 0 0 1 1
\(f_{13}\!\) 1101 \(((u) v)\!\) 0 0 1 0 1 0 1 1
\(f_{14}\!\) 1110 \(((u)(v))~\!\) 0 0 0 1 0 1 1 1
\(f_{15}\!\) 1111 \(((~))\!\) 0 0 0 0 1 1 1 1


\(\text{Table 9.} ~~ \text{Simple Qualifiers of Propositions (Version 2)}\!\)
\(u\colon\!\)
\(v\colon\!\)
1100
1010
\(f\!\) \((\ell_{11})\!\)
\(\text{No } u \!\)
\(\text{is } v \!\)
\((\ell_{10})\!\)
\(\text{No } u \!\)
\(\text{is }(v)\!\)
\((\ell_{01})\!\)
\(\text{No }(u)\!\)
\(\text{is } v \!\)
\((\ell_{00})\!\)
\(\text{No }(u)\!\)
\(\text{is }(v)\!\)
\( \ell_{00} \!\)
\(\text{Some }(u)\!\)
\(\text{is }(v)\!\)
\( \ell_{01} \!\)
\(\text{Some }(u)\!\)
\(\text{is } v \!\)
\( \ell_{10}~\!\)
\(\text{Some } u \!\)
\(\text{is }(v)\!\)
\( \ell_{11} \!\)
\(\text{Some } u \!\)
\(\text{is } v \!\)
\(f_0\!\) 0000 \((~)\!\) 1 1 1 1 0 0 0 0
\(f_1\!\) 0001 \((u)(v)\!\) 1 1 1 0 1 0 0 0
\(f_2\!\) 0010 \((u) v\!\) 1 1 0 1 0 1 0 0
\(f_4\!\) 0100 \(u (v)\!\) 1 0 1 1 0 0 1 0
\(f_8\!\) 1000 \(u v\!\) 0 1 1 1 0 0 0 1
\(f_3\!\) 0011 \((u)~\!\) 1 1 0 0 1 1 0 0
\(f_{12}\!\) 1100 \(u\!\) 0 0 1 1 0 0 1 1
\(f_6\!\) 0110 \((u, v)\!\) 1 0 0 1 0 1 1 0
\(f_9\!\) 1001 \(((u, v))\!\) 0 1 1 0 1 0 0 1
\(f_5\!\) 0101 \((v)\!\) 1 0 1 0 1 0 1 0
\(f_{10}\!\) 1010 \(v\!\) 0 1 0 1 0 1 0 1
\(f_7\!\) 0111 \((u v)\!\) 1 0 0 0 1 1 1 0
\(f_{11}\!\) 1011 \((u (v))\!\) 0 1 0 0 1 1 0 1
\(f_{13}\!\) 1101 \(((u) v)\!\) 0 0 1 0 1 0 1 1
\(f_{14}\!\) 1110 \(((u)(v))~\!\) 0 0 0 1 0 1 1 1
\(f_{15}\!\) 1111 \(((~))\!\) 0 0 0 0 1 1 1 1


\(\text{Table 10.} ~~ \text{Relation of Quantifiers to Higher Order Propositions}\!\)
\(\text{Mnemonic}\!\) \(\text{Category}\!\) \(\text{Classical Form}\!\) \(\text{Alternate Form}\!\) \(\text{Symmetric Form}\!\) \(\text{Operator}\!\)
\(\text{E}\!\)
\(\text{Exclusive}\!\)
\(\text{Universal}\!\)
\(\text{Negative}\!\)
\(\text{All}\ u\ \text{is}\ (v)\!\)   \(\text{No}\ u\ \text{is}\ v \!\) \((\ell_{11})\!\)
\(\text{A}\!\)
\(\text{Absolute}~\!\)
\(\text{Universal}\!\)
\(\text{Affirmative}\!\)
\(\text{All}\ u\ \text{is}\ v \!\)   \(\text{No}\ u\ \text{is}\ (v)\!\) \((\ell_{10})\!\)
    \(\text{All}\ v\ \text{is}\ u \!\) \(\text{No}\ v\ \text{is}\ (u)\!\) \(\text{No}\ (u)\ \text{is}\ v \!\) \((\ell_{01})\!\)
    \(\text{All}\ (v)\ \text{is}\ u \!\) \(\text{No}\ (v)\ \text{is}\ (u)\!\) \(\text{No}\ (u)\ \text{is}\ (v)\!\) \((\ell_{00})\!\)
    \(\text{Some}\ (u)\ \text{is}\ (v)\!\)   \(\text{Some}\ (u)\ \text{is}\ (v)\!\) \(\ell_{00}\!\)
    \(\text{Some}\ (u)\ \text{is}\ v\!\)   \(\text{Some}\ (u)\ \text{is}\ v\!\) \(\ell_{01}\!\)
\(\text{O}\!\)
\(\text{Obtrusive}\!\)
\(\text{Particular}\!\)
\(\text{Negative}\!\)
\(\text{Some}\ u\ \text{is}\ (v)\!\)   \(\text{Some}\ u\ \text{is}\ (v)\!\) \(\ell_{10}~\!\)
\(\text{I}\!\)
\(\text{Indefinite}\!\)
\(\text{Particular}\!\)
\(\text{Affirmative}\!\)
\(\text{Some}\ u\ \text{is}\ v\!\)   \(\text{Some}\ u\ \text{is}\ v\!\) \(\ell_{11}\!\)


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 \(\Upsilon,\!\) 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 : \bigcup_{\ell = 1, 2, 3} ((\mathbb{B}^k \to \mathbb{B})^\ell \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:

\(\Upsilon_p^r q = \Upsilon (p, q, r)\!\)
\(\Upsilon_p^r : (\mathbb{B}^k \to \mathbb{B}) \to \mathbb{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^k\!\) 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 : \mathbb{B}^k \to \mathbb{B}\!\) for the lower index \(p,\!\) and the continued conjunction or continued product operation \(\textstyle\prod\!\) for the upper index \(r.\!\) Taking the upper default value gives license to the following readings:

\(\Upsilon_p (q) = \Upsilon (p, q) = \Upsilon (p, q, \textstyle\prod).\!\)
\(\Upsilon_p = \Upsilon (p, \underline{~~}, \textstyle\prod) : (\mathbb{B}^k \to \mathbb{B}) \to \mathbb{B}.\!\)

This means that \(\Upsilon_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 \Rightarrow q,\!\) or that \(\underline{(p (q))} = \underline{1}.\!\)

Throwing in the lower default value permits the following abbreviations:

\(\Upsilon q = \Upsilon (q) = \Upsilon_1 (q) = \Upsilon (1, q, \textstyle\prod).\!\)
\(\Upsilon = \Upsilon (1, \underline{~~}, \textstyle\prod)) : (\mathbb{B}^k\ \to \mathbb{B}) \to \mathbb{B}.\!\)

This means that \(\Upsilon 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 : \mathbb{B}^k \to \mathbb{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.

Readings

  • Quine, W.V. (1969/1981), "On the Limits of Decision", Akten des XIV. Internationalen Kongresses für Philosophie, vol. 3 (1969). Reprinted, pp. 156–163 in Quine (ed., 1981), Theories and Things, Harvard University Press, Cambridge, MA.

Document History

Note. The above material is excerpted from a project report on Charles Sanders Peirce's conceptions of inquiry and analogy. Online formatting of the original document and continuation of the initial project are currently in progress under the title Functional Logic : Inquiry and Analogy.

Inquiry and Analogy

Author: Jon Awbrey November 1, 1995
Course: Engineering 690, Graduate Project Cont'd from Winter 1995
Supervisors: F. Mili & M.A. Zohdy Oakland University
| Version:  Draft 3.25
| Created:  01 Jan 1995
| Relayed:  01 Nov 1995
| Revised:  24 Dec 2001
| Revised:  12 Mar 2004

Functional Logic

Ontology List

  1. http://suo.ieee.org/ontology/msg05480.html
  2. http://suo.ieee.org/ontology/msg05481.html
  3. http://suo.ieee.org/ontology/msg05482.html
  4. http://suo.ieee.org/ontology/msg05483.html
  5. http://suo.ieee.org/ontology/msg05484.html
  6. http://suo.ieee.org/ontology/msg05485.html

Inquiry List

  1. http://stderr.org/pipermail/inquiry/2004-March/001256.html
  2. http://stderr.org/pipermail/inquiry/2004-March/001257.html
  3. http://stderr.org/pipermail/inquiry/2004-March/001258.html
  4. http://stderr.org/pipermail/inquiry/2004-March/001259.html
  5. http://stderr.org/pipermail/inquiry/2004-March/001260.html
  6. http://stderr.org/pipermail/inquiry/2004-March/001261.html

NKS Forum

  1. http://forum.wolframscience.com/showthread.php?postid=1957#post1957
  2. http://forum.wolframscience.com/showthread.php?postid=1960#post1960
  3. http://forum.wolframscience.com/showthread.php?postid=1961#post1961
  4. http://forum.wolframscience.com/showthread.php?postid=1962#post1962
  5. http://forum.wolframscience.com/showthread.php?postid=1964#post1964
  6. http://forum.wolframscience.com/showthread.php?postid=1966#post1966
  7. http://forum.wolframscience.com/showthread.php?postid=1968#post1968