Changes

! <math>\mbox{Boolean Domain}\ \mathbb{B}</math>

! <math>\mbox{Boolean Domain}\ \mathbb{B}</math>

|-

|-

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

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

| <math>\begin{smallmatrix}\mbox{Basic Space}\end{smallmatrix}</math>

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

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

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

|-

|-

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

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

| <math>\begin{smallmatrix}\mbox{Function Space}\end{smallmatrix}</math>

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

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

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

|-

|-

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

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

| <math>\begin{smallmatrix}\mbox{Tangent Vector}\end{smallmatrix}</math>

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

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

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

|-

|-

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

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

| <math>\begin{smallmatrix}\mbox{Vector Field}\end{smallmatrix}</math>

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

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

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

|-

|-

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

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

| <font size="4">"</font>

| <font size="4">"</font>

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

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

|-

|-

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

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

| <font size="4">"</font>

| <font size="4">"</font>

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

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

|-

|-

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

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

| <math>\begin{smallmatrix}\mbox{Derivation}\end{smallmatrix}</math>

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

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

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

|-

|-

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

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

| <math>\begin{smallmatrix}\mbox{Basic Transformation}\end{smallmatrix}</math>

| <math>\mbox{Basic}\!</math> <math>\mbox{Transformation}\!</math>

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

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

|-

|-

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

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

| <math>\begin{smallmatrix}\mbox{Function Transformation}\end{smallmatrix}</math>

| <math>\mbox{Function}\!</math> <math>\mbox{Transformation}\!</math>

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

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

| <math>\ldots\!</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.

The arrangement of types collected in Table&nbsp;3 (repeated below) can serve as a good introduction to several ideas about ''higher order propositional expressions'' (HOPE's) and also about the ''propositions as types'' (PAT) isomorphism.

The arrangement of types collected in Table&nbsp;3 (repeated below) can serve as a good introduction to several ideas about ''higher order propositional expressions'' (HOPE's) and also about the ''propositions as types'' (PAT) isomorphism.

{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

{| align="center" border="1" cellpadding="4" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

|+ '''Table 3.  Analogy Between Real and Boolean Types'''

|+ '''Table 3.  Analogy of Real and Boolean Types'''

|- style="background:ghostwhite"

|- style="background:ghostwhite"

! Real Domain '''R'''

! <math>\mbox{Real Domain}\ \mathbb{R}</math>

! &larr;&rarr;

! <math>\longleftrightarrow</math>

! Boolean Domain '''B'''

! <math>\mbox{Boolean Domain}\ \mathbb{B}</math>

|-

|-

| '''R'''^''n''

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

| Basic Space

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

| '''B'''^''n''

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

|-

|-

| '''R'''^''n''&nbsp;&rarr;&nbsp;'''R'''

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

| Function Space

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

| '''B'''^''n''&nbsp;&rarr;&nbsp;'''B'''

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

|-

|-

| ('''R'''^''n''&rarr;'''R''')&nbsp;&rarr;&nbsp;'''R'''

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

| Tangent Vector

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

| ('''B'''^''n''&rarr;'''B''')&nbsp;&rarr;&nbsp;'''B'''

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

|-

|-

| '''R'''^''n''&nbsp;&rarr;&nbsp;(('''R'''^''n''&rarr;'''R''')&rarr;'''R''')

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

| Vector Field

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

| '''B'''^''n''&nbsp;&rarr;&nbsp;(('''B'''^''n''&rarr;'''B''')&rarr;'''B''')

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

|-

|-

| ('''R'''^''n''&nbsp;&times;&nbsp;('''R'''^''n''&rarr; '''R'''))&nbsp;&rarr;&nbsp;'''R'''

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

| ditto

| <font size="4">"</font>

| ('''B'''^''n''&nbsp;&times;&nbsp;('''B'''^''n''&rarr; '''B'''))&nbsp;&rarr;&nbsp;'''B'''

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

|-

|-

| (('''R'''^''n''&rarr;'''R''')&nbsp;&times;&nbsp;'''R'''^''n'')&nbsp;&rarr;&nbsp;'''R'''

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

| <font size="4">"</font>

| (('''B'''^''n''&rarr;'''B''')&nbsp;&times;&nbsp;'''B'''^''n'')&nbsp;&rarr;&nbsp;'''B'''

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

| ('''R'''^''n''&rarr;'''R''')&nbsp;&rarr;&nbsp;('''R'''^''n''&rarr;'''R''')

| ('''B'''^''n''&rarr;'''B''')&nbsp;&rarr;&nbsp;('''B'''^''n''&rarr;'''B''')

|-

|-

| '''R'''^''n''&nbsp;&rarr;&nbsp;'''R'''^''m''

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

| Basic Transformation

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

| '''B'''^''n''&nbsp;&rarr;&nbsp;'''B'''^''m''

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

|-

|-

| ('''R'''^''n''&rarr;'''R''')&nbsp;&rarr;&nbsp;('''R'''^''m''&rarr;'''R''')

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

| Function Transformation

| <math>\mbox{Basic}\!</math> <math>\mbox{Transformation}\!</math>

| ('''B'''^''n''&rarr;'''B''')&nbsp;&rarr;&nbsp;('''B'''^''m''&rarr;'''B''')

| <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>\mbox{Function}\!</math> <math>\mbox{Transformation}\!</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 ('''K'''^''n''&nbsp;&rarr; '''K''')&nbsp;&rarr;&nbsp;'''K''', where '''K''' is the chosen ground field, in the present case either '''R''' or '''B'''.  At a point in a space of type '''K'''^''n'', a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an ''f'' of type ('''K'''^''n''&nbsp;&rarr; '''K'''), and maps it to a ground field value of type '''K'''.  This value is known as the ''derivative'' of ''f'' in the direction <math>\vartheta\!</math> [Che46, 76-77].  In the boolean case, <math>\vartheta\!</math>&nbsp;:&nbsp;('''B'''^''n''&nbsp;&rarr; '''B''')&nbsp;&rarr;&nbsp;'''B''' 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 ('''K'''^''n''&nbsp;&rarr; '''K''')&nbsp;&rarr;&nbsp;'''K''', where '''K''' is the chosen ground field, in the present case either '''R''' or '''B'''.  At a point in a space of type '''K'''^''n'', a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an ''f'' of type ('''K'''^''n''&nbsp;&rarr; '''K'''), and maps it to a ground field value of type '''K'''.  This value is known as the ''derivative'' of ''f'' in the direction <math>\vartheta\!</math> [Che46, 76-77].  In the boolean case, <math>\vartheta\!</math>&nbsp;:&nbsp;('''B'''^''n''&nbsp;&rarr; '''B''')&nbsp;&rarr;&nbsp;'''B''' has the form of a proposition about propositions, in other words, a proposition of the next higher type.