Changes

Differential Logic and Dynamic Systems (view source)

Revision as of 21:40, 14 January 2021

526 bytes removed , 21:40, 14 January 2021

→‎A Functional Conception of Propositional Calculus: update

Line 238: Line 238:

|}

−

In the general case, we start with a set of logical features <math>\{a_1, \ldots, a_n\}</math> that represent properties of objects or propositions about the world. In concrete examples the features <math>\{a_i\!\}</math> commonly appear as capital letters from an ''alphabet'' like <math>\{A, B, C, \ldots\}</math> or as meaningful words from a linguistic ''vocabulary'' of codes. This language can be drawn from any sources, whether natural, technical, or artificial in character and interpretation. In the application to dynamic systems we tend to use the letters <math>\{x_1, \ldots, x_n\}</math> as our coordinate propositions, and to interpret them as denoting properties of a system's ''state'', that is, as propositions about its location in configuration space. Because I have to consider non-deterministic systems from the outset, I often use the word ''state'' in a loose sense, to denote the position or configuration component of a contemplated state vector, whether or not it ever gets a deterministic completion.

+

In the general case, we start with a set of logical features <math>\{a_1, \ldots, a_n\}</math> that represent properties of objects or propositions about the world. In concrete examples the features <math>\{a_i\}</math> commonly appear as capital letters from an ''alphabet'' like <math>\{A, B, C, \ldots\}</math> or as meaningful words from a linguistic ''vocabulary'' of codes. This language can be drawn from any sources, whether natural, technical, or artificial in character and interpretation. In the application to dynamic systems we tend to use the letters <math>\{x_1, \ldots, x_n\}</math> as our coordinate propositions, and to interpret them as denoting properties of a system's ''state'', that is, as propositions about its location in configuration space. Because I have to consider non-deterministic systems from the outset, I often use the word ''state'' in a loose sense, to denote the position or configuration component of a contemplated state vector, whether or not it ever gets a deterministic completion.

−

The set of logical features <math>\{a_1, \ldots, a_n\}</math> provides a basis for generating an <math>n\!</math>-dimensional ''[[universe of discourse]]'' that I denote as <math>[a_1, \ldots, a_n].</math> It is useful to consider each universe of discourse as a unified categorical object that incorporates both the set of points <math>\langle a_1, \ldots, a_n \rangle</math> and the set of propositions <math>f : \langle a_1, \ldots, a_n \rangle \to \mathbb{B}</math> that are implicit with the ordinary picture of a venn diagram on <math>n\!</math> features. Thus, we may regard the universe of discourse <math>[a_1, \ldots, a_n]</math> as an ordered pair having the type <math>(\mathbb{B}^n, (\mathbb{B}^n \to \mathbb{B}),</math> and we may abbreviate this last type designation as <math>\mathbb{B}^n\ +\!\to \mathbb{B},</math> or even more succinctly as <math>[\mathbb{B}^n].</math> (Used this way, the angle brackets <math>\langle\ldots\rangle</math> are referred to as ''generator brackets''.)

+

The set of logical features <math>\{a_1, \ldots, a_n\}</math> provides a basis for generating an <math>n</math>-dimensional ''[[universe of discourse]]'' that I denote as <math>[a_1, \ldots, a_n].</math> It is useful to consider each universe of discourse as a unified categorical object that incorporates both the set of points <math>\langle a_1, \ldots, a_n \rangle</math> and the set of propositions <math>f : \langle a_1, \ldots, a_n \rangle \to \mathbb{B}</math> that are implicit with the ordinary picture of a venn diagram on <math>n</math> features. Thus, we may regard the universe of discourse <math>[a_1, \ldots, a_n]</math> as an ordered pair having the type <math>(\mathbb{B}^n, (\mathbb{B}^n \to \mathbb{B}),</math> and we may abbreviate this last type designation as <math>\mathbb{B}^n\ +\!\to \mathbb{B},</math> or even more succinctly as <math>[\mathbb{B}^n].</math> (Used this way, the angle brackets <math>\langle\ldots\rangle</math> are referred to as ''generator brackets''.)

−

Table 2 exhibits the scheme of notation I use to formalize the domain of propositional calculus, corresponding to the logical content of truth tables and venn diagrams. Although it overworks the square brackets a bit, I also use either one of the equivalent notations <math>[n]\!</math> or <math>\mathbf{n}</math> to denote the data type of a finite set on <math>n\!</math> elements.

+

Table 2 exhibits the scheme of notation I use to formalize the domain of propositional calculus, corresponding to the logical content of truth tables and venn diagrams. Although it overworks the square brackets a bit, I also use either one of the equivalent notations <math>[n]</math> or <math>\mathbf{n}</math> to denote the data type of a finite set on <math>n</math> elements.

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"

−

|+ style="height:30px" | <math>\text{Table 2.} ~~ \text{Propositional Calculus : Basic Notation}\!</math>

+

|+ style="height:30px" | <math>\text{Table 2.} ~~ \text{Propositional Calculus : Basic Notation}</math>

|- style="height:40px; background:ghostwhite"

−

| <math>\text{Symbol}\!</math>

+

| <math>\text{Symbol}</math>

−

| <math>\text{Notation}\!</math>

+

| <math>\text{Notation}</math>

−

| <math>\text{Description}\!</math>

+

| <math>\text{Description}</math>

−

| <math>\text{Type}\!</math>

+

| <math>\text{Type}</math>

|-

−

| <math>\mathfrak{A}\!</math>

+

| <math>\mathfrak{A}</math>

−

| <math>\{ {}^{\backprime\backprime} a_1 {}^{\prime\prime}, \ldots, {}^{\backprime\backprime} a_n {}^{\prime\prime} \}\!</math>

+

| <math>\{ {}^{\backprime\backprime} a_1 {}^{\prime\prime}, \ldots, {}^{\backprime\backprime} a_n {}^{\prime\prime} \}</math>

−

| <math>\text{Alphabet}\!</math>

+

| <math>\text{Alphabet}</math>

−

| <math>[n] = \mathbf{n}\!</math>

+

| <math>[n] = \mathbf{n}</math>

|-

−

| <math>\mathcal{A}\!</math>

+

| <math>\mathcal{A}</math>

−

| <math>\{ a_1, \ldots, a_n \}\!</math>

+

| <math>\{ a_1, \ldots, a_n \}</math>

−

| <math>\text{Basis}\!</math>

+

| <math>\text{Basis}</math>

−

| <math>[n] = \mathbf{n}\!</math>

+

| <math>[n] = \mathbf{n}</math>

|-

−

| <math>A_i\!</math>

+

| <math>A_i</math>

−

| <math>\{ \texttt{(} a_i \texttt{)}, a_i \}\!</math>

+

| <math>\{ \texttt{(} a_i \texttt{)}, a_i \}</math>

−

| <math>\text{Dimension}~ i\!</math>

+

| <math>\text{Dimension}~ i</math>

−

| <math>\mathbb{B}\!</math>

+

| <math>\mathbb{B}</math>

|-

−

| <math>A\!</math>

+

| <math>A</math>

|

<math>\begin{matrix}

Line 294: Line 294:

\text{of discourse}

\end{matrix}</math>

−

| <math>\mathbb{B}^n\!</math>

+

| <math>\mathbb{B}^n</math>

|-

−

| <math>A^*\!</math>

+

| <math>A^*</math>

−

| <math>(\mathrm{hom} : A \to \mathbb{B})\!</math>

+

| <math>(\mathrm{hom} : A \to \mathbb{B})</math>

−

| <math>\text{Linear functions}\!</math>

+

| <math>\text{Linear functions}</math>

−

| <math>(\mathbb{B}^n)^* \cong \mathbb{B}^n\!</math>

+

| <math>(\mathbb{B}^n)^* \cong \mathbb{B}^n</math>

|-

−

| <math>A^\uparrow\!</math>

+

| <math>A^\uparrow</math>

−

| <math>(A \to \mathbb{B})\!</math>

+

| <math>(A \to \mathbb{B})</math>

−

| <math>\text{Boolean functions}\!</math>

+

| <math>\text{Boolean functions}</math>

−

| <math>\mathbb{B}^n \to \mathbb{B}\!</math>

+

| <math>\mathbb{B}^n \to \mathbb{B}</math>

|-

−

| <math>A^\bullet\!</math>

+

| <math>A^\bullet</math>

|

<math>\begin{matrix}

Line 352: Line 352:

These concepts and notations may now be explained in greater detail. In order to begin as simply as possible, let us distinguish two levels of analysis and set out initially on the easier path. On the first level of analysis we take spaces like <math>\mathbb{B},</math> <math>\mathbb{B}^n,</math> and <math>(\mathbb{B}^n \to \mathbb{B})</math> at face value and treat them as the primary objects of interest. On the second level of analysis we use these spaces as coordinate charts for talking about points and functions in more fundamental spaces.

−

A pair of spaces, of types <math>\mathbb{B}^n</math> and <math>(\mathbb{B}^n \to \mathbb{B}),</math> give typical expression to everything ~~that~~ we commonly associate with the ordinary picture of a venn diagram. The dimension, <math>n,\!</math> counts the number of "circles" or simple closed curves that are inscribed in the universe of discourse, corresponding to its relevant logical features or basic propositions. Elements of type <math>\mathbb{B}^n</math> correspond to what are often called propositional ''interpretations'' in logic, that is, the different assignments of truth values to sentence letters. Relative to a given universe of discourse, these interpretations are visualized as its ''cells'', in other words, the smallest enclosed areas or undivided regions of the venn diagram. The functions <math>f : \mathbb{B}^n \to \mathbb{B}</math> correspond to the different ways of shading the venn diagram to indicate arbitrary propositions, regions, or sets. Regions included under a shading indicate the ''models'', and regions excluded represent the ''non-models'' of a proposition. To recognize and formalize the natural cohesion of these two layers of concepts into a single universe of discourse, we introduce the type notations <math>[\mathbb{B}^n] = \mathbb{B}^n\ +\!\to \mathbb{B}</math> to stand for the pair of types <math>(\mathbb{B}^n, (\mathbb{B}^n \to \mathbb{B})).</math> The resulting "stereotype" serves to frame the universe of discourse as a unified categorical object, and makes it subject to prescribed sets of evaluations and transformations (categorical morphisms or ''arrows'') that affect the universe of discourse as an integrated whole.

+

A pair of spaces, of types <math>\mathbb{B}^n</math> and <math>(\mathbb{B}^n \to \mathbb{B}),</math> give typical expression to everything we commonly associate with the ordinary picture of a venn diagram. The dimension, <math>n,</math> counts the number of “circles” or simple closed curves that are inscribed in the universe of discourse, corresponding to its relevant logical features or basic propositions. Elements of type <math>\mathbb{B}^n</math> correspond to what are often called propositional ''interpretations'' in logic, that is, the different assignments of truth values to sentence letters. Relative to a given universe of discourse, these interpretations are visualized as its ''cells'', in other words, the smallest enclosed areas or undivided regions of the venn diagram. The functions <math>f : \mathbb{B}^n \to \mathbb{B}</math> correspond to the different ways of shading the venn diagram to indicate arbitrary propositions, regions, or sets. Regions included under a shading indicate the ''models'', and regions excluded represent the ''non-models'' of a proposition. To recognize and formalize the natural cohesion of these two layers of concepts into a single universe of discourse, we introduce the type notations <math>[\mathbb{B}^n] = \mathbb{B}^n\ +\!\to \mathbb{B}</math> to stand for the pair of types <math>(\mathbb{B}^n, (\mathbb{B}^n \to \mathbb{B})).</math> The resulting “stereotype” serves to frame the universe of discourse as a unified categorical object, and makes it subject to prescribed sets of evaluations and transformations (categorical morphisms or ''arrows'') that affect the universe of discourse as an integrated whole.

−

Most of the time we can serve the algebraic, geometric, and logical interests of our study without worrying about their occasional conflicts and incidental divergences. The conventions and definitions already set down will continue to cover most of the algebraic and functional aspects of our discussion, but to handle the logical and qualitative aspects we will need to add a few more. In general, abstract sets may be denoted by gothic, greek, or script capital variants of <math>A, B, C,\!</math> and so on, with their elements being denoted by a corresponding set of subscripted letters in plain lower case, for example, <math>\mathcal{A} = \{a_i\}.</math> Most of the time, a set such as <math>\mathcal{A} = \{a_i\}\!</math> will be employed as the ''alphabet'' of a [[formal language]]. These alphabet letters serve to name the logical features (properties or propositions) that generate a particular universe of discourse. When we want to discuss the particular features of a universe of discourse, beyond the abstract designation of a type like <math>(\mathbb{B}^n\ +\!\to \mathbb{B}),</math> then we may use the following notations. If <math>\mathcal{A} = \{a_1, \ldots, a_n\}</math> is an alphabet of logical features, then <math>A = \langle \mathcal{A} \rangle = \langle a_1, \ldots, a_n \rangle</math> is the set of interpretations, <math>A^\uparrow = (A \to \mathbb{B})</math> is the set of propositions, and <math>A^\bullet = [\mathcal{A}] = [a_1, \ldots, a_n]</math> is the combination of these interpretations and propositions into the universe of discourse that is based on the features <math>\{a_1, \ldots, a_n\}.</math>

+

Most of the time we can serve the algebraic, geometric, and logical interests of our study without worrying about their occasional conflicts and incidental divergences. The conventions and definitions already set down will continue to cover most of the algebraic and functional aspects of our discussion, but to handle the logical and qualitative aspects we will need to add a few more. In general, abstract sets may be denoted by gothic, greek, or script capital variants of <math>A, B, C,</math> and so on, with their elements being denoted by a corresponding set of subscripted letters in plain lower case, for example, <math>\mathcal{A} = \{a_i\}.</math> Most of the time, a set such as <math>\mathcal{A} = \{a_i\}</math> will be employed as the ''alphabet'' of a [[formal language]]. These alphabet letters serve to name the logical features (properties or propositions) that generate a particular universe of discourse. When we want to discuss the particular features of a universe of discourse, beyond the abstract designation of a type like <math>(\mathbb{B}^n\ +\!\to \mathbb{B}),</math> then we may use the following notations. If <math>\mathcal{A} = \{a_1, \ldots, a_n\}</math> is an alphabet of logical features, then <math>A = \langle \mathcal{A} \rangle = \langle a_1, \ldots, a_n \rangle</math> is the set of interpretations, <math>A^\uparrow = (A \to \mathbb{B})</math> is the set of propositions, and <math>A^\bullet = [\mathcal{A}] = [a_1, \ldots, a_n]</math> is the combination of these interpretations and propositions into the universe of discourse that is based on the features <math>\{a_1, \ldots, a_n\}.</math>

As always, especially in concrete examples, these rules may be dropped whenever necessary, reverting to a free assortment of feature labels. However, when we need to talk about the logical aspects of a space that is already named as a vector space, it will be necessary to make special provisions. At any rate, these elaborations can be deferred until actually needed.

Line 369: Line 369:

|}

−

For much of our discussion propositions and boolean functions are treated as the same formal objects, or as different interpretations of the same formal calculus. This rule of interpretation has exceptions, though. There is a distinctively logical interest in the use of propositional calculus that is not exhausted by its functional interpretation. It is part of our task in this study to deal with these uniquely logical characteristics as they present themselves both in our subject matter and in our formal calculus. Just to provide a hint of what's at stake: In logic, as opposed to the more imaginative realms of mathematics, we consider it a good thing to always know what we are talking about. Where mathematics encourages tolerance for uninterpreted symbols as intermediate terms, logic exerts a keener effort to interpret directly each oblique carrier of meaning, no matter how slight, and to unfold the complicities of every indirection in the flow of information. Translated into functional terms, this means that we want to maintain a continual, immediate, and persistent sense of both the converse relation <math>f^{-1} \subseteq \mathbb{B} \times \mathbb{B}^n,</math> or what is the same thing, <math>f^{-1} : \mathbb{B} \to \mathcal{P}(\mathbb{B}^n),</math> and the ''fibers'' or inverse images <math>f^{-1}(0)\!</math> and <math>f^{-1}(1),\!</math> associated with each boolean function <math>f : \mathbb{B}^n \to \mathbb{B}</math> that we use. In practical terms, the desired implementation of a propositional interpreter should incorporate our intuitive recognition that the induced partition of the functional domain into level sets <math>f^{-1}(b),\!</math> for <math>b \in \mathbb{B},</math> is part and parcel of understanding the denotative uses of each propositional function <math>f.\!</math>

+

For much of our discussion propositions and boolean functions are treated as the same formal objects, or as different interpretations of the same formal calculus. This rule of interpretation has exceptions, though. There is a distinctively logical interest in the use of propositional calculus that is not exhausted by its functional interpretation. It is part of our task in this study to deal with these uniquely logical characteristics as they present themselves both in our subject matter and in our formal calculus. Just to provide a hint of what's at stake: In logic, as opposed to the more imaginative realms of mathematics, we consider it a good thing to always know what we are talking about. Where mathematics encourages tolerance for uninterpreted symbols as intermediate terms, logic exerts a keener effort to interpret directly each oblique carrier of meaning, no matter how slight, and to unfold the complicities of every indirection in the flow of information. Translated into functional terms, this means that we want to maintain a continual, immediate, and persistent sense of both the converse relation <math>f^{-1} \subseteq \mathbb{B} \times \mathbb{B}^n,</math> or what is the same thing, <math>f^{-1} : \mathbb{B} \to \mathcal{P}(\mathbb{B}^n),</math> and the ''fibers'' or inverse images <math>f^{-1}(0)</math> and <math>f^{-1}(1),</math> associated with each boolean function <math>f : \mathbb{B}^n \to \mathbb{B}</math> that we use. In practical terms, the desired implementation of a propositional interpreter should incorporate our intuitive recognition that the induced partition of the functional domain into level sets <math>f^{-1}(b),</math> for <math>b \in \mathbb{B},</math> is part and parcel of understanding the denotative uses of each propositional function <math>f.</math>

===Special Classes of Propositions===

−

It is important to remember that the coordinate propositions <math>\{a_i\},\!</math> besides being projection maps <math>a_i : \mathbb{B}^n \to \mathbb{B},</math> are propositions on an equal footing with all others, even though employed as a basis in a particular moment. This set of <math>n\!</math> propositions may sometimes be referred to as the ''basic propositions'', the ''coordinate propositions'', or the ''simple propositions'' that found a universe of discourse. Either one of the equivalent notations, <math>\{a_i : \mathbb{B}^n \to \mathbb{B}\}</math> or <math>(\mathbb{B}^n \xrightarrow{i} \mathbb{B}),</math> may be used to indicate the adoption of the propositions <math>a_i\!</math> as a basis for describing a universe of discourse.

+

It is important to remember that the coordinate propositions <math>\{a_i\},</math> besides being projection maps <math>a_i : \mathbb{B}^n \to \mathbb{B},</math> are propositions on an equal footing with all others, even though employed as a basis in a particular moment. This set of <math>n</math> propositions may sometimes be referred to as the ''basic propositions'', the ''coordinate propositions'', or the ''simple propositions'' that found a universe of discourse. Either one of the equivalent notations, <math>\{a_i : \mathbb{B}^n \to \mathbb{B}\}</math> or <math>(\mathbb{B}^n \xrightarrow{i} \mathbb{B}),</math> may be used to indicate the adoption of the propositions <math>a_i</math> as a basis for describing a universe of discourse.

−

Among the <math>2^{2^n}</math> propositions in <math>[a_1, \ldots, a_n]</math> are several families of <math>2^n\!</math> propositions each that take on special forms with respect to the basis <math>\{ a_1, \ldots, a_n \}.</math> Three of these families are especially prominent in the present context, the ''linear'', the ''positive'', and the ''singular'' propositions. Each family is naturally parameterized by the coordinate <math>n\!</math>-tuples in <math>\mathbb{B}^n</math> and falls into <math>n + 1\!</math> ranks, with a binomial coefficient <math>\tbinom{n}{k}</math> giving the number of propositions that have rank or weight <math>k.\!</math>

+

Among the <math>2^{2^n}</math> propositions in <math>[a_1, \ldots, a_n]</math> are several families of <math>2^n</math> propositions each that take on special forms with respect to the basis <math>\{ a_1, \ldots, a_n \}.</math> Three of these families are especially prominent in the present context, the ''linear'', the ''positive'', and the ''singular'' propositions. Each family is naturally parameterized by the coordinate <math>n</math>-tuples in <math>\mathbb{B}^n</math> and falls into <math>n + 1</math> ranks, with a binomial coefficient <math>\tbinom{n}{k}</math> giving the number of propositions that have rank or weight <math>k.</math>

<ul>

<li>

−

The ''linear propositions'', <math>\{ \ell : \mathbb{B}^n \to \mathbb{B} \} = (\mathbb{B}^n \xrightarrow{\ell} \mathbb{B}),\!</math> may be written as sums:

+

The ''linear propositions'', <math>\{ \ell : \mathbb{B}^n \to \mathbb{B} \} = (\mathbb{B}^n \xrightarrow{\ell} \mathbb{B}),</math> may be written as sums:

{| align="center" cellpadding="8" width="90%"

Line 387: Line 387:

~\text{where}~

\left\{\begin{matrix} e_i = a_i \\ \text{or} \\ e_i = 0 \end{matrix}\right\}

−

~\text{for}~ i = 1 ~\text{to}~ n.\!</math>

+

~\text{for}~ i = 1 ~\text{to}~ n.</math>

|}

</li>

<li>

−

The ''positive propositions'', <math>\{ p : \mathbb{B}^n \to \mathbb{B} \} = (\mathbb{B}^n \xrightarrow{p} \mathbb{B}),\!</math> may be written as products:

+

The ''positive propositions'', <math>\{ p : \mathbb{B}^n \to \mathbb{B} \} = (\mathbb{B}^n \xrightarrow{p} \mathbb{B}),</math> may be written as products:

{| align="center" cellpadding="8" width="90%"

Line 399: Line 399:

~\text{where}~

\left\{\begin{matrix} e_i = a_i \\ \text{or} \\ e_i = 1 \end{matrix}\right\}

−

~\text{for}~ i = 1 ~\text{to}~ n.\!</math>

+

~\text{for}~ i = 1 ~\text{to}~ n.</math>

|}

</li>

<li>

−

The ''singular propositions'', <math>\{ \mathbf{x} : \mathbb{B}^n \to \mathbb{B} \} = (\mathbb{B}^n \xrightarrow{s} \mathbb{B}),\!</math> may be written as products:

+

The ''singular propositions'', <math>\{ \mathbf{x} : \mathbb{B}^n \to \mathbb{B} \} = (\mathbb{B}^n \xrightarrow{s} \mathbb{B}),</math> may be written as products:

{| align="center" cellpadding="8" width="90%"

Line 411: Line 411:

~\text{where}~

\left\{\begin{matrix} e_i = a_i \\ \text{or} \\ e_i = \texttt{(} a_i \texttt{)} \end{matrix}\right\}

−

~\text{for}~ i = 1 ~\text{to}~ n.\!</math>

+

~\text{for}~ i = 1 ~\text{to}~ n.</math>

|}

</li>

Line 417: Line 417:

</ul>

−

In each case the rank <math>k\!</math> ranges from <math>0\!</math> to <math>n\!</math> and counts the number of positive appearances of the coordinate propositions <math>a_1, \ldots, a_n\!</math> in the resulting expression. For example, for <math>{n = 3},\!</math> the linear proposition of rank <math>0\!</math> is <math>0,\!</math> the positive proposition of rank <math>0\!</math> is <math>1,\!</math> and the singular proposition of rank <math>0\!</math> is <math>\texttt{(} a_1 \texttt{)(} a_2 \texttt{)(} a_3\texttt{)}.\!</math>

+

In each case the rank <math>k</math> ranges from <math>0</math> to <math>n</math> and counts the number of positive appearances of the coordinate propositions <math>a_1, \ldots, a_n</math> in the resulting expression. For example, for <math>{n = 3},</math> the linear proposition of rank <math>0</math> is <math>0,</math> the positive proposition of rank <math>0</math> is <math>1,</math> and the singular proposition of rank <math>0</math> is <math>\texttt{(} a_1 \texttt{)(} a_2 \texttt{)(} a_3\texttt{)}.</math>

The basic propositions <math>a_i : \mathbb{B}^n \to \mathbb{B}</math> are both linear and positive. So these two kinds of propositions, the linear and the positive, may be viewed as two different ways of generalizing the class of basic propositions.

−

Linear propositions and positive propositions are generated by taking boolean sums and products, respectively, over selected subsets of basic propositions, so both families of propositions are parameterized by the powerset <math>\mathcal{P}(\mathcal{I}),</math> that is, the set of all subsets <math>J\!</math> of the basic index set <math>\mathcal{I} = \{1, \ldots, n\}.\!</math>

+

Linear propositions and positive propositions are generated by taking boolean sums and products, respectively, over selected subsets of basic propositions, so both families of propositions are parameterized by the powerset <math>\mathcal{P}(\mathcal{I}),</math> that is, the set of all subsets <math>J</math> of the basic index set <math>\mathcal{I} = \{1, \ldots, n\}.</math>

−

Let us define <math>\mathcal{A}_J</math> as the subset of <math>\mathcal{A}</math> that is given by <math>\{a_i : i \in J\}.\!</math> Then we may comprehend the action of the linear and the positive propositions in the following terms:

+

Let us define <math>\mathcal{A}_J</math> as the subset of <math>\mathcal{A}</math> that is given by <math>\{a_i : i \in J\}.</math> Then we may comprehend the action of the linear and the positive propositions in the following terms:

* The linear proposition <math>\ell_J : \mathbb{B}^n \to \mathbb{B}</math> evaluates each cell <math>\mathbf{x}</math> of <math>\mathbb{B}^n</math> by looking at the coefficients of <math>\mathbf{x}</math> with respect to the features that <math>\ell_J</math> "likes", namely those in <math>\mathcal{A}_J,</math> and then adds them up in <math>\mathbb{B}.</math> Thus, <math>\ell_J(\mathbf{x})</math> computes the parity of the number of features that <math>\mathbf{x}</math> has in <math>\mathcal{A}_J,</math> yielding one for odd and zero for even. Expressed in this idiom, <math>\ell_J(\mathbf{x}) = 1</math> says that <math>\mathbf{x}</math> seems ''odd'' (or ''oddly true'') to <math>\mathcal{A}_J,</math> whereas <math>\ell_J(\mathbf{x}) = 0</math> says that <math>\mathbf{x}</math> seems ''even'' (or ''evenly true'') to <math>\mathcal{A}_J,</math> so long as we recall that ''zero times'' is evenly often, too.

−

* The positive proposition <math>p_J : \mathbb{B}^n \to \mathbb{B}</math> evaluates each cell <math>\mathbf{x}</math> of <math>\mathbb{B}^n</math> by looking at the coefficients of <math>\mathbf{x}</math> with regard to the features that <math>p_J\!</math> "likes", namely those in <math>\mathcal{A}_J,</math> and then takes their product in <math>\mathbb{B}.</math> Thus, <math>p_J(\mathbf{x})</math> assesses the unanimity of the multitude of features that <math>\mathbf{x}</math> has in <math>\mathcal{A}_J,</math> yielding one for all and aught for else. In these consensual or contractual terms, <math>p_J(\mathbf{x}) = 1</math> means that <math>\mathbf{x}</math> is ''AOK'' or congruent with all of the conditions of <math>\mathcal{A}_J,</math> while <math>p_J(\mathbf{x}) = 0</math> means that <math>\mathbf{x}</math> defaults or dissents from some condition of <math>\mathcal{A}_J.</math>

+

* The positive proposition <math>p_J : \mathbb{B}^n \to \mathbb{B}</math> evaluates each cell <math>\mathbf{x}</math> of <math>\mathbb{B}^n</math> by looking at the coefficients of <math>\mathbf{x}</math> with regard to the features that <math>p_J</math> "likes", namely those in <math>\mathcal{A}_J,</math> and then takes their product in <math>\mathbb{B}.</math> Thus, <math>p_J(\mathbf{x})</math> assesses the unanimity of the multitude of features that <math>\mathbf{x}</math> has in <math>\mathcal{A}_J,</math> yielding one for all and aught for else. In these consensual or contractual terms, <math>p_J(\mathbf{x}) = 1</math> means that <math>\mathbf{x}</math> is ''AOK'' or congruent with all of the conditions of <math>\mathcal{A}_J,</math> while <math>p_J(\mathbf{x}) = 0</math> means that <math>\mathbf{x}</math> defaults or dissents from some condition of <math>\mathcal{A}_J.</math>

===Basis Relativity and Type Ambiguity===

Line 433: Line 433:

Finally, two things are important to keep in mind with regard to the simplicity, linearity, positivity, and singularity of propositions.

−

First, all of these properties are relative to a particular basis. For example, a singular proposition with respect to a basis <math>\mathcal{A}</math> will not remain singular if <math>\mathcal{A}</math> is extended by a number of new and independent features. Even if we stick to the original set of pairwise options <math>\{a_i\} \cup \{ \texttt{(} a_i \texttt{)} \}\!</math> to select a new basis, the sets of linear and positive propositions are determined by the choice of simple propositions, and this determination is tantamount to the conventional choice of a cell as origin.

+

First, all of these properties are relative to a particular basis. For example, a singular proposition with respect to a basis <math>\mathcal{A}</math> will not remain singular if <math>\mathcal{A}</math> is extended by a number of new and independent features. Even if we stick to the original set of pairwise options <math>\{a_i\} \cup \{ \texttt{(} a_i \texttt{)} \}</math> to select a new basis, the sets of linear and positive propositions are determined by the choice of simple propositions, and this determination is tantamount to the conventional choice of a cell as origin.

Second, the singular propositions <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B},</math> picking out as they do a single cell or a coordinate tuple <math>\mathbf{x}</math> of <math>\mathbb{B}^n,</math> become the carriers or the vehicles of a certain type-ambiguity that vacillates between the dual forms <math>\mathbb{B}^n</math> and <math>(\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B})</math> and infects the whole hierarchy of types built on them. In other words, the terms that signify the interpretations <math>\mathbf{x} : \mathbb{B}^n</math> and the singular propositions <math>\mathbf{x} : \mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}</math> are fully equivalent in information, and this means that every token of the type <math>\mathbb{B}^n</math> can be reinterpreted as an appearance of the subtype <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}.</math> And vice versa, the two types can be exchanged with each other everywhere that they turn up. In practical terms, this allows the use of singular propositions as a way of denoting points, forming an alternative to coordinate tuples.

−

For example, relative to the universe of discourse <math>[a_1, a_2, a_3]\!</math> the singular proposition <math>a_1 a_2 a_3 : \mathbb{B}^3 \xrightarrow{s} \mathbb{B}</math> could be explicitly retyped as <math>a_1 a_2 a_3 : \mathbb{B}^3</math> to indicate the point <math>(1, 1, 1)\!</math> but in most cases the proper interpretation could be gathered from context. Both notations remain dependent on a particular basis, but the code that is generated under the singular option has the advantage in its self-commenting features, in other words, it constantly reminds us of its basis in the process of denoting points. When the time comes to put a multiplicity of different bases into play, and to search for objects and properties that remain invariant under the transformations between them, this infinitesimal potential advantage may well evolve into an overwhelming practical necessity.

+

For example, relative to the universe of discourse <math>[a_1, a_2, a_3]</math> the singular proposition <math>a_1 a_2 a_3 : \mathbb{B}^3 \xrightarrow{s} \mathbb{B}</math> could be explicitly retyped as <math>a_1 a_2 a_3 : \mathbb{B}^3</math> to indicate the point <math>(1, 1, 1)</math> but in most cases the proper interpretation could be gathered from context. Both notations remain dependent on a particular basis, but the code that is generated under the singular option has the advantage in its self-commenting features, in other words, it constantly reminds us of its basis in the process of denoting points. When the time comes to put a multiplicity of different bases into play, and to search for objects and properties that remain invariant under the transformations between them, this infinitesimal potential advantage may well evolve into an overwhelming practical necessity.

===The Analogy Between Real and Boolean Types===

Line 457: Line 457:

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"

−

|+ style="height:30px" | <math>\text{Table 3.} ~~ \text{Analogy Between Real and Boolean Types}\!</math>

+

|+ style="height:30px" | <math>\text{Table 3.} ~~ \text{Analogy Between Real and Boolean Types}</math>

|- style="height:40px; background:ghostwhite"

−

| <math>\text{Real Domain} ~ \mathbb{R}\!</math>

+

| <math>\text{Real Domain} ~ \mathbb{R}</math>

−

| <math>\longleftrightarrow\!</math>

+

| <math>\longleftrightarrow</math>

−

| <math>\text{Boolean Domain} ~ \mathbb{B}\!</math>

+

| <math>\text{Boolean Domain} ~ \mathbb{B}</math>

|-

−

| <math>\mathbb{R}^n\!</math>

+

| <math>\mathbb{R}^n</math>

−

| <math>\text{Basic Space}\!</math>

+

| <math>\text{Basic Space}</math>

−

| <math>\mathbb{B}^n\!</math>

+

| <math>\mathbb{B}^n</math>

|-

−

| <math>\mathbb{R}^n \to \mathbb{R}\!</math>

+

| <math>\mathbb{R}^n \to \mathbb{R}</math>

−

| <math>\text{Function Space}\!</math>

+

| <math>\text{Function Space}</math>

−

| <math>\mathbb{B}^n \to \mathbb{B}\!</math>

+

| <math>\mathbb{B}^n \to \mathbb{B}</math>

|-

−

| <math>(\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R}\!</math>

+

| <math>(\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R}</math>

−

| <math>\text{Tangent Vector}\!</math>

+

| <math>\text{Tangent Vector}</math>

−

| <math>(\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}\!</math>

+

| <math>(\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math>

|-

−

| <math>\mathbb{R}^n \to ((\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R})\!</math>

+

| <math>\mathbb{R}^n \to ((\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R})</math>

−

| <math>\text{Vector Field}\!</math>

+

| <math>\text{Vector Field}</math>

−

| <math>\mathbb{B}^n \to ((\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B})\!</math>

+

| <math>\mathbb{B}^n \to ((\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B})</math>

|-

−

| <math>(\mathbb{R}^n \times (\mathbb{R}^n \to \mathbb{R})) \to \mathbb{R}\!</math>

+

| <math>(\mathbb{R}^n \times (\mathbb{R}^n \to \mathbb{R})) \to \mathbb{R}</math>

| '''"'''

−

| <math>(\mathbb{B}^n \times (\mathbb{B}^n \to \mathbb{B})) \to \mathbb{B}\!</math>

+

| <math>(\mathbb{B}^n \times (\mathbb{B}^n \to \mathbb{B})) \to \mathbb{B}</math>

|-

−

| <math>((\mathbb{R}^n \to \mathbb{R}) \times \mathbb{R}^n) \to \mathbb{R}\!</math>

+

| <math>((\mathbb{R}^n \to \mathbb{R}) \times \mathbb{R}^n) \to \mathbb{R}</math>

| '''"'''

−

| <math>((\mathbb{B}^n \to \mathbb{B}) \times \mathbb{B}^n) \to \mathbb{B}\!</math>

+

| <math>((\mathbb{B}^n \to \mathbb{B}) \times \mathbb{B}^n) \to \mathbb{B}</math>

|-

−

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^n \to \mathbb{R})~~~\!~~</math>

+

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^n \to \mathbb{R})</math>

−

| <math>\text{Derivation}\!</math>

+

| <math>\text{Derivation}</math>

−

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^n \to \mathbb{B})\!</math>

+

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^n \to \mathbb{B})</math>

|-

−

| <math>\mathbb{R}^n \to \mathbb{R}^m\!</math>

+

| <math>\mathbb{R}^n \to \mathbb{R}^m</math>

| <math>\begin{matrix}\text{Basic}\\[2pt]\text{Transformation}\end{matrix}</math>

−

| <math>\mathbb{B}^n \to \mathbb{B}^m\!</math>

+

| <math>\mathbb{B}^n \to \mathbb{B}^m</math>

|-

−

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^m \to \mathbb{R})\!</math>

+

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^m \to \mathbb{R})</math>

| <math>\begin{matrix}\text{Function}\\[2pt]\text{Transformation}\end{matrix}</math>

−

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})\!</math>

+

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math>

|}

−

The Table exhibits a sample of likely parallels between the real and boolean domains. The central column gives a selection of terminology that is borrowed from differential geometry and extended in its meaning to the logical side of the Table. These are the varieties of spaces that come up when we turn to analyzing the dynamics of processes that pursue their courses through the states of an arbitrary space <math>X.\!</math> Moreover, when it becomes necessary to approach situations of overwhelming dynamic complexity in a succession of qualitative reaches, then the methods of logic that are afforded by the boolean domains, with their declarative means of synthesis and deductive modes of analysis, supply a natural battery of tools for the task.

+

The Table exhibits a sample of likely parallels between the real and boolean domains. The central column gives a selection of terminology that is borrowed from differential geometry and extended in its meaning to the logical side of the Table. These are the varieties of spaces that come up when we turn to analyzing the dynamics of processes that pursue their courses through the states of an arbitrary space <math>X.</math> Moreover, when it becomes necessary to approach situations of overwhelming dynamic complexity in a succession of qualitative reaches, then the methods of logic that are afforded by the boolean domains, with their declarative means of synthesis and deductive modes of analysis, supply a natural battery of tools for the task.

−

It is usually expedient to take these spaces two at a time, in dual pairs of the form <math>X\!</math> and <math>(X \to \mathbb{K}).</math> In general, one creates pairs of type schemas by replacing any space <math>X\!</math> with its dual <math>(X \to \mathbb{K}),</math> for example, pairing the type <math>X \to Y</math> with the type <math>(X \to \mathbb{K}) \to (Y \to \mathbb{K}),</math> and <math>X \times Y</math> with <math>(X \to \mathbb{K}) \times (Y \to \mathbb{K}).</math> The word ''dual'' is used here in its broader sense to mean all of the functionals, not just the linear ones. Given any function <math>f : X \to \mathbb{K},</math> the ''converse'' or inverse relation corresponding to <math>f\!</math> is denoted <math>f^{-1},\!</math> and the subsets of <math>X\!</math> that are defined by <math>f^{-1}(k),\!</math> taken over <math>k\!</math> in <math>\mathbb{K},</math> are called the ''fibers'' or the ''level sets'' of the function <math>f.\!</math>

+

It is usually expedient to take these spaces two at a time, in dual pairs of the form <math>X</math> and <math>(X \to \mathbb{K}).</math> In general, one creates pairs of type schemas by replacing any space <math>X</math> with its dual <math>(X \to \mathbb{K}),</math> for example, pairing the type <math>X \to Y</math> with the type <math>(X \to \mathbb{K}) \to (Y \to \mathbb{K}),</math> and <math>X \times Y</math> with <math>(X \to \mathbb{K}) \times (Y \to \mathbb{K}).</math> The word ''dual'' is used here in its broader sense to mean all of the functionals, not just the linear ones. Given any function <math>f : X \to \mathbb{K},</math> the ''converse'' or inverse relation corresponding to <math>f</math> is denoted <math>f^{-1},</math> and the subsets of <math>X</math> that are defined by <math>f^{-1}(k),</math> taken over <math>k</math> in <math>\mathbb{K},</math> are called the ''fibers'' or the ''level sets'' of the function <math>f.</math>

===Theory of Control and Control of Theory===

Line 519: Line 519:

|}

−

In the boolean context a function <math>f : X \to \mathbb{B}</math> is tantamount to a ''proposition'' about elements of <math>X,\!</math> and the elements of <math>X\!</math> constitute the ''interpretations'' of that proposition. The fiber <math>f^{-1}(1)\!</math> comprises the set of ''models'' of <math>f,\!</math> or examples of elements in <math>X\!</math> satisfying the proposition <math>f.\!</math> The fiber <math>f^{-1}(0)\!</math> collects the complementary set of ''anti-models'', or the exceptions to the proposition <math>f\!</math> that exist in <math>X.\!</math> Of course, the space of functions <math>(X \to \mathbb{B})\!</math> is isomorphic to the set of all subsets of <math>X,\!</math> called the ''power set'' of <math>X,\!</math> and often denoted <math>\mathcal{P}(X)</math> or <math>2^X.\!</math>

+

In the boolean context a function <math>f : X \to \mathbb{B}</math> is tantamount to a ''proposition'' about elements of <math>X,</math> and the elements of <math>X</math> constitute the ''interpretations'' of that proposition. The fiber <math>f^{-1}(1)</math> comprises the set of ''models'' of <math>f,</math> or examples of elements in <math>X</math> satisfying the proposition <math>f.</math> The fiber <math>f^{-1}(0)</math> collects the complementary set of ''anti-models'', or the exceptions to the proposition <math>f</math> that exist in <math>X.</math> Of course, the space of functions <math>(X \to \mathbb{B})</math> is isomorphic to the set of all subsets of <math>X,</math> called the ''power set'' of <math>X,</math> and often denoted <math>\mathcal{P}(X)</math> or <math>2^X.</math>

−

The operation of replacing <math>X\!</math> by <math>(X \to \mathbb{B})\!</math> in a type schema corresponds to a certain shift of attitude towards the space <math>X,\!</math> in which one passes from a focus on the ostensibly individual elements of <math>X\!</math> to a concern with the states of information and uncertainty that one possesses about objects and situations in <math>X.\!</math> The conceptual obstacles in the path of this transition can be smoothed over by using singular functions <math>(\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B})</math> as stepping stones. First of all, it's an easy step from an element <math>\mathbf{x}</math> of type <math>\mathbb{B}^n</math> to the equivalent information of a singular proposition <math>\mathbf{x} : X \xrightarrow{s} \mathbb{B}, </math> and then only a small jump of generalization remains to reach the type of an arbitrary proposition <math>f : X \to \mathbb{B},</math> perhaps understood to indicate a relaxed constraint on the singularity of points or a neighborhood circumscribing the original <math>\mathbf{x}.</math> This is frequently a useful transformation, communicating between the ''objective'' and the ''intentional'' perspectives, in spite perhaps of the open objection that this distinction is transient in the mean time and ultimately superficial.

+

The operation of replacing <math>X</math> by <math>(X \to \mathbb{B})</math> in a type schema corresponds to a certain shift of attitude towards the space <math>X,</math> in which one passes from a focus on the ostensibly individual elements of <math>X</math> to a concern with the states of information and uncertainty that one possesses about objects and situations in <math>X.</math> The conceptual obstacles in the path of this transition can be smoothed over by using singular functions <math>(\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B})</math> as stepping stones. First of all, it's an easy step from an element <math>\mathbf{x}</math> of type <math>\mathbb{B}^n</math> to the equivalent information of a singular proposition <math>\mathbf{x} : X \xrightarrow{s} \mathbb{B}, </math> and then only a small jump of generalization remains to reach the type of an arbitrary proposition <math>f : X \to \mathbb{B},</math> perhaps understood to indicate a relaxed constraint on the singularity of points or a neighborhood circumscribing the original <math>\mathbf{x}.</math> This is frequently a useful transformation, communicating between the ''objective'' and the ''intentional'' perspectives, in spite perhaps of the open objection that this distinction is transient in the mean time and ultimately superficial.

It is hoped that this measure of flexibility, allowing us to stretch a point into a proposition, can be useful in the examination of inquiry driven systems, where the differences between empirical, intentional, and theoretical propositions constitute the discrepancies and the distributions that drive experimental activity. I can give this model of inquiry a cybernetic cast by realizing that theory change and theory evolution, as well as the choice and the evaluation of experiments, are actions that are taken by a system or its agent in response to the differences that are detected between observational contents and theoretical coverage.

Line 534: Line 534:

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"

−

|+ style="height:30px" | <math>\text{Table 3.} ~~ \text{Analogy Between Real and Boolean Types}\!</math>

+

|+ style="height:30px" | <math>\text{Table 3.} ~~ \text{Analogy Between Real and Boolean Types}</math>

|- style="height:40px; background:ghostwhite"

−

| <math>\text{Real Domain} ~ \mathbb{R}\!</math>

+

| <math>\text{Real Domain} ~ \mathbb{R}</math>

−

| <math>\longleftrightarrow\!</math>

+

| <math>\longleftrightarrow</math>

−

| <math>\text{Boolean Domain} ~ \mathbb{B}\!</math>

+

| <math>\text{Boolean Domain} ~ \mathbb{B}</math>

|-

−

| <math>\mathbb{R}^n\!</math>

+

| <math>\mathbb{R}^n</math>

−

| <math>\text{Basic Space}\!</math>

+

| <math>\text{Basic Space}</math>

−

| <math>\mathbb{B}^n\!</math>

+

| <math>\mathbb{B}^n</math>

|-

−

| <math>\mathbb{R}^n \to \mathbb{R}\!</math>

+

| <math>\mathbb{R}^n \to \mathbb{R}</math>

−

| <math>\text{Function Space}\!</math>

+

| <math>\text{Function Space}</math>

−

| <math>\mathbb{B}^n \to \mathbb{B}\!</math>

+

| <math>\mathbb{B}^n \to \mathbb{B}</math>

|-

−

| <math>(\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R}\!</math>

+

| <math>(\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R}</math>

−

| <math>\text{Tangent Vector}\!</math>

+

| <math>\text{Tangent Vector}</math>

−

| <math>(\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}\!</math>

+

| <math>(\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math>

|-

−

| <math>\mathbb{R}^n \to ((\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R})\!</math>

+

| <math>\mathbb{R}^n \to ((\mathbb{R}^n \to \mathbb{R}) \to \mathbb{R})</math>

−

| <math>\text{Vector Field}\!</math>

+

| <math>\text{Vector Field}</math>

−

| <math>\mathbb{B}^n \to ((\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B})\!</math>

+

| <math>\mathbb{B}^n \to ((\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B})</math>

|-

−

| <math>(\mathbb{R}^n \times (\mathbb{R}^n \to \mathbb{R})) \to \mathbb{R}\!</math>

+

| <math>(\mathbb{R}^n \times (\mathbb{R}^n \to \mathbb{R})) \to \mathbb{R}</math>

| '''"'''

−

| <math>(\mathbb{B}^n \times (\mathbb{B}^n \to \mathbb{B})) \to \mathbb{B}\!</math>

+

| <math>(\mathbb{B}^n \times (\mathbb{B}^n \to \mathbb{B})) \to \mathbb{B}</math>

|-

−

| <math>((\mathbb{R}^n \to \mathbb{R}) \times \mathbb{R}^n) \to \mathbb{R}\!</math>

+

| <math>((\mathbb{R}^n \to \mathbb{R}) \times \mathbb{R}^n) \to \mathbb{R}</math>

| '''"'''

−

| <math>((\mathbb{B}^n \to \mathbb{B}) \times \mathbb{B}^n) \to \mathbb{B}\!</math>

+

| <math>((\mathbb{B}^n \to \mathbb{B}) \times \mathbb{B}^n) \to \mathbb{B}</math>

|-

−

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^n \to \mathbb{R})~~~\!~~</math>

+

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^n \to \mathbb{R})</math>

−

| <math>\text{Derivation}\!</math>

+

| <math>\text{Derivation}</math>

−

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^n \to \mathbb{B})\!</math>

+

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^n \to \mathbb{B})</math>

|-

−

| <math>\mathbb{R}^n \to \mathbb{R}^m\!</math>

+

| <math>\mathbb{R}^n \to \mathbb{R}^m</math>

| <math>\begin{matrix}\text{Basic}\\[2pt]\text{Transformation}\end{matrix}</math>

−

| <math>\mathbb{B}^n \to \mathbb{B}^m\!</math>

+

| <math>\mathbb{B}^n \to \mathbb{B}^m</math>

|-

−

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^m \to \mathbb{R})\!</math>

+

| <math>(\mathbb{R}^n \to \mathbb{R}) \to (\mathbb{R}^m \to \mathbb{R})</math>

| <math>\begin{matrix}\text{Function}\\[2pt]\text{Transformation}\end{matrix}</math>

−

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})\!</math>

+

| <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math>

|}

−

First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math> At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an <math>f\!</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math> This value is known as the ''derivative'' of <math>f\!</math> in the direction <math>\vartheta\!</math> [Che46, 76–77]. In the boolean case <math>\vartheta : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type.

+

First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math> At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta</math> takes a function on that space, an <math>f</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math> This value is known as the ''derivative'' of <math>f</math> in the direction <math>\vartheta</math> [Che46, 76–77]. In the boolean case <math>\vartheta : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type.

−

Next, by way of illustrating the propositions as types idea, consider a proposition of the form <math>X \Rightarrow (Y \Rightarrow Z).</math> One knows from propositional calculus that this is logically equivalent to a proposition of the form <math>(X \land Y) \Rightarrow Z.</math> But this equivalence should remind us of the functional isomorphism that exists between a construction of the type <math>X \to (Y \to Z)</math> and a construction of the type <math>(X \times Y) \to Z.</math> The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows “<math>\to~~~\!~~</math>” and products “<math>\times\!</math>” with the respective logical arrows “<math>\Rightarrow\!</math>” and products “<math>\land\!</math>”. Accordingly, viewing the result as a proposition, we can employ axioms and theorems of propositional calculus to suggest appropriate isomorphisms among the categorical and functional constructions.

+

Next, by way of illustrating the propositions as types idea, consider a proposition of the form <math>X \Rightarrow (Y \Rightarrow Z).</math> One knows from propositional calculus that this is logically equivalent to a proposition of the form <math>(X \land Y) \Rightarrow Z.</math> But this equivalence should remind us of the functional isomorphism that exists between a construction of the type <math>X \to (Y \to Z)</math> and a construction of the type <math>(X \times Y) \to Z.</math> The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows “<math>\to</math>” and products “<math>\times</math>” with the respective logical arrows “<math>\Rightarrow</math>” and products “<math>\land</math>”. Accordingly, viewing the result as a proposition, we can employ axioms and theorems of propositional calculus to suggest appropriate isomorphisms among the categorical and functional constructions.

−

Finally, examine the middle four rows of Table 3. These display a series of isomorphic types that stretch from the categories that are labeled ''Vector Field'' to those that are labeled ''Derivation''. A ''vector field'', also known as an ''infinitesimal transformation'', associates a tangent vector at a point with each point of a space. In symbols, a vector field is a function of the form <math>\textstyle \xi : X \to \bigcup_{x \in X} \xi_x\!</math> that assigns to each point <math>x\!</math> of the space <math>X\!</math> a tangent vector to <math>X\!</math> at that point, namely, the tangent vector <math>\xi_x\!</math> [Che46, 82–83]. If <math>X\!</math> is of the type <math>\mathbb{K}^n,</math> then <math>\xi\!</math> is of the type <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K}).</math> This has the pattern <math>X \to (Y \to Z),</math> with <math>X = \mathbb{K}^n,</math> <math>Y = (\mathbb{K}^n \to \mathbb{K}),</math> and <math>Z = \mathbb{K}.</math>

+

Finally, examine the middle four rows of Table 3. These display a series of isomorphic types that stretch from the categories that are labeled ''Vector Field'' to those that are labeled ''Derivation''. A ''vector field'', also known as an ''infinitesimal transformation'', associates a tangent vector at a point with each point of a space. In symbols, a vector field is a function of the form <math>\textstyle \xi : X \to \bigcup_{x \in X} \xi_x</math> that assigns to each point <math>x</math> of the space <math>X</math> a tangent vector to <math>X</math> at that point, namely, the tangent vector <math>\xi_x</math> [Che46, 82–83]. If <math>X</math> is of the type <math>\mathbb{K}^n,</math> then <math>\xi</math> is of the type <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K}).</math> This has the pattern <math>X \to (Y \to Z),</math> with <math>X = \mathbb{K}^n,</math> <math>Y = (\mathbb{K}^n \to \mathbb{K}),</math> and <math>Z = \mathbb{K}.</math>

−

Applying the propositions as types analogy, one can follow this pattern through a series of metamorphoses from the type of a vector field to the type of a derivation, as traced out in Table 4. Observe how the function <math>f : X \to \mathbb{K},</math> associated with the place of <math>Y\!</math> in the pattern, moves through its paces from the second to the first position. In this way, the vector field <math>\xi,\!</math> initially viewed as attaching each tangent vector <math>\xi_x\!</math> to the site <math>x\!</math> where it acts in <math>X,\!</math> now comes to be seen as acting on each scalar potential <math>f : X \to \mathbb{K}</math> like a generalized species of differentiation, producing another function <math>\xi f : X \to \mathbb{K}</math> of the same type.

+

Applying the propositions as types analogy, one can follow this pattern through a series of metamorphoses from the type of a vector field to the type of a derivation, as traced out in Table 4. Observe how the function <math>f : X \to \mathbb{K},</math> associated with the place of <math>Y</math> in the pattern, moves through its paces from the second to the first position. In this way, the vector field <math>\xi,</math> initially viewed as attaching each tangent vector <math>\xi_x</math> to the site <math>x</math> where it acts in <math>X,</math> now comes to be seen as acting on each scalar potential <math>f : X \to \mathbb{K}</math> like a generalized species of differentiation, producing another function <math>\xi f : X \to \mathbb{K}</math> of the same type.

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"

−

|+ style="height:30px" | <math>\text{Table 4.} ~~ \text{An Equivalence Based on the Propositions as Types Analogy}\!</math>

+

|+ style="height:30px" | <math>\text{Table 4.} ~~ \text{An Equivalence Based on the Propositions as Types Analogy}</math>

|- style="height:40px; background:ghostwhite"

−

| <math>\text{Pattern}\!</math>

+

| <math>\text{Pattern}</math>

−

| <math>\text{Construct}\!</math>

+

| <math>\text{Construct}</math>

−

| <math>\text{Instance}\!</math>

+

| <math>\text{Instance}</math>

|-

−

| <math>X \to (Y \to Z)\!</math>

+

| <math>X \to (Y \to Z)</math>

−

| <math>\text{Vector Field}\!</math>

+

| <math>\text{Vector Field}</math>

−

| <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K})\!</math>

+

| <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K})</math>

|-

−

| <math>(X \times Y) \to Z\!</math>

+

| <math>(X \times Y) \to Z</math>

−

| <math>\Uparrow\!</math>

+

| <math>\Uparrow</math>

−

| <math>(\mathbb{K}^n \times (\mathbb{K}^n \to \mathbb{K})) \to \mathbb{K}\!</math>

+

| <math>(\mathbb{K}^n \times (\mathbb{K}^n \to \mathbb{K})) \to \mathbb{K}</math>

|-

−

| <math>(Y \times X) \to Z\!</math>

+

| <math>(Y \times X) \to Z</math>

−

| <math>\Downarrow\!</math>

+

| <math>\Downarrow</math>

−

| <math>((\mathbb{K}^n \to \mathbb{K}) \times \mathbb{K}^n) \to \mathbb{K}\!</math>

+

| <math>((\mathbb{K}^n \to \mathbb{K}) \times \mathbb{K}^n) \to \mathbb{K}</math>

|-

−

| <math>Y \to (X \to Z)\!</math>

+

| <math>Y \to (X \to Z)</math>

−

| <math>\text{Derivation}\!</math>

+

| <math>\text{Derivation}</math>

−

| <math>(\mathbb{K}^n \to \mathbb{K}) \to (\mathbb{K}^n \to \mathbb{K})\!</math>

+

| <math>(\mathbb{K}^n \to \mathbb{K}) \to (\mathbb{K}^n \to \mathbb{K})</math>

|}

Line 631: Line 631:

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:left; width:75%"

−

|+ style="height:30px" | <math>\text{Table 5.} ~~ \text{A Bridge Over Troubled Waters}\!</math>

+

|+ style="height:30px" | <math>\text{Table 5.} ~~ \text{A Bridge Over Troubled Waters}</math>

|- style="height:40px; background:ghostwhite"

−

| align="center" | <math>\text{Linear Space}\!</math>

+

| align="center" | <math>\text{Linear Space}</math>

−

| align="center" | <math>\text{Liminal Space}\!</math>

+

| align="center" | <math>\text{Liminal Space}</math>

−

| align="center" | <math>\text{Logical Space}\!</math>

+

| align="center" | <math>\text{Logical Space}</math>

|-

| <math>\begin{matrix}\mathcal{X} & = & \{ x_1, \ldots, x_n \}\end{matrix}</math>

Line 805: Line 805:

−

The left side of the Table collects mostly standard notation for an <math>n\!</math>-dimensional vector space over a field <math>\mathbb{K}.</math> The right side of the table repeats the first elements of a notation that I sketched above, to be used in further developments of propositional calculus. (I plan to use this notation in the logical analysis of neural network systems.) The middle column of the table is designed as a transitional step from the case of an arbitrary field <math>\mathbb{K},</math> with a special interest in the continuous line <math>\mathbb{R},</math> to the qualitative and discrete situations that are instanced and typified by <math>\mathbb{B}.</math>

+

The left side of the Table collects mostly standard notation for an <math>n</math>-dimensional vector space over a field <math>\mathbb{K}.</math> The right side of the table repeats the first elements of a notation that I sketched above, to be used in further developments of propositional calculus. (I plan to use this notation in the logical analysis of neural network systems.) The middle column of the table is designed as a transitional step from the case of an arbitrary field <math>\mathbb{K},</math> with a special interest in the continuous line <math>\mathbb{R},</math> to the qualitative and discrete situations that are instanced and typified by <math>\mathbb{B}.</math>

I now proceed to explain these concepts in more detail. The most important ideas developed in Table 5 are these:

Line 813: Line 813:

* The idea of passing from a more complex universe to a simpler universe by a process of ''thresholding'' each dimension of variation down to a single bit of information.

−

For the sake of concreteness, let us suppose that we start with a continuous <math>n\!</math>-dimensional vector space like <math>X = \langle x_1, \ldots, x_n \rangle \cong \mathbb{R}^n.</math> The coordinate system <math>\mathcal{X} = \{x_i\}</math> is a set of maps <math>x_i : \mathbb{R}^n \to \mathbb{R},</math> also known as the ''coordinate projections''. Given a "dataset" of points <math>\mathbf{x}</math> in <math>\mathbb{R}^n,</math> there are numerous ways of sensibly reducing the data down to one bit for each dimension. One strategy that is general enough for our present purposes is as follows. For each <math>i\!</math> we choose an <math>n\!</math>-ary relation <math>L_i\!</math> on <math>\mathbb{R}^n,</math> that is, a subset of <math>\mathbb{R}^n,</math> and then we define the <math>i^\mathrm{th}\!</math> threshold map, or ''limen'' <math>\underline{x}_i</math> as follows:

+

For the sake of concreteness, let us suppose that we start with a continuous <math>n</math>-dimensional vector space like <math>X = \langle x_1, \ldots, x_n \rangle \cong \mathbb{R}^n.</math> The coordinate system <math>\mathcal{X} = \{x_i\}</math> is a set of maps <math>x_i : \mathbb{R}^n \to \mathbb{R},</math> also known as the ''coordinate projections''. Given a "dataset" of points <math>\mathbf{x}</math> in <math>\mathbb{R}^n,</math> there are numerous ways of sensibly reducing the data down to one bit for each dimension. One strategy that is general enough for our present purposes is as follows. For each <math>i</math> we choose an <math>n</math>-ary relation <math>L_i</math> on <math>\mathbb{R}^n,</math> that is, a subset of <math>\mathbb{R}^n,</math> and then we define the <math>i^\mathrm{th}</math> threshold map, or ''limen'' <math>\underline{x}_i</math> as follows:

{| align="center" cellpadding="8" width="90%"

−

| <math>\underline{x}_i : \mathbb{R}^n \to \mathbb{B}\ \text{such that:}\!</math>

+

| <math>\underline{x}_i : \mathbb{R}^n \to \mathbb{B}\ \text{such that:}</math>

|-

|

Line 826: Line 826:

|}

−

In other notations that are sometimes used, the operator <math>\chi (\ldots)</math> or the corner brackets <math>\lceil\ldots\rceil</math> can be used to denote a ''characteristic function'', that is, a mapping from statements to their truth values in <math>\mathbb{B}.</math> Finally, it is not uncommon to use the name of the relation itself as a predicate that maps <math>n\!</math>-tuples into truth values. Thus we have the following notational variants of the above definition:

+

In other notations that are sometimes used, the operator <math>\chi (\ldots)</math> or the corner brackets <math>\lceil\ldots\rceil</math> can be used to denote a ''characteristic function'', that is, a mapping from statements to their truth values in <math>\mathbb{B}.</math> Finally, it is not uncommon to use the name of the relation itself as a predicate that maps <math>n</math>-tuples into truth values. Thus we have the following notational variants of the above definition:

{| align="center" cellpadding="8" width="90%"

Line 835: Line 835:

|}

−

Notice that, as defined here, there need be no actual relation between the <math>n\!</math>-dimensional subsets <math>\{L_i\}\!</math> and the coordinate axes corresponding to <math>\{x_i\},\!</math> aside from the circumstance that the two sets have the same cardinality. In concrete cases, though, one usually has some reason for associating these "volumes" with these "lines", for instance, <math>L_i\!</math> is bounded by some hyperplane that intersects the <math>i^\text{th}\!</math> axis at a unique threshold value <math>r_i \in \mathbb{R}.\!</math> Often, the hyperplane is chosen normal to the axis. In recognition of this motive, let us make the following convention. When the set <math>L_i\!</math> has points on the <math>i^\text{th}\!</math> axis, that is, points of the form <math>(0, \ldots, 0, r_i, 0, \ldots, 0)</math> where only the <math>x_i\!</math> coordinate is possibly non-zero, we may pick any one of these coordinate values as a parametric index of the relation. In this case we say that the indexing is ''real'', otherwise the indexing is ''imaginary''. For a knowledge based system <math>X,\!</math> this should serve once again to mark the distinction between ''acquaintance'' and ''opinion''.

+

Notice that, as defined here, there need be no actual relation between the <math>n</math>-dimensional subsets <math>\{L_i\}</math> and the coordinate axes corresponding to <math>\{x_i\},</math> aside from the circumstance that the two sets have the same cardinality. In concrete cases, though, one usually has some reason for associating these "volumes" with these "lines", for instance, <math>L_i</math> is bounded by some hyperplane that intersects the <math>i^\text{th}</math> axis at a unique threshold value <math>r_i \in \mathbb{R}.</math> Often, the hyperplane is chosen normal to the axis. In recognition of this motive, let us make the following convention. When the set <math>L_i</math> has points on the <math>i^\text{th}</math> axis, that is, points of the form <math>(0, \ldots, 0, r_i, 0, \ldots, 0)</math> where only the <math>x_i</math> coordinate is possibly non-zero, we may pick any one of these coordinate values as a parametric index of the relation. In this case we say that the indexing is ''real'', otherwise the indexing is ''imaginary''. For a knowledge based system <math>X,</math> this should serve once again to mark the distinction between ''acquaintance'' and ''opinion''.

−

States of knowledge about the location of a system or about the distribution of a population of systems in a state space <math>X = \mathbb{R}^n</math> can now be expressed by taking the set <math>\underline{\mathcal{X}} = \{\underline{x}_i\}</math> as a basis of logical features. In picturesque terms, one may think of the underscore and the subscript as combining to form a subtextual spelling for the <math>i^\text{th}\!</math> threshold map. This can help to remind us that the ''threshold operator'' <math>(\underline{~})_i</math> acts on <math>\mathbf{x}</math> by setting up a kind of a “hurdle” for it. In this interpretation the coordinate proposition <math>\underline{x}_i</math> asserts that the representative point <math>\mathbf{x}</math> resides ''above'' the <math>i^\mathrm{th}\!</math> threshold.

+

States of knowledge about the location of a system or about the distribution of a population of systems in a state space <math>X = \mathbb{R}^n</math> can now be expressed by taking the set <math>\underline{\mathcal{X}} = \{\underline{x}_i\}</math> as a basis of logical features. In picturesque terms, one may think of the underscore and the subscript as combining to form a subtextual spelling for the <math>i^\text{th}</math> threshold map. This can help to remind us that the ''threshold operator'' <math>(\underline{~})_i</math> acts on <math>\mathbf{x}</math> by setting up a kind of a “hurdle” for it. In this interpretation the coordinate proposition <math>\underline{x}_i</math> asserts that the representative point <math>\mathbf{x}</math> resides ''above'' the <math>i^\mathrm{th}</math> threshold.

−

Primitive assertions of the form <math>\underline{x}_i (\mathbf{x})</math> may then be negated and joined by means of propositional connectives in the usual ways to provide information about the state <math>\mathbf{x}</math> of a contemplated system or a statistical ensemble of systems. Parentheses <math>\texttt{(} \ldots \texttt{)}\!</math> may be used to indicate logical negation. Eventually one discovers the usefulness of the <math>k\!</math>-ary ''just one false'' operators of the form <math>\texttt{(} a_1 \texttt{,} \ldots \texttt{,} a_k \texttt{)},\!</math> as treated in earlier reports. This much tackle generates a space of points (cells, interpretations), <math>\underline{X} \cong \mathbb{B}^n,</math> and a space of functions (regions, propositions), <math>\underline{X}^\uparrow \cong (\mathbb{B}^n \to \mathbb{B}).</math> Together these form a new universe of discourse <math>\underline{X}^\bullet</math> of the type <math>(\mathbb{B}^n, (\mathbb{B}^n \to \mathbb{B})),</math> which we may abbreviate as <math>\mathbb{B}^n\ +\!\to \mathbb{B}</math> or most succinctly as <math>[\mathbb{B}^n].</math>

+

Primitive assertions of the form <math>\underline{x}_i (\mathbf{x})</math> may then be negated and joined by means of propositional connectives in the usual ways to provide information about the state <math>\mathbf{x}</math> of a contemplated system or a statistical ensemble of systems. Parentheses <math>\texttt{(} \ldots \texttt{)}</math> may be used to indicate logical negation. Eventually one discovers the usefulness of the <math>k</math>-ary ''just one false'' operators of the form <math>\texttt{(} a_1 \texttt{,} \ldots \texttt{,} a_k \texttt{)},</math> as treated in earlier reports. This much tackle generates a space of points (cells, interpretations), <math>\underline{X} \cong \mathbb{B}^n,</math> and a space of functions (regions, propositions), <math>\underline{X}^\uparrow \cong (\mathbb{B}^n \to \mathbb{B}).</math> Together these form a new universe of discourse <math>\underline{X}^\bullet</math> of the type <math>(\mathbb{B}^n, (\mathbb{B}^n \to \mathbb{B})),</math> which we may abbreviate as <math>\mathbb{B}^n\ +\!\to \mathbb{B}</math> or most succinctly as <math>[\mathbb{B}^n].</math>

The square brackets have been chosen to recall the rectangular frame of a venn diagram. In thinking about a universe of discourse it is a good idea to keep this picture in mind, graphically illustrating the links among the elementary cells <math>\underline{\mathbf{x}},</math> the defining features <math>\underline{x}_i,</math> and the potential shadings <math>f : \underline{X} \to \mathbb{B}</math> all at the same time, not to mention the arbitrariness of the way we choose to inscribe our distinctions in the medium of a continuous space.

−

Finally, let <math>X^*\!</math> denote the space of linear functions, <math>(\ell : X \to \mathbb{K}),</math> which has in the finite case the same dimensionality as <math>X,\!</math> and let the same notation be extended across the Table.

+

Finally, let <math>X^*</math> denote the space of linear functions, <math>(\ell : X \to \mathbb{K}),</math> which has in the finite case the same dimensionality as <math>X,</math> and let the same notation be extended across the Table.

We have just gone through a lot of work, apparently doing nothing more substantial than spinning a complex spell of notational devices through a labyrinth of baffled spaces and baffling maps. The reason for doing this was to bind together and to constitute the intuitive concept of a universe of discourse into a coherent categorical object, the kind of thing, once grasped, that can be turned over in the mind and considered in all its manifold changes and facets. The effort invested in these preliminary measures is intended to pay off later, when we need to consider the state transformations and the time evolution of neural network systems.

Line 858: Line 858:

|}

−

To prepare for the next phase of discussion, Tables 6 and 7 collect and summarize all of the propositional forms on one and two variables. These propositional forms are represented over bases of boolean variables as complete sets of boolean-valued functions. Adjacent to their names and specifications are listed what are roughly the simplest expressions in the ''[[cactus language]]'', the particular syntax for propositional calculus that I use in formal and computational contexts. For the sake of orientation, the English paraphrases and the more common notations are listed in the last two columns. As simple and circumscribed as these low-dimensional universes may appear to be, a careful exploration of their differential extensions will involve us in complexities sufficient to demand our attention for some time to come.

+

To prepare for the next phase of discussion, Tables 6 and 7 collect and summarize all of the propositional forms on one and two variables. These propositional forms are represented over bases of boolean variables as complete sets of boolean-valued functions. Adjacent to their names and specifications are listed what are roughly the simplest expressions in the ''[[Cactus_Language_•_Overview|cactus language]]'', the particular syntax for propositional calculus that I use in formal and computational contexts. For the sake of orientation, the English paraphrases and the more common notations are listed in the last two columns. As simple and circumscribed as these low-dimensional universes may appear to be, a careful exploration of their differential extensions will involve us in complexities sufficient to demand our attention for some time to come.

−

Propositional forms on one variable correspond to boolean functions <math>f : \mathbb{B}^1 \to \mathbb{B}.</math> In Table 6 these functions are listed in a variant form of [[truth table]], one in which the axes of the usual arrangement are rotated through a right angle. Each function <math>f_i\!</math> is indexed by the string of values that it takes on the points of the universe <math>X^\bullet = [x] \cong \mathbb{B}^1.</math> The binary index generated in this way is converted to its decimal equivalent and these are used as conventional names for the <math>f_i,\!</math> as shown in the first column of the Table. In their own right the <math>2^1\!</math> points of the universe <math>X^\bullet</math> are coordinated as a space of type <math>\mathbb{B}^1,</math> this in light of the universe <math>X^\bullet</math> being a functional domain where the coordinate projection <math>x\!</math> takes on its values in <math>\mathbb{B}.</math>

+

Propositional forms on one variable correspond to boolean functions <math>f : \mathbb{B}^1 \to \mathbb{B}.</math> In Table 6 these functions are listed in a variant form of [[truth table]], one in which the axes of the usual arrangement are rotated through a right angle. Each function <math>f_i</math> is indexed by the string of values that it takes on the points of the universe <math>X^\bullet = [x] \cong \mathbb{B}^1.</math> The binary index generated in this way is converted to its decimal equivalent and these are used as conventional names for the <math>f_i,</math> as shown in the first column of the Table. In their own right the <math>2^1</math> points of the universe <math>X^\bullet</math> are coordinated as a space of type <math>\mathbb{B}^1,</math> this in light of the universe <math>X^\bullet</math> being a functional domain where the coordinate projection <math>x</math> takes on its values in <math>\mathbb{B}.</math>

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"

−

|+ style="height:30px" | <math>\text{Table 6.} ~~ \text{Propositional Forms on One Variable}\!</math>

+

|+ style="height:30px" | <math>\text{Table 6.} ~~ \text{Propositional Forms on One Variable}</math>

|- style="height:40px; background:ghostwhite"

| style="width:16%" | <math>\begin{matrix}\mathcal{L}_1 \\ \text{Decimal}\end{matrix}</math>

Line 875: Line 875:

|- style="background:ghostwhite"

|  

−

| align="right" | <math>x\colon\!</math>

+

| align="right" | <math>x\colon</math>

−

| <math>1~0\!</math>

+

| <math>1~0</math>

|  

|-

−

| <math>f_0\!</math>

+

| <math>f_0</math>

−

| <math>f_{00}\!</math>

+

| <math>f_{00}</math>

−

| <math>0~0\!</math>

+

| <math>0~0</math>

−

| <math>\texttt{(~)}\!</math>

+

| <math>\texttt{(} ~ \texttt{)}</math>

−

| <math>\text{false}\!</math>

+

| <math>\text{false}</math>

−

| <math>0\!</math>

+

| <math>0</math>

|-

−

| <math>f_1\!</math>

+

| <math>f_1</math>

−

| <math>f_{01}\!</math>

+

| <math>f_{01}</math>

−

| <math>0~1\!</math>

+

| <math>0~1</math>

−

| <math>\texttt{(} x \texttt{)}\!</math>

+

| <math>\texttt{(} x \texttt{)}</math>

−

| <math>\text{not}~ x\!</math>

+

| <math>\text{not}~ x</math>

−

| <math>\lnot x\!</math>

+

| <math>\lnot x</math>

|-

−

| <math>f_2\!</math>

+

| <math>f_2</math>

−

| <math>f_{10}\!</math>

+

| <math>f_{10}</math>

−

| <math>1~0\!</math>

+

| <math>1~0</math>

−

| <math>x\!</math>

+

| <math>x</math>

−

| <math>x\!</math>

+

| <math>x</math>

−

| <math>x\!</math>

+

| <math>x</math>

|-

−

| <math>f_3\!</math>

+

| <math>f_3</math>

−

| <math>f_{11}\!</math>

+

| <math>f_{11}</math>

−

| <math>1~1\!</math>

+

| <math>1~1</math>

−

| <math>\texttt{((~))}\!</math>

+

| <math>\texttt{((} ~ \texttt{))}</math>

−

| <math>\text{true}\!</math>

+

| <math>\text{true}</math>

−

| <math>1\!</math>

+

| <math>1</math>

|}

−

Propositional forms on two variables correspond to boolean functions <math>f : \mathbb{B}^2 \to \mathbb{B}.</math> In Table 7 each function <math>f_i\!</math> is indexed by the values that it takes on the points of the universe <math>X^\bullet = [x, y] \cong \mathbb{B}^2.</math> Converting the binary index thus generated to a decimal equivalent, we obtain the functional nicknames that are listed in the first column. The <math>2^2\!</math> points of the universe <math>X^\bullet</math> are coordinated as a space of type <math>\mathbb{B}^2,</math> as indicated under the heading of the Table, where the coordinate projections <math>x\!</math> and <math>y\!</math> run through the various combinations of their values in <math>\mathbb{B}.</math>

+

Propositional forms on two variables correspond to boolean functions <math>f : \mathbb{B}^2 \to \mathbb{B}.</math> In Table 7 each function <math>f_i</math> is indexed by the values that it takes on the points of the universe <math>X^\bullet = [x, y] \cong \mathbb{B}^2.</math> Converting the binary index thus generated to a decimal equivalent, we obtain the functional nicknames that are listed in the first column. The <math>2^2</math> points of the universe <math>X^\bullet</math> are coordinated as a space of type <math>\mathbb{B}^2,</math> as indicated under the heading of the Table, where the coordinate projections <math>x</math> and <math>y</math> run through the various combinations of their values in <math>\mathbb{B}.</math>

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"

−

|+ style="height:30px" | <math>\text{Table 7-a.} ~~ \text{Propositional Forms on Two Variables}\!</math>

+

|+ style="height:30px" | <math>\text{Table 7-a.} ~~ \text{Propositional Forms on Two Variables}</math>

|- style="height:40px; background:ghostwhite"

−

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_1 \\ \text{Decimal}\end{matrix}\!</math>

+

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_1 \\ \text{Decimal}\end{matrix}</math>

−

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_2 \\ \text{Binary}\end{matrix}\!</math>

+

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_2 \\ \text{Binary}\end{matrix}</math>

−

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_3 \\ \text{Vector}\end{matrix}\!</math>

+

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_3 \\ \text{Vector}\end{matrix}</math>

−

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_4 \\ \text{Cactus}\end{matrix}\!</math>

+

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_4 \\ \text{Cactus}\end{matrix}</math>

−

| style="width:25%" | <math>\begin{matrix}\mathcal{L}_5 \\ \text{English}\end{matrix}\!</math>

+

| style="width:25%" | <math>\begin{matrix}\mathcal{L}_5 \\ \text{English}\end{matrix}</math>

−

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_6 \\ \text{Ordinary}\end{matrix}\!</math>

+

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_6 \\ \text{Ordinary}\end{matrix}</math>

|- style="background:ghostwhite"

|  

−

| align="right" | <math>x\colon\!</math>

+

| align="right" | <math>x\colon</math>

−

| <math>1~1~0~0\!</math>

+

| <math>1~1~0~0</math>

|  

Line 934: Line 934:

|- style="background:ghostwhite"

|  

−

| align="right" | <math>y\colon\!</math>

+

| align="right" | <math>y\colon</math>

−

| <math>1~0~1~0\!</math>

+

| <math>1~0~1~0</math>

|  

Line 957: Line 957:

\\[4pt]

f_{7}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 975: Line 975:

\\[4pt]

f_{0111}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 993: Line 993:

\\[4pt]

0~1~1~1

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

−

\texttt{(~)}

+

\texttt{(} ~ \texttt{)}

\\[4pt]

\texttt{(} x \texttt{)(} y \texttt{)}

Line 1,011: Line 1,011:

\\[4pt]

\texttt{(} x ~ y \texttt{)}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,029: Line 1,029:

\\[4pt]

\text{not both}~ x ~\text{and}~ y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,047: Line 1,047:

\\[4pt]

\lnot x \lor \lnot y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

|-

| valign="bottom" |

Line 1,066: Line 1,066:

\\[4pt]

f_{15}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,084: Line 1,084:

\\[4pt]

f_{1111}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,102: Line 1,102:

\\[4pt]

1~1~1~1

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,119: Line 1,119:

\texttt{((} x \texttt{)(} y \texttt{))}

\\[4pt]

−

\texttt{((~))}

+

\texttt{((} ~ \texttt{))}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,138: Line 1,138:

\\[4pt]

\text{true}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,156: Line 1,156:

\\[4pt]

1

−

\end{matrix}\!</math>

+

\end{matrix}</math>

|}

Line 1,162: Line 1,162:

{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"

−

|+ style="height:30px" | <math>\text{Table 7-b.} ~~ \text{Propositional Forms on Two Variables}\!</math>

+

|+ style="height:30px" | <math>\text{Table 7-b.} ~~ \text{Propositional Forms on Two Variables}</math>

|- style="height:40px; background:ghostwhite"

| style="width:15%" | <math>\begin{matrix}\mathcal{L}_1 \\ \text{Decimal}\end{matrix}</math>

Line 1,172: Line 1,172:

|- style="background:ghostwhite"

|  

−

| align="right" | <math>x\colon\!</math>

+

| align="right" | <math>x\colon</math>

−

| <math>1~1~0~0\!</math>

+

| <math>1~1~0~0</math>

|  

Line 1,179: Line 1,179:

|- style="background:ghostwhite"

|  

−

| align="right" | <math>y\colon\!</math>

+

| align="right" | <math>y\colon</math>

−

| <math>1~0~1~0\!</math>

+

| <math>1~0~1~0</math>

|  

|-

−

| <math>f_{0}\!</math>

+

| <math>f_{0}</math>

−

| <math>f_{0000}\!</math>

+

| <math>f_{0000}</math>

−

| <math>0~0~0~0\!</math>

+

| <math>0~0~0~0</math>

−

| <math>\texttt{(~)}\!</math>

+

| <math>\texttt{(} ~ \texttt{)}</math>

−

| <math>\text{false}\!</math>

+

| <math>\text{false}</math>

−

| <math>0\!</math>

+

| <math>0</math>

|-

| valign="bottom" |

Line 1,201: Line 1,201:

\\[4pt]

f_{8}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,211: Line 1,211:

\\[4pt]

f_{1000}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,221: Line 1,221:

\\[4pt]

1~0~0~0

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,231: Line 1,231:

\\[4pt]

~ x ~~ y ~

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,241: Line 1,241:

\\[4pt]

x ~\text{and}~ y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,251: Line 1,251:

\\[4pt]

x \land y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

|-

| valign="bottom" |

Line 1,258: Line 1,258:

\\[4pt]

f_{12}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,264: Line 1,264:

\\[4pt]

f_{1100}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,270: Line 1,270:

\\[4pt]

1~1~0~0

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,276: Line 1,276:

\\[4pt]

x

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,282: Line 1,282:

\\[4pt]

x

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,288: Line 1,288:

\\[4pt]

x

−

\end{matrix}\!</math>

+

\end{matrix}</math>

|-

| valign="bottom" |

Line 1,295: Line 1,295:

\\[4pt]

f_{9}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,301: Line 1,301:

\\[4pt]

f_{1001}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,307: Line 1,307:

\\[4pt]

1~0~0~1

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,313: Line 1,313:

\\[4pt]

\texttt{((} x \texttt{,} y \texttt{))}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,319: Line 1,319:

\\[4pt]

x ~\text{equal to}~ y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,325: Line 1,325:

\\[4pt]

x = y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

|-

| valign="bottom" |

Line 1,332: Line 1,332:

\\[4pt]

f_{10}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,338: Line 1,338:

\\[4pt]

f_{1010}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,344: Line 1,344:

\\[4pt]

1~0~1~0

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,350: Line 1,350:

\\[4pt]

y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,362: Line 1,362:

\\[4pt]

y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

|-

| valign="bottom" |

Line 1,373: Line 1,373:

\\[4pt]

f_{14}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,383: Line 1,383:

\\[4pt]

f_{1110}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,393: Line 1,393:

\\[4pt]

1~1~1~0

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,403: Line 1,403:

\\[4pt]

\texttt{((} x \texttt{)(} y \texttt{))}

−

\end{matrix}\!</math>

+

\end{matrix}</math>

| valign="bottom" |

<math>\begin{matrix}

Line 1,423: Line 1,423:

\\[4pt]

x \lor y

−

\end{matrix}\!</math>

+

\end{matrix}</math>

|-

−

| <math>f_{15}\!</math>

+

| <math>f_{15}</math>

−

| <math>f_{1111}\!</math>

+

| <math>f_{1111}</math>

−

| <math>1~1~1~1\!</math>

+

| <math>1~1~1~1</math>

−

| <math>\texttt{((~))}\!</math>

+

| <math>\texttt{((} ~ \texttt{))}</math>

−

| <math>\text{true}\!</math>

+

| <math>\text{true}</math>

−

| <math>1\!</math>

+

| <math>1</math>

|}

Jon Awbrey

12,080

edits

Changes

Differential Logic and Dynamic Systems (view source)

Revision as of 21:40, 14 January 2021

Navigation menu

Page actions

Page actions

Personal tools

Navigation

semantic

Site statistics

Tools

Search