Functional Logic • Quantification Theory

Author: Jon Awbrey

Functional Conception of Quantification Theory

Up till now quantification theory has been based on the assumption of individual variables ranging over universal collections of perfectly determinate elements.  The mere act of writing 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.  As we reflect more critically on the conventional assumptions in the light of pragmatic and constructive principles, however, they begin to appear as problematic hypotheses whose warrants are not beyond question, as projects of exhaustive determination overreaching the powers of finite information and control to manage.  Thus it is worth considering how the scene of quantification theory might be shifted nearer to familiar ground, toward the predicates themselves which represent our continuing acquaintance with phenomena.

Higher Order Propositional Expressions

If functions of type $X\to \mathbb {B}$ are propositions about things in $X$ then functions of type $(X\to \mathbb {B} )\to \mathbb {B}$ are propositions about propositions about things in $X,$ the first in a series of higher order propositions based on $X.$

To ground this inquiry in concrete material, let us begin with a consideration of higher order propositional expressions, in particular, those stemming from propositions on 1 and 2 variables.

Note on notation.  The discussion that follows uses minimal negation operations, expressed as parenthesized 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 a proposition about propositions.  If the original order of propositions consists of maps of the form $f:X\to \mathbb {B} ,$ then the next higher order of propositions consists of maps of the form $m:(X\to \mathbb {B} )\to \mathbb {B} .$  It is often useful to think of a higher order proposition as a measure on propositions.

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 based on this set, all taking the form $m:(\mathbb {B} \to \mathbb {B} )\to \mathbb {B} .$

Table 1 lists the 16 measures of the form $m:(\mathbb {B} \to \mathbb {B} )\to \mathbb {B} .$

${\text{Table 1. Higher Order Propositions}}~(n=1)$

The contents of Table 1 are organized as follows.  Columns 1 and 2 form a truth table for the four propositions of the form $f:\mathbb {B} \to \mathbb {B} ,$ with the row leaders in Column 1 displaying the names of the functions $f_{i}$ for $i$ = 0 to 3, 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 a more or less canonical expression for the proposition in question.  The last sixteen columns are headed by a series of conventional names for the measures $m_{j}$ as $j$ ranges from 0 to 15, where the entries in the body of the Table record the values assigned to each $f_{i}$ by each $m_{j}.$

Table 2 presents a sample of interpretive categories for higher order propositions of type $(\mathbb {B} ^{1}\to \mathbb {B} )\to \mathbb {B} ,$ but it's best to put off discussing this Table further until we get beyond the 1-dimensional case.  The lower dimensional cases tend to be extremely condensed or degenerate in their structures, and the pattern of what's going on here can be set in higher relief as soon as we get even two logical variables to play off each other.

${\text{Table 2. Interpretive Categories for Higher Order Propositions}}~(n=1)$

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's first consider the universe of discourse $X^{\bullet }=[x_{1},x_{2}]=[u,v]$ based on two logical features or boolean variables $u$ and $v.$

The universe of discourse $X^{\bullet }$ consists of two parts, a set of points and a set of propositions.

The points of $X^{\bullet }$ form a space notated as follows.

${\begin{matrix}X&=&\langle u,v\rangle &=&\{(u,v)\}&\cong &\mathbb {B} ^{2}\end{matrix}}$

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.

${\begin{array}{*{11}{c}}X&=&\{\quad {\texttt {(}}u{\texttt {)(}}v{\texttt {)}}&,&{\texttt {(}}u{\texttt {)}}~v&,&u~{\texttt {(}}v{\texttt {)}}&,&u~v\quad \}&\cong &\mathbb {B} ^{2}\end{array}}$

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.

${\begin{array}{*{11}{c}}X&=&\{\quad (0,0)&,&(0,1)&,&(1,0)&,&(1,1)\quad \}&\cong &\mathbb {B} ^{2}\end{array}}$

The propositions of $X^{\bullet }$ form a space notated as follows.

${\begin{array}{*{7}{c}}X^{\uparrow }&=&(X\to \mathbb {B} )&=&\{f:X\to \mathbb {B} \}&\cong &(\mathbb {B} ^{2}\to \mathbb {B} )\end{array}}$

As always, it is convenient to overlook the finer marks of distinction between isomorphic structures, so long as one is aware of their presence and knows when it is critical to call on them again.

The next higher order universe of discourse that is built on $X^{\bullet }$ is $X^{\bullet 2}=[X^{\bullet }]=[[u,v]],$ which may be developed in the following way.  The propositions of $X^{\bullet }$ become the points of $X^{\bullet 2},$ and the mappings of the type $m:(X\to \mathbb {B} )\to \mathbb {B}$ become the propositions of $X^{\bullet 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, let us 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}(0)$ that $m_{j}$ dislikes and the pictures $m_{j}^{-1}(1)$ that $m_{j}$ likes.

There are $2^{16}=65536$ measures of the form $m:(\mathbb {B} ^{2}\to \mathbb {B} )\to \mathbb {B} .$  Table 3 shows the first 24 of their number in the style of higher order truth table used above.  The column headed $m_{j}$ shows the value of the measure $m_{j}$ on each of the propositions $f_{i}:\mathbb {B} ^{2}\to \mathbb {B}$ for $i$ = 0 to 15.  The arrangement of measures in the order indicated will be called their standard ordering.  In this scheme of things, the index $j$ of the measure $m_{j}$ is the decimal equivalent of the bit string in the corresponding column of the Table, reading the binary digits in order from bottom to top.

${\text{Table 3. Higher Order Propositions}}~(n=2)$

Umpire Operators

The $2^{16}$ measures of type $(\mathbb {B} \times \mathbb {B} \to \mathbb {B} )\to \mathbb {B}$ present a formidable array of propositions about propositions about 2-dimensional universes of discourse.  The early entries in their standard ordering define universes too amorphous to detain us for long on a first pass but as we turn toward the high end of the ordering we begin to recognize familiar structures worth examining from new angles.

Instrumental to our study we define a couple of higher order operators,

${\begin{matrix}\Upsilon :(\mathbb {B} \times \mathbb {B} \to \mathbb {B} )^{2}\to \mathbb {B} &&{\text{and}}&&\Upsilon _{1}:(\mathbb {B} \times \mathbb {B} \to \mathbb {B} )\to \mathbb {B} ,\end{matrix}}$

referred to as the relative and absolute umpire operators, respectively.  If either operator is defined in terms of more primitive notions then the remaining operator can be defined in terms of the one first established.

Let $X=\langle u,v\rangle$ be a two-dimensional boolean space, $X\cong \mathbb {B} \times \mathbb {B} ,$ generated by two boolean variables or logical features $u$ and $v.$

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

${\begin{matrix}\Upsilon (e,f)=1&&{\text{if and only if}}&&e\Rightarrow f\end{matrix}}$

Expressing it another way:

${\begin{matrix}\Upsilon (e,f)=1&&\iff &&{\texttt {(}}e{\texttt {(}}f{\texttt {))}}=1\end{matrix}}$

In writing this, however, it is important to observe that the $1$ appearing on the left side and the $1$ appearing on the right side of the logical equivalence have different meanings.  Filling in the details, we have the following.

${\begin{matrix}\Upsilon (e,f)=1\in \mathbb {B} &&\iff &&{\texttt {(}}e{\texttt {(}}f{\texttt {))}}=1:\langle u,v\rangle \to \mathbb {B} \end{matrix}}$

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.

${\begin{matrix}\Upsilon (e,f)=1_{\mathbb {B} }&&\iff &&{\texttt {(}}e{\texttt {(}}f{\texttt {))}}=1_{X\to \mathbb {B} }\end{matrix}}$

Finally, it is often convenient to write the first argument as a subscript.  Thus we have the following equation.

${\begin{matrix}\Upsilon _{e}(f)&=&\Upsilon (e,f).\end{matrix}}$

The absolute umpire operator, also known as the umpire measure, is a higher order proposition $\Upsilon _{1}:(\mathbb {B} \times \mathbb {B} \to \mathbb {B} )\to \mathbb {B}$ defined by the equation $\Upsilon _{1}(f)=\Upsilon (1,f).$  In this case the subscript $1$ on the left and the argument $1$ on the right both refer to the constant proposition $1:\mathbb {B} \times \mathbb {B} \to \mathbb {B} .$  In most settings where $\Upsilon _{1}$ is applied to arguments it is safe to omit the subscript $1$ since the number of arguments indicates which type of operator is meant.  Thus, we have the following identities and equivalents.

${\begin{matrix}\Upsilon f=\Upsilon _{1}(f)=1_{\mathbb {B} }&\iff &{\texttt {(}}1{\texttt {(}}f{\texttt {))}}=\mathbf {1} &\iff &f=1_{\mathbb {B} \times \mathbb {B} \to \mathbb {B} }\end{matrix}}$

The umpire measure $\Upsilon _{1}$ is defined at the level of boolean functions as mathematical objects but can also be understood in terms of the judgments it induces on the syntactic level.  In that interpretation $\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 measure could have been defined as $\Upsilon _{e}f=\Upsilon {\texttt {(}}e{\texttt {(}}f{\texttt {))}}.$

Measure for Measure

Let us define two families of measures,

$\alpha _{i},\beta _{i}:(\mathbb {B} \times \mathbb {B} \to \mathbb {B} )\to \mathbb {B} ~{\text{for}}~i=0~{\text{to}}~15,$

by means of the following equations:

${\begin{matrix}\alpha _{i}f&=&\Upsilon (f_{i},f)&=&\Upsilon (f_{i}\Rightarrow f),\\[6pt]\beta _{i}f&=&\Upsilon (f,f_{i})&=&\Upsilon (f\Rightarrow f_{i}).\end{matrix}}$

Table 4 shows the value of each $\alpha _{i}$ on each of the 16 boolean functions $f:\mathbb {B} \times \mathbb {B} \to \mathbb {B} .$  In terms of the implication ordering on the 16 functions, $\alpha _{i}f=1$ says that $f$ is above or identical to $f_{i}$ in the implication lattice, that is, $f\geq f_{i}$ in the implication ordering.

${\text{Table 4. Qualifiers of the Implication Ordering}}~\alpha _{i}f=\Upsilon (f_{i},f)$

Table 5 shows the value of each $\beta _{i}$ on each of the 16 boolean functions $f:\mathbb {B} \times \mathbb {B} \to \mathbb {B} .$  In terms of the implication ordering on the 16 functions, $\beta _{i}f=1$ says that $f$ is below or identical to $f_{i}$ in the implication lattice, that is, $f\leq f_{i}$ in the implication ordering.

${\text{Table 5. Qualifiers of the Implication Ordering}}~\beta _{i}f=\Upsilon (f,f_{i})$

Applied to a given proposition $f,$ the qualifiers $\alpha _{i}$ and $\beta _{i}$ tell whether $f$ is above $f_{i}$ or below $f_{i},$ respectively, in the implication ordering.  By way of example, let us trace the effects of several such measures, namely, those which occupy the limiting positions in the Tables.

${\begin{array}{*{8}{r}}\alpha _{0}f=1&\mathrm {iff} &f_{0}\Rightarrow f&\mathrm {iff} &0\Rightarrow f,&\mathrm {hence} &\alpha _{0}f=1&\mathrm {for~all} ~f.\\[4pt]\alpha _{15}f=1&\mathrm {iff} &f_{15}\Rightarrow f&\mathrm {iff} &1\Rightarrow f,&\mathrm {hence} &\alpha _{15}f=1&\mathrm {iff} ~f=1.\\[4pt]\beta _{0}f=1&\mathrm {iff} &f\Rightarrow f_{0}&\mathrm {iff} &f\Rightarrow 0,&\mathrm {hence} &\beta _{0}f=1&\mathrm {iff} ~f=0.\\[4pt]\beta _{15}f=1&\mathrm {iff} &f\Rightarrow f_{15}&\mathrm {iff} &f\Rightarrow 1,&\mathrm {hence} &\beta _{15}f=1&\mathrm {for~all} ~f.\end{array}}$

Expressed in terms of the propositional forms they value positively, $\alpha _{0}=\beta _{15}$ is a totally indiscriminate measure, accepting all propositions $f:\mathbb {B} \times \mathbb {B} \to \mathbb {B} ,$ whereas $\alpha _{15}$ and $\beta _{0}$ are measures valuing the constant propositions $1:\mathbb {B} \times \mathbb {B} \to \mathbb {B}$ and $0:\mathbb {B} \times \mathbb {B} \to \mathbb {B} ,$ respectively, above all others.

Finally, in conformity with the use of fiber notation to indicate sets of models, it is natural to use notations like the following to denote sets of propositions satisfying the umpires in question.

${\begin{matrix}[|\alpha _{i}|]&=&\alpha _{i}^{-1}(1),\\[6pt][|\beta _{i}|]&=&\beta _{i}^{-1}(1),\\[6pt][|\Upsilon _{p}|]&=&\Upsilon _{p}^{-1}(1).\end{matrix}}$

Extending the Existential Interpretation to Quantificational Logic

One of the resources we have for this work is a formal calculus based on C.S. Peirce's logical graphs.  For now we'll adopt the existential interpretation of that calculus, fixing the meanings of logical constants and connectives at the core level of propositional logic.  To build on that core we'll need to extend the existential interpretation to encompass the analysis of quantified propositions, or quantifications.  That in turn will take developing two further capacities of our calculus.  On the formal side we'll need to consider higher order functional types, continuing our earlier venture above.  In terms of content we'll need to consider new species of elemental or singular propositions.

Let us return to the 2-dimensional universe $X^{\bullet }=[u,v].$  A bridge between propositions and quantifications is afforded by a set of measures or qualifiers $\ell _{ij}:(\mathbb {B} \times \mathbb {B} \to \mathbb {B} )\to \mathbb {B}$ defined by the following equations.

${\begin{array}{*{11}{l}}\ell _{00}f&=&\ell _{{\texttt {(}}u{\texttt {)(}}v{\texttt {)}}}f&=&\alpha _{1}f&=&\Upsilon _{{\texttt {(}}u{\texttt {)(}}v{\texttt {)}}}f&=&\Upsilon _{{\texttt {(}}u{\texttt {)(}}v{\texttt {)}}\,\Rightarrow \,f}&=&f~{\text{likes}}~{\texttt {(}}u{\texttt {)(}}v{\texttt {)}}\\\ell _{01}f&=&\ell _{{\texttt {(}}u{\texttt {)}}v}f&=&\alpha _{2}f&=&\Upsilon _{{\texttt {(}}u{\texttt {)}}v}f&=&\Upsilon _{{\texttt {(}}u{\texttt {)}}v\,\Rightarrow \,f}&=&f~{\text{likes}}~{\texttt {(}}u{\texttt {)}}v\\\ell _{10}f&=&\ell _{u{\texttt {(}}v{\texttt {)}}}f&=&\alpha _{4}f&=&\Upsilon _{u{\texttt {(}}v{\texttt {)}}}f&=&\Upsilon _{u{\texttt {(}}v{\texttt {)}}\,\Rightarrow \,f}&=&f~{\text{likes}}~u{\texttt {(}}v{\texttt {)}}\\\ell _{11}f&=&\ell _{u\,v}f&=&\alpha _{8}f&=&\Upsilon _{u\,v}f&=&\Upsilon _{u\,v\,\Rightarrow \,f}&=&f~{\text{likes}}~u\,v\end{array}}$

A higher order proposition $\ell _{ij}:(\mathbb {B} \times \mathbb {B} \to \mathbb {B} )\to \mathbb {B}$ tells us something about the proposition $f:\mathbb {B} \times \mathbb {B} \to \mathbb {B} ,$ namely, which elements in the space of type $\mathbb {B} \times \mathbb {B}$ are assigned a positive value by $f.$  Taken together, the $\ell _{ij}$ operators give us a way to express many useful observations about the propositions in $X^{\bullet }=[u,v].$  Figure 6 summarizes the action of the $\ell _{ij}$ operators on the propositions of type $f:\mathbb {B} \times \mathbb {B} \to \mathbb {B} .$

${\text{Figure 6. 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 expanding landscape of higher order propositions has come round to the point where we can begin to open up new perspectives on quantificational logic.

Though it may be all the same from a purely formal point of view, it does serve intuition to adopt a slightly different interpretation for the two-valued space we take as the target of our basic indicator functions.  In that spirit we declare a novel type of existence-valued functions $f:\mathbb {B} ^{k}\to \mathbb {E}$ where $\mathbb {E} =\{-e,+e\}=\{\mathrm {empty} ,\mathrm {existent} \}$ is a pair of values indicating whether anything exists in the cells of the underlying universe of discourse.  As usual, we won't be too picky about the coding of those functions, reverting to binary codes whenever the intended interpretation is clear enough.  With that interpretation in mind the next few Tables illustrate the correspondence between classical quantification theory and higher order indicator functions.

Table 7 exhibits a fourfold schema of quantified propositional forms traditionally known as a “Square of Opposition”, relating it to a quartet of higher order propositions which, depending on context, are also known as measures, qualifiers, or higher order indicator functions.

${\text{Table 7. Syllogistic Premisses as Higher Order Indicator Functions}}$

${\begin{array}{clcl}\mathrm {A} &{\text{Universal Affirmative}}&{\text{All}}~u~{\text{is}}~v&{\text{Indicator of}}~u{\texttt {(}}v{\texttt {)}}=0\\[4pt]\mathrm {E} &{\text{Universal Negative}}&{\text{All}}~u~{\text{is}}~{\texttt {(}}v{\texttt {)}}&{\text{Indicator of}}~u\cdot v=0\\[4pt]\mathrm {I} &{\text{Particular Affirmative}}&{\text{Some}}~u~{\text{is}}~v&{\text{Indicator of}}~u\cdot v=1\\[4pt]\mathrm {O} &{\text{Particular Negative}}&{\text{Some}}~u~{\text{is}}~{\texttt {(}}v{\texttt {)}}&{\text{Indicator of}}~u{\texttt {(}}v{\texttt {)}}=1\end{array}}$

Table 8 develops the above ideas in further detail, expressing a larger set of quantified propositional forms by means of propositions about propositions.

${\text{Table 8. Simple Qualifiers of Propositions (Version 1)}}$

${\begin{matrix}u\!:\\v\!:\end{matrix}}$	${\begin{matrix}1100\\1010\end{matrix}}$	$f$	${\begin{smallmatrix}{\texttt {(}}\ell _{11}{\texttt {)}}\\{\text{No}}~u\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{10}{\texttt {)}}\\{\text{No}}~u\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{01}{\texttt {)}}\\{\text{No}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{00}{\texttt {)}}\\{\text{No}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{00}\\{\text{Some}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{01}\\{\text{Some}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{10}\\{\text{Some}}~u\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{11}\\{\text{Some}}~u\\{\text{is}}~v\end{smallmatrix}}$
$f_{0}$	$0000$	${\texttt {(}}~{\texttt {)}}$	1	1	1	1	0	0	0	0
$f_{1}$	$0001$	${\texttt {(}}u{\texttt {)(}}v{\texttt {)}}$	1	1	1	0	1	0	0	0
$f_{2}$	$0010$	${\texttt {(}}u{\texttt {)}}~v$	1	1	0	1	0	1	0	0
$f_{3}$	$0011$	${\texttt {(}}u{\texttt {)}}$	1	1	0	0	1	1	0	0
$f_{4}$	$0100$	$u~{\texttt {(}}v{\texttt {)}}$	1	0	1	1	0	0	1	0
$f_{5}$	$0101$	${\texttt {(}}v{\texttt {)}}$	1	0	1	0	1	0	1	0
$f_{6}$	$0110$	${\texttt {(}}u{\texttt {,}}v{\texttt {)}}$	1	0	0	1	0	1	1	0
$f_{7}$	$0111$	${\texttt {(}}u~v{\texttt {)}}$	1	0	0	0	1	1	1	0
$f_{8}$	$1000$	$u~v$	0	1	1	1	0	0	0	1
$f_{9}$	$1001$	${\texttt {((}}u{\texttt {,}}v{\texttt {))}}$	0	1	1	0	1	0	0	1
$f_{10}$	$1010$	$v$	0	1	0	1	0	1	0	1
$f_{11}$	$1011$	${\texttt {(}}u~{\texttt {(}}v{\texttt {))}}$	0	1	0	0	1	1	0	1
$f_{12}$	$1100$	$u$	0	0	1	1	0	0	1	1
$f_{13}$	$1101$	${\texttt {((}}u{\texttt {)}}~v{\texttt {)}}$	0	0	1	0	1	0	1	1
$f_{14}$	$1110$	${\texttt {((}}u{\texttt {)(}}v{\texttt {))}}$	0	0	0	1	0	1	1	1
$f_{15}$	$1111$	${\texttt {((}}~{\texttt {))}}$	0	0	0	0	1	1	1	1

Tables 9 and 10 present the same information as Table 8, sorting the rows in different orders to reveal other symmetries in the arrays.

${\text{Table 9. Simple Qualifiers of Propositions (Version 2)}}$

${\begin{matrix}u\!:\\v\!:\end{matrix}}$	${\begin{matrix}1100\\1010\end{matrix}}$	$f$	${\begin{smallmatrix}{\texttt {(}}\ell _{11}{\texttt {)}}\\{\text{No}}~u\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{10}{\texttt {)}}\\{\text{No}}~u\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{01}{\texttt {)}}\\{\text{No}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{00}{\texttt {)}}\\{\text{No}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{00}\\{\text{Some}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{01}\\{\text{Some}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{10}\\{\text{Some}}~u\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{11}\\{\text{Some}}~u\\{\text{is}}~v\end{smallmatrix}}$
$f_{0}$	$0000$	${\texttt {(}}~{\texttt {)}}$	1	1	1	1	0	0	0	0
$f_{1}$	$0001$	${\texttt {(}}u{\texttt {)(}}v{\texttt {)}}$	1	1	1	0	1	0	0	0
$f_{2}$	$0010$	${\texttt {(}}u{\texttt {)}}~v$	1	1	0	1	0	1	0	0
$f_{4}$	$0100$	$u~{\texttt {(}}v{\texttt {)}}$	1	0	1	1	0	0	1	0
$f_{8}$	$1000$	$u~v$	0	1	1	1	0	0	0	1
$f_{3}$	$0011$	${\texttt {(}}u{\texttt {)}}$	1	1	0	0	1	1	0	0
$f_{12}$	$1100$	$u$	0	0	1	1	0	0	1	1
$f_{6}$	$0110$	${\texttt {(}}u{\texttt {,}}v{\texttt {)}}$	1	0	0	1	0	1	1	0
$f_{9}$	$1001$	${\texttt {((}}u{\texttt {,}}v{\texttt {))}}$	0	1	1	0	1	0	0	1
$f_{5}$	$0101$	${\texttt {(}}v{\texttt {)}}$	1	0	1	0	1	0	1	0
$f_{10}$	$1010$	$v$	0	1	0	1	0	1	0	1
$f_{7}$	$0111$	${\texttt {(}}u~v{\texttt {)}}$	1	0	0	0	1	1	1	0
$f_{11}$	$1011$	${\texttt {(}}u~{\texttt {(}}v{\texttt {))}}$	0	1	0	0	1	1	0	1
$f_{13}$	$1101$	${\texttt {((}}u{\texttt {)}}~v{\texttt {)}}$	0	0	1	0	1	0	1	1
$f_{14}$	$1110$	${\texttt {((}}u{\texttt {)(}}v{\texttt {))}}$	0	0	0	1	0	1	1	1
$f_{15}$	$1111$	${\texttt {((}}~{\texttt {))}}$	0	0	0	0	1	1	1	1

${\text{Table 10. Simple Qualifiers of Propositions (Version 3)}}$

${\begin{matrix}u\!:\\v\!:\end{matrix}}$	${\begin{matrix}1100\\1010\end{matrix}}$	$f$	${\begin{smallmatrix}{\texttt {(}}\ell _{11}{\texttt {)}}\\{\text{No}}~u\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{10}{\texttt {)}}\\{\text{No}}~u\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{01}{\texttt {)}}\\{\text{No}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}{\texttt {(}}\ell _{00}{\texttt {)}}\\{\text{No}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{00}\\{\text{Some}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{01}\\{\text{Some}}~{\texttt {(}}u{\texttt {)}}\\{\text{is}}~v\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{10}\\{\text{Some}}~u\\{\text{is}}~{\texttt {(}}v{\texttt {)}}\end{smallmatrix}}$	${\begin{smallmatrix}\ell _{11}\\{\text{Some}}~u\\{\text{is}}~v\end{smallmatrix}}$
$f_{0}$	$0000$	${\texttt {(}}~{\texttt {)}}$	1	1	1	1	0	0	0	0
$f_{1}$	$0001$	${\texttt {(}}u{\texttt {)(}}v{\texttt {)}}$	1	1	1	0	1	0	0	0
$f_{2}$	$0010$	${\texttt {(}}u{\texttt {)}}~v$	1	1	0	1	0	1	0	0
$f_{4}$	$0100$	$u~{\texttt {(}}v{\texttt {)}}$	1	0	1	1	0	0	1	0
$f_{8}$	$1000$	$u~v$	0	1	1	1	0	0	0	1
$f_{12}$	$1100$	$u$	0	0	1	1	0	0	1	1
$f_{10}$	$1010$	$v$	0	1	0	1	0	1	0	1
$f_{9}$	$1001$	${\texttt {((}}u{\texttt {,}}v{\texttt {))}}$	0	1	1	0	1	0	0	1
$f_{6}$	$0110$	${\texttt {(}}u{\texttt {,}}v{\texttt {)}}$	1	0	0	1	0	1	1	0
$f_{5}$	$0101$	${\texttt {(}}v{\texttt {)}}$	1	0	1	0	1	0	1	0
$f_{3}$	$0011$	${\texttt {(}}u{\texttt {)}}$	1	1	0	0	1	1	0	0
$f_{7}$	$0111$	${\texttt {(}}u~v{\texttt {)}}$	1	0	0	0	1	1	1	0
$f_{11}$	$1011$	${\texttt {(}}u~{\texttt {(}}v{\texttt {))}}$	0	1	0	0	1	1	0	1
$f_{13}$	$1101$	${\texttt {((}}u{\texttt {)}}~v{\texttt {)}}$	0	0	1	0	1	0	1	1
$f_{14}$	$1110$	${\texttt {((}}u{\texttt {)(}}v{\texttt {))}}$	0	0	0	1	0	1	1	1
$f_{15}$	$1111$	${\texttt {((}}~{\texttt {))}}$	0	0	0	0	1	1	1	1

Table 11 provides a thumbnail sketch of the relationships discussed in this section.

${\text{Table 11. Relation of Quantifiers to Higher Order Propositions}}$

${\text{Mnemonic}}$	${\text{Category}}$	${\text{Classical Form}}$	${\text{Alternate Form}}$	${\text{Symmetric Form}}$	${\text{Operator}}$
${\begin{matrix}{\text{E}}\\{\text{Exclusive}}\end{matrix}}$	${\begin{matrix}{\text{Universal}}\\{\text{Negative}}\end{matrix}}$	${\text{All}}~u~{\text{is}}~{\texttt {(}}v{\texttt {)}}$		${\text{No}}~u~{\text{is}}~v$	${\texttt {(}}\ell _{11}{\texttt {)}}$
${\begin{matrix}{\text{A}}\\{\text{Absolute}}\end{matrix}}$	${\begin{matrix}{\text{Universal}}\\{\text{Affirmative}}\end{matrix}}$	${\text{All}}~u~{\text{is}}~v$		${\text{No}}~u~{\text{is}}~{\texttt {(}}v{\texttt {)}}$	${\texttt {(}}\ell _{10}{\texttt {)}}$
		${\text{All}}~v~{\text{is}}~u$	${\text{No}}~v~{\text{is}}~{\texttt {(}}u{\texttt {)}}$	${\text{No}}~{\texttt {(}}u{\texttt {)}}~{\text{is}}~v$	${\texttt {(}}\ell _{01}{\texttt {)}}$
		${\text{All}}~{\texttt {(}}v{\texttt {)}}~{\text{is}}~u$	${\text{No}}~{\texttt {(}}v{\texttt {)}}~{\text{is}}~{\texttt {(}}u{\texttt {)}}$	${\text{No}}~{\texttt {(}}u{\texttt {)}}~{\text{is}}~{\texttt {(}}v{\texttt {)}}$	${\texttt {(}}\ell _{00}{\texttt {)}}$
		${\text{Some}}~{\texttt {(}}u{\texttt {)}}~{\text{is}}~{\texttt {(}}v{\texttt {)}}$		${\text{Some}}~{\texttt {(}}u{\texttt {)}}~{\text{is}}~{\texttt {(}}v{\texttt {)}}$	$\ell _{00}$
		${\text{Some}}~{\texttt {(}}u{\texttt {)}}~{\text{is}}~v$		${\text{Some}}~{\texttt {(}}u{\texttt {)}}~{\text{is}}~v$	$\ell _{01}$
${\begin{matrix}{\text{O}}\\{\text{Obtrusive}}\end{matrix}}$	${\begin{matrix}{\text{Particular}}\\{\text{Negative}}\end{matrix}}$	${\text{Some}}~u~{\text{is}}~{\texttt {(}}v{\texttt {)}}$		${\text{Some}}~u~{\text{is}}~{\texttt {(}}v{\texttt {)}}$	$\ell _{10}$
${\begin{matrix}{\text{I}}\\{\text{Indefinite}}\end{matrix}}$	${\begin{matrix}{\text{Particular}}\\{\text{Affirmative}}\end{matrix}}$	${\text{Some}}~u~{\text{is}}~v$		${\text{Some}}~u~{\text{is}}~v$	$\ell _{11}$

Generalized Umpire Operators

To get a better handle on the space of higher order propositions and continue developing our functional approach to quantification theory, we'll need a number of specialized tools.  To begin, we define a higher order operator $\Upsilon ,$ called the umpire operator, which takes 1, 2, or 3 propositions as arguments and returns a single truth value as the result.  Operators with optional numbers of arguments are called multigrade operators, typically defined as unions over function types.  Expressing $\Upsilon$ in that form gives the following formula.

$\Upsilon :\bigcup _{\ell =1,2,3}((\mathbb {B} ^{k}\to \mathbb {B} )^{\ell }\to \mathbb {B} ).$

In contexts of application, that is, where a multigrade operator is actually being applied to arguments, the number of arguments in the argument list tells which of the optional types is “operative”.  In the case of $\Upsilon ,$ the first and last arguments appear as indices, the one in the middle serving 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.

${\begin{matrix}\Upsilon _{p}^{r}q=\Upsilon (p,q,r)\\[10pt]\Upsilon _{p}^{r}:(\mathbb {B} ^{k}\to \mathbb {B} )\to \mathbb {B} \end{matrix}}$

The operation $\Upsilon _{p}^{r}q$ evaluates the proposition $q$ on each model of the proposition $p$ and combines the results according to the method indicated by the connective parameter $r.$  In principle, the index $r$ may specify any logical connective on as many as $2^{k}$ arguments but in practice we usually have a much simpler form of combination in mind, typically either products or sums.  By convention, each of the accessory indices $p,r$ is assigned a default value 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.

${\begin{matrix}\Upsilon _{p}(q)=\Upsilon (p,q)=\Upsilon (p,q,\textstyle \prod ).\\[10pt]\Upsilon _{p}=\Upsilon (p,{\underline {~~}},\textstyle \prod ):(\mathbb {B} ^{k}\to \mathbb {B} )\to \mathbb {B} .\end{matrix}}$

This means $\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 ${\texttt {(}}p{\texttt {(}}q{\texttt {))}}=1.$

Throwing in the lower default value permits the following abbreviations.

${\begin{matrix}\Upsilon q=\Upsilon (q)=\Upsilon _{1}(q)=\Upsilon (1,q,\textstyle \prod ).\\[10pt]\Upsilon =\Upsilon (1,{\underline {~~}},\textstyle \prod )):(\mathbb {B} ^{k}\ \to \mathbb {B} )\to \mathbb {B} .\end{matrix}}$

This means $\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.

References

• 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.

Related Topics

• Functional Logic • Inquiry and Analogy
• Functional Logic • Higher Order Propositions

Resources

• Logic Syllabus

Document History

Note. The above material is taken 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.

1995 • Oakland University • Inquiry and Analogy

Author:	Jon Awbrey	November 1, 1995
Course:	Engineering 690, Graduate Project	Winter Term, January 1995
Supervisors:	M.A. Zohdy and F. Mili	Oakland University

| Version:  Draft 3.25
| Created:  01 Jan 1995
| Relayed:  01 Nov 1995
| Revised:  24 Dec 2001
| Revised:  12 Mar 2004

2004 • Inquiry List • Functional Logic

• http://web.archive.org/web/20140821214025/http://stderr.org/pipermail/inquiry/2004-March/thread.html#1256

1. http://web.archive.org/web/20090303000827/http://stderr.org/pipermail/inquiry/2004-March/001256.html
2. http://web.archive.org/web/20090303001935/http://stderr.org/pipermail/inquiry/2004-March/001257.html
3. http://web.archive.org/web/20090303002148/http://stderr.org/pipermail/inquiry/2004-March/001258.html
4. http://web.archive.org/web/20090303001240/http://stderr.org/pipermail/inquiry/2004-March/001259.html
5. http://web.archive.org/web/20090303001940/http://stderr.org/pipermail/inquiry/2004-March/001260.html
6. http://web.archive.org/web/20090303002026/http://stderr.org/pipermail/inquiry/2004-March/001261.html

2004 • Ontology List • Functional Logic

• http://web.archive.org/web/20090302185041/http://suo.ieee.org/ontology/thrd2.html#05480

1. http://web.archive.org/web/20090303202815/http://suo.ieee.org/ontology/msg05480.html
2. http://web.archive.org/web/20090302145522/http://suo.ieee.org/ontology/msg05481.html
3. http://web.archive.org/web/20090302145531/http://suo.ieee.org/ontology/msg05482.html
4. http://web.archive.org/web/20090303203051/http://suo.ieee.org/ontology/msg05483.html
5. http://web.archive.org/web/20090303203442/http://suo.ieee.org/ontology/msg05484.html
6. http://web.archive.org/web/20090302145538/http://suo.ieee.org/ontology/msg05485.html

2004 • NKS Forum • Functional Logic

• http://web.archive.org/web/20131120210604/http://forum.wolframscience.com/archive/topic/254.html
• http://web.archive.org/web/20090302144746/http://forum.wolframscience.com/showthread.php?threadid=254

2004 • NKS Forum • Introduction to Inquiry Driven Systems

• http://web.archive.org/web/20131104033846/http://forum.wolframscience.com/archive/topic/598.html
• http://web.archive.org/web/20160406171418/http://forum.wolframscience.com/showthread.php?threadid=598

1. http://web.archive.org/web/20090302150057/http://forum.wolframscience.com/showthread.php?postid=1957#post1957
2. http://web.archive.org/web/20090302145607/http://forum.wolframscience.com/showthread.php?postid=1960#post1960
3. http://web.archive.org/web/20090302150102/http://forum.wolframscience.com/showthread.php?postid=1961#post1961
4. http://web.archive.org/web/20090302150134/http://forum.wolframscience.com/showthread.php?postid=1962#post1962
5. http://web.archive.org/web/20090302145918/http://forum.wolframscience.com/showthread.php?postid=1964#post1964
6. http://web.archive.org/web/20090302145303/http://forum.wolframscience.com/showthread.php?postid=1966#post1966
7. http://web.archive.org/web/20090302150013/http://forum.wolframscience.com/showthread.php?postid=1968#post1968