Functional Logic : Higher Order Propositions
Idea
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 of a series of higher order propositions based on \(X.\)
Higher Order Propositional Expressions
By way of equipping the discussion with a modicum of concrete material, let's begin with a consideration of higher order propositions and logical operators that stem from the ordinary 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 that are 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}.\)
| \(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\) | \(\texttt{(~)}\) | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 |
| \(f_{1}\) | \(0 ~ 1\) | \(\texttt{(} x \texttt{)}\) | 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\) | \(\texttt{((~))}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 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 topped by a collection 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. These 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.
| 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's first consider the universe of discourse \(X^\circ = [x_1, x_2] = [u, v]\) that is based on just two logical features or boolean variables \(u\) and \(v.\)
The universe of discourse \(X^\circ\) consists of two parts, a set of points and a set of propositions.
The points of \(X^\circ\) form a space notated as follows:
|
\(\begin{matrix} X & = & \lang u, v \rang & = & \{ (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^\circ\) 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^\circ\) is \(X^{\circ 2} = [X^\circ] = [[u, v]],\) which may be developed in the following way. The propositions of \(X^\circ\) become the points of \(X^{\circ 2}\), and the mappings of the type \(m : (X \to \mathbb{B}) \to \mathbb{B}\) become the propositions of \(X^{\circ 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 these measures in the same style of higher order truth table used above. 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. Let us refer to the arrangement of measures that continues according to this plan as 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.
| \(\begin{matrix}u\!:\\v\!:\end{matrix}\) | \(\begin{matrix}1100\\1010\end{matrix}\) | \(f\) | \(\underset{0}{m}\) | \(\underset{1}{m}\) | \(\underset{2}{m}\) | \(\underset{3}{m}\) | \(\underset{4}{m}\) | \(\underset{5}{m}\) | \(\underset{6}{m}\) | \(\underset{7}{m}\) | \(\underset{8}{m}\) | \(\underset{9}{m}\) | \(\underset{10}{m}\) | \(\underset{11}{m}\) | \(\underset{12}{m}\) | \(\underset{13}{m}\) | \(\underset{14}{m}\) | \(\underset{15}{m}\) | \(\underset{16}{m}\) | \(\underset{17}{m}\) | \(\underset{18}{m}\) | \(\underset{19}{m}\) | \(\underset{20}{m}\) | \(\underset{21}{m}\) | \(\underset{22}{m}\) | \(\underset{23}{m}\) |
| \(f_{0}\) | \(0000\) | \(\texttt{(~)}\) | 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\) | \(\texttt{(} u \texttt{)(} v \texttt{)}\) | 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\) | \(\texttt{(} u\texttt{)} ~ 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\) | \(\texttt{(} u \texttt{)}\) | 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 ~ \texttt{(} v \texttt{)}\) | 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\) | \(\texttt{(} v \texttt{)}\) | 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\) | \(\texttt{(} u \texttt{,} v \texttt{)}\) | 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\) | \(\texttt{(} u ~ v \texttt{)}\) | 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\) | \(\texttt{((} u \texttt{,} v \texttt{))}\) | 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\) | \(\texttt{(} u ~ \texttt{(} v \texttt{))}\) | 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\) | \(\texttt{((} u \texttt{)} ~ v \texttt{)}\) | 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\) | \(\texttt{((} u \texttt{)(} v \texttt{))}\) | 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\) | \(\texttt{((~))}\) | 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 : (\lang u, v \rang \to \mathbb{B})^2 \to \mathbb{B}\) and \(\Upsilon_1 : (\lang u, v \rang \to \mathbb{B}) \to \mathbb{B},\) referred to as the relative and absolute umpire operators, respectively. If either 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 : \lang u, v \rang \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.\)
| \(\Upsilon (e, f) = 1 \qquad \operatorname{if~and~only~if} \qquad e \Rightarrow f\) |
Expressing it another way:
| \(\Upsilon (e, f) = 1 \qquad \iff \qquad \texttt{(} e \texttt{(} f \texttt{))} = 1\) |
In writing this, however, it is important to notice 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:
|
\( \Upsilon (e, f) = 1 \in \mathbb{B} \qquad \iff \qquad \texttt{(} e \texttt{(} f \texttt{))} = 1 : \lang u, v \rang \to \mathbb{B} \) |
Writing types as subscripts and using the fact that \(X = \lang u, v \rang,\) it is possible to express this a little more succinctly as follows:
|
\( \Upsilon (e, f) = 1_\mathbb{B} \qquad \iff \qquad \texttt{(} e \texttt{(} f \texttt{))} = 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 the relative umpire operator, we next define the absolute umpire operator, also known as the umpire measure. In the present setting this is a higher order proposition \(\Upsilon_1 : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}\) that is defined by the equation \(\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_\mathbb{B} \qquad \iff \qquad \texttt{(} 1 \texttt{(} f \texttt{))} = \mathbf{1} \qquad \iff \qquad f = 1_{\mathbb{B}^2 \to \mathbb{B}} \) |
The umpire measure is defined at the level of boolean 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 \texttt{(} e \texttt{(} f \texttt{))}.\)
Measure for Measure
Define two families of measures:
| \(\alpha_i, \beta_i : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}, ~ 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}\) |
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.
| \(\begin{matrix}u\!:\\v\!:\end{matrix}\) | \(\begin{matrix}1100\\1010\end{matrix}\) | \(f\) | \(\alpha_{15}\) | \(\alpha_{14}\) | \(\alpha_{13}\) | \(\alpha_{12}\) | \(\alpha_{11}\) | \(\alpha_{10}\) | \(\alpha_{9}\) | \(\alpha_{8}\) | \(\alpha_{7}\) | \(\alpha_{6}\) | \(\alpha_{5}\) | \(\alpha_{4}\) | \(\alpha_{3}\) | \(\alpha_{2}\) | \(\alpha_{1}\) | \(\alpha_{0}\) |
| \(f_{0}\) | \(0000\) | \(\texttt{(~)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 |
| \(f_{1}\) | \(0001\) | \(\texttt{(} u \texttt{)(} v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 |
| \(f_{2}\) | \(0010\) | \(\texttt{(} u\texttt{)} ~ v\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 1 |
| \(f_{3}\) | \(0011\) | \(\texttt{(} u \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 |
| \(f_{4}\) | \(0100\) | \(u ~ \texttt{(} v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 |
| \(f_{5}\) | \(0101\) | \(\texttt{(} v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 |
| \(f_{6}\) | \(0110\) | \(\texttt{(} u \texttt{,} v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 |
| \(f_{7}\) | \(0111\) | \(\texttt{(} u ~ v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| \(f_{8}\) | \(1000\) | \(u ~ v\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 |
| \(f_{9}\) | \(1001\) | \(\texttt{((} u \texttt{,} v \texttt{))}\) | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 |
| \(f_{10}\) | \(1010\) | \(v\) | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 1 |
| \(f_{11}\) | \(1011\) | \(\texttt{(} u ~ \texttt{(} v \texttt{))}\) | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 |
| \(f_{12}\) | \(1100\) | \(u\) | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 |
| \(f_{13}\) | \(1101\) | \(\texttt{((} u \texttt{)} ~ v \texttt{)}\) | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 |
| \(f_{14}\) | \(1110\) | \(\texttt{((} u \texttt{)(} v \texttt{))}\) | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 |
| \(f_{15}\) | \(1111\) | \(\texttt{((~))}\) | 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.
| \(\begin{matrix}u\!:\\v\!:\end{matrix}\) | \(\begin{matrix}1100\\1010\end{matrix}\) | \(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\) | \(\texttt{(~)}\) | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| \(f_{1}\) | \(0001\) | \(\texttt{(} u \texttt{)(} v \texttt{)}\) | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 0 | 1 |
| \(f_{2}\) | \(0010\) | \(\texttt{(} u\texttt{)} ~ v\) | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | 1 |
| \(f_{3}\) | \(0011\) | \(\texttt{(} u \texttt{)}\) | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 |
| \(f_{4}\) | \(0100\) | \(u ~ \texttt{(} v \texttt{)}\) | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 |
| \(f_{5}\) | \(0101\) | \(\texttt{(} v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 1 |
| \(f_{6}\) | \(0110\) | \(\texttt{(} u \texttt{,} v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 |
| \(f_{7}\) | \(0111\) | \(\texttt{(} u ~ v \texttt{)}\) | 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\) | \(\texttt{((} u \texttt{,} v \texttt{))}\) | 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\) | \(\texttt{(} u ~ \texttt{(} v \texttt{))}\) | 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\) | \(\texttt{((} u \texttt{)} ~ v \texttt{)}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 1 |
| \(f_{14}\) | \(1110\) | \(\texttt{((} u \texttt{)(} v \texttt{))}\) | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 |
| \(f_{15}\) | \(1111\) | \(\texttt{((~))}\) | 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\) 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 that occupy the limiting positions of the Tables.
|
\(\begin{array}{*{8}{r}} \alpha_{0} f = 1 & \operatorname{iff} & f_{0} \Rightarrow f & \operatorname{iff} & 0 \Rightarrow f, & \operatorname{hence} & \alpha_{0} f = 1 & \operatorname{for~all} ~ f. \\ \alpha_{15} f = 1 & \operatorname{iff} & f_{15} \Rightarrow f & \operatorname{iff} & 1 \Rightarrow f, & \operatorname{hence} & \alpha_{15} f = 1 & \operatorname{iff} ~ f = 1. \\ \beta_{0} f = 1 & \operatorname{iff} & f \Rightarrow f_{0} & \operatorname{iff} & f \Rightarrow 0, & \operatorname{hence} & \beta_{0} f = 1 & \operatorname{iff} ~ f = 0. \\ \beta_{15} f = 1 & \operatorname{iff} & f \Rightarrow f_{15} & \operatorname{iff} & f \Rightarrow 1, & \operatorname{hence} & \beta_{15} f = 1 & \operatorname{for~all} ~ f. \end{array}\) |
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 fiber notation to indicate sets of models, it is natural to use notations like the following to denote sets of propositions that satisfy the umpires in question.
| \([| \alpha_i |]\) | \(=\) | \((\alpha_i)^{-1}(1),\) |
| \([| \beta_i |]\) | \(=\) | \((\beta_i)^{-1}(1),\) |
| \([| \Upsilon_p |]\) | \(=\) | \((\Upsilon_p)^{-1}(1).\) |
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. 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, 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 medium of quantification theory closer to familiar ground, toward the predicates themselves that represent our continuing acquaintance with phenomena.
