Directory:Jon Awbrey/Papers/Differential Logic and Dynamic Systems 3.0 - Revision history

Jon Awbrey: update

2013-10-03T15:46:50Z

update

Jon Awbrey: update

2013-09-25T00:44:14Z

update

Show changes

Jon Awbrey: /* Transformations of Type B2 → B2 */ link to image

2013-07-08T14:56:43Z

Transformations of Type B2 → B2: link to image

Jon Awbrey: delete obsolete tags

2013-07-08T14:41:24Z

delete obsolete tags

Jon Awbrey: /* Differential Analysis of Propositions and Transformations */ fix accidental deletion

2011-07-28T04:16:45Z

Differential Analysis of Propositions and Transformations: fix accidental deletion

Jon Awbrey: /* Propositional Transformations */ ‘artificial’

2011-07-28T04:14:15Z

Propositional Transformations: ‘artificial’

Jon Awbrey: cleanup

2011-07-28T04:04:21Z

cleanup

Jon Awbrey: /* Reality at the Threshold of Logic */ tweak table

2009-07-12T21:00:19Z

Reality at the Threshold of Logic: tweak table

Jon Awbrey: /* Propositions as Types and Higher Order Types */ tweak table

2009-07-12T04:28:39Z

Propositions as Types and Higher Order Types: tweak table

Jon Awbrey: /* Propositions as Types and Higher Order Types */ tweak table

2009-07-12T04:20:55Z

Propositions as Types and Higher Order Types: tweak table

@@ Line 45: / Line 45: @@
 <br>
-{| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%"
+{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:75%"
-|+ <math>\text{Table 1.} ~~ \text{Syntax and Semantics of a Calculus for Propositional Logic}</math>
+|+ style="height:30px" | <math>\text{Table 1.} ~~ \text{Syntax and Semantics of a Calculus for Propositional Logic}\!</math>
-|- style="background:#f0f0ff"
+|- style="height:40px; background:ghostwhite"
 | <math>\text{Graph}\!</math>
 | <math>\text{Expression}~\!</math>
@@ Line 287: / Line 287: @@
 |-
 | <math>A_i\!</math>
-| <math>\{ (a_i), a_i \}\!</math>
+| <math>\{ \texttt{(} a_i \texttt{)}, a_i \}\!</math>
 | <math>\text{Dimension}~ i\!</math>
 | <math>\mathbb{B}\!</math>
@@ Line 671: / Line 671: @@
+|
 <math>\begin{matrix}
-\underline{X}_i & = & \{ (\underline{x}_i), \underline{x}_i \}
+\underline{X}_i & = & \{ \texttt{(} \underline{x}_i \texttt{)}, \underline{x}_i \}
 \\
 & \cong & \mathbb{B}
@@ Line 677: / Line 677: @@
+|
 <math>\begin{matrix}
-A_i & = & \{ (a_i), a_i \}
+A_i & = & \{ \texttt{(} a_i \texttt{)}, a_i \}
 \\
 & \cong & \mathbb{B}
@@ Line 1,690: / Line 1,690: @@
 |-
 | <math>\mathrm{d}A_i\!</math>
-| <math>\{ (\mathrm{d}a_i), \mathrm{d}a_i \}~\!</math>
+| <math>\{ \texttt{(} \mathrm{d}a_i \texttt{)}, \mathrm{d}a_i \}\!</math>
 | <math>\text{Differential dimension}~ i\!</math>
 | <math>\mathbb{D}\!</math>

@@ Line 7,301: / Line 7,301: @@
 Figure 70-b shows another way to picture the action of the tangent functor on the logical transformation ''F''‹''u'',&nbsp;''v''›&nbsp;=&nbsp;‹((''u'')(''v'')),&nbsp;((''u'',&nbsp;''v''))›, roughly in the style of the ''bundle of universes'' type of diagram.
-<p>[[Image:Tangent_Functor_Ferris_Wheel.gif|center|frame|<font size="3">'''Figure 70-b.  Tangent Functor Ferris Wheel for F‹u, v› = ‹((u)(v)), ((u, v))›'''</font>]]</p>
+<p>[[Image:Diff Log Dyn Sys -- Figure 70-b -- Tangent Functor Diagram.gif|center|frame|<font size="3">'''Figure 70-b.  Tangent Functor Ferris Wheel for F‹u, v› = ‹((u)(v)), ((u, v))›'''</font>]]</p>
 * '''Nota Bene.'''  The original Figure&nbsp;70-b lost some of its labeling in a succession of platform metamorphoses over the years, so I have included an Ascii version below to indicate where the missing labels go.

@@ Line 9,329: / Line 9,329: @@
 Recoded:  03 Jun 2007
 </pre>
 [[Category:Adaptive Systems]]

@@ Line 3,338: / Line 3,338: @@
 | width="4%"  | &nbsp;
 | width="92%" |
-he resultant metaphysical problem now is this:  ''Does the man go round the squirrel or not?''
+The resultant metaphysical problem now is this:  ''Does the man go round the squirrel or not?''
 | width="4%"  | &nbsp;
 |-

@@ Line 3,088: / Line 3,088: @@
 | width="4%"  | &nbsp;
 | width="92%" |
-If only the word 'artificial' were associated with the idea of ''art'', or expert skill gained through voluntary apprenticeship (instead of suggesting the factitious and unreal), we might say that ''logical'' refers to artificial thought.
+If only the word &lsquo;artificial&rsquo; were associated with the idea of ''art'', or expert skill gained through voluntary apprenticeship (instead of suggesting the factitious and unreal), we might say that ''logical'' refers to artificial thought.
 | width="4%"  | &nbsp;
 |-

@@ Line 9,330: / Line 9,330: @@
 </pre>
-{{aficionados}}<sharethis />
+<br><sharethis />
 <!--semantic tags-->

@@ Line 612: / Line 612: @@
 |}
-Table 5 accumulates an array of notation that I hope will not be too distracting.  Some of it is rarely needed, but has been filled in for the sake of completeness.  Its purpose is simple, to give literal expression to the visual intuitions that come with venn diagrams, and to help build a bridge between our qualitative and quantitative outlooks on dynamic systems.
+Table&nbsp;5 accumulates an array of notation that I hope will not be too distracting.  Some of it is rarely needed, but has been filled in for the sake of completeness.  Its purpose is simple, to give literal expression to the visual intuitions that come with venn diagrams, and to help build a bridge between our qualitative and quantitative outlooks on dynamic systems.
-{| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:left; width:96%"
+<br>
-|+ '''Table 5.  A Bridge Over Troubled Waters'''
-|- style="background:ghostwhite"
+{| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; width:90%"
-| align="center" | <math>\mbox{Linear Space}\!</math>
+|+ <math>\text{Table 5.}~~\text{A Bridge Over Troubled Waters}</math>
-| align="center" | <math>\mbox{Liminal Space}\!</math>
+|- style="background:#f0f0ff"
-| align="center" | <math>\mbox{Logical Space}\!</math>
+| align="center" | <math>\text{Linear Space}\!</math>
 |-
+|
@@ Line 758: / Line 760: @@
 = & [\mathbb{B}^n]                                    \\
 \end{matrix}</math>
-|}<br>
+|}
 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>

@@ Line 569: / Line 569: @@
 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&nbsp;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>\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&ndash;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&nbsp;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>\xi : X \to \textstyle\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&ndash;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&nbsp;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:96%"
+<br>
-|+ '''Table 4.  An Equivalence Based on the Propositions as Types Analogy
-'''
+{| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%"
-|- style="background:ghostwhite"
+|+ <math>\text{Table 4.}~~\text{An Equivalence Based on the Propositions as Types Analogy}</math>
-! <math>\mbox{Pattern}\!</math>
+|- style="background:#f0f0ff"
-! <math>\mbox{Construct}\!</math>
+| <math>\text{Pattern}\!</math>
-! <math>\mbox{Instance}\!</math>
+| <math>\text{Construct}\!</math>
 |-
 | <math>X \to (Y \to Z)</math>
@@ Line 596: / Line 597: @@
 | <math>\mbox{Derivation}\!</math>
 | <math>(\mathbb{K}^n \to \mathbb{K}) \to (\mathbb{K}^n \to \mathbb{K})</math>
-|}<br>
+|}
 ===Reality at the Threshold of Logic===

@@ Line 513: / Line 513: @@
 The types collected in Table&nbsp;3 (repeated below) serve to illustrate the themes of ''higher order propositional expressions'' and the ''propositions as types'' (PAT) analogy.
-{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"
+<br>
-|+ '''Table 3.  Analogy Between Real and Boolean Types'''
-|- style="background:ghostwhite"
+{| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%"
-! <math>\mbox{Real Domain}\ \mathbb{R}</math>
+|+ <math>\text{Table 3.}~~\text{Analogy Between Real and Boolean Types}</math>
-! <math>\longleftrightarrow</math>
+|- style="background:#f0f0ff"
-! <math>\mbox{Boolean Domain}\ \mathbb{B}</math>
+| <math>\text{Real Domain}~ \mathbb{R}</math>
 |-
 | <math>\mathbb{R}^n</math>
@@ Line 559: / Line 561: @@
 <p><math>\mbox{Transformation}\!</math></p>
 | <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math>
-|}<br>
+|}
 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&ndash;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.