Changes

Line 694: Line 694:  
==Work Area==
 
==Work Area==
   −
<pre>
+
===Logical Tangent Vectors===
Logical Tangent Vectors
      
Discuss variation in portrayal of v in df(u,v):
 
Discuss variation in portrayal of v in df(u,v):
Line 711: Line 710:  
It helps to introduce some notation:
 
It helps to introduce some notation:
    +
<pre>
 
Let R = {real values}
 
Let R = {real values}
   Line 718: Line 718:     
Let U = Bn, p: Bn -> B.
 
Let U = Bn, p: Bn -> B.
 +
</pre>
    
In these terms, analogies of the following form are being explored:
 
In these terms, analogies of the following form are being explored:
 +
 +
<pre>
    
Rn f: Rn -> R
 
Rn f: Rn -> R
Line 730: Line 733:     
Bn p: Bn -> B
 
Bn p: Bn -> B
 +
</pre>
    
There are several circumstances that prevent the qualitative study from reducing to a special application of the quantitative theory and method.  These aspects of the logical problem domain make it something more than "differential geometry over the field of two elements", though it is always an advantage to recognize any facet of the problem region that does so reduce.
 
There are several circumstances that prevent the qualitative study from reducing to a special application of the quantitative theory and method.  These aspects of the logical problem domain make it something more than "differential geometry over the field of two elements", though it is always an advantage to recognize any facet of the problem region that does so reduce.
Line 743: Line 747:  
For example, a tangent vector at a point should be a certain kind of map of type
 
For example, a tangent vector at a point should be a certain kind of map of type
   −
v: (Bn -> B) -> B.
+
: v : (Bn -> B) -> B.
    
Consequently, a vector field should be a certain kind of map of type
 
Consequently, a vector field should be a certain kind of map of type
   −
w: Bn -> ((Bn -> B) -> B),
+
: w : Bn -> ((Bn -> B) -> B),
 +
 
 +
or
   −
or w: (Bn x (Bn -> B)) -> B,
+
: w : (Bn x (Bn -> B)) -> B,
    
and this is isomorphic to a derivation of type
 
and this is isomorphic to a derivation of type
   −
z: (Bn -> B) -> (Bn -> B).
+
: z : (Bn -> B) -> (Bn -> B).
    
Derivations, alias vector fields, also known as infinitesimal transformations, are the elements of Lie algebras, whose theory provides a systematic framework for the study of differential dynamics.
 
Derivations, alias vector fields, also known as infinitesimal transformations, are the elements of Lie algebras, whose theory provides a systematic framework for the study of differential dynamics.
Line 767: Line 773:  
Upon each point of the universe is built a duality of spaces, a pair of spaces that are linear duals of each other, the tangent (co-normal) and normal (co-tangent) spaces at that point.  As duals, either one may be chosen to institute their reciprocal definitions.  The functional bias that serves the purpose of programming computational implementations of these concepts makes it slightly more expedient to define the normal or co-tangent space first.
 
Upon each point of the universe is built a duality of spaces, a pair of spaces that are linear duals of each other, the tangent (co-normal) and normal (co-tangent) spaces at that point.  As duals, either one may be chosen to institute their reciprocal definitions.  The functional bias that serves the purpose of programming computational implementations of these concepts makes it slightly more expedient to define the normal or co-tangent space first.
   −
Original Universe of Discourse
+
===Original Universe of Discourse===
    
To do this, it helps to put concrete units, qualitatively distinctive features, back into the discussion.  For this we need to introduce some further notation.  Let A = {a1,...,an} be an alphabet of n symbols (letters, words, or sentences).  These symbols are interpreted as denoting the basic events, features, or propositions of a universe of discourse to which the logical calculus is being applied.  Graphically, the ai correspond to the property circles of a Venn diagram.  In functional terms A is a system of coordinate maps ai: U -> B.
 
To do this, it helps to put concrete units, qualitatively distinctive features, back into the discussion.  For this we need to introduce some further notation.  Let A = {a1,...,an} be an alphabet of n symbols (letters, words, or sentences).  These symbols are interpreted as denoting the basic events, features, or propositions of a universe of discourse to which the logical calculus is being applied.  Graphically, the ai correspond to the property circles of a Venn diagram.  In functional terms A is a system of coordinate maps ai: U -> B.
Line 773: Line 779:  
The circumstance that the universe U of type Bn is generated by the alphabet A is indicated by U = <A> = <a1,...,an>.  In concrete terms, we may express U as a product of distinct factors:
 
The circumstance that the universe U of type Bn is generated by the alphabet A is indicated by U = <A> = <a1,...,an>.  In concrete terms, we may express U as a product of distinct factors:
   −
U = Xi Ai = A1 x ... x An.
+
: U = Xi Ai = A1 x ... x An.
    
Here, Ai is an alphabet of two symbols, Ai = {(ai), ai}, where (ai) is a symbol with the logical value of "not ai".  Each Ai has the type B, under the ordered correspondence {(ai), ai} = {0, 1}.  The relation between the concrete signature and the abstract type of the universe U is indicated by the form:
 
Here, Ai is an alphabet of two symbols, Ai = {(ai), ai}, where (ai) is a symbol with the logical value of "not ai".  Each Ai has the type B, under the ordered correspondence {(ai), ai} = {0, 1}.  The relation between the concrete signature and the abstract type of the universe U is indicated by the form:
   −
Xi Ai = A1 x ... x An -> Bn.
+
: Xi Ai = A1 x ... x An -> Bn.
   −
Special Forms of Propositions
+
===Special Forms of Propositions===
    
Among the 2^2n propositions or functions in (Bn -> B) are several fundamental sets of 2n propositions each that take on special forms with respect to a given basis A.  Three of these forms are especially common, the singular, the linear, and the simple propositions.  Each set is naturally parameterized by the vectors in Bn and falls into n+1 ranks, with a binomial coefficient (n;k) giving the number of propositions of rank or weight k.
 
Among the 2^2n propositions or functions in (Bn -> B) are several fundamental sets of 2n propositions each that take on special forms with respect to a given basis A.  Three of these forms are especially common, the singular, the linear, and the simple propositions.  Each set is naturally parameterized by the vectors in Bn and falls into n+1 ranks, with a binomial coefficient (n;k) giving the number of propositions of rank or weight k.
Line 785: Line 791:  
The singular propositions may be expressed as products:
 
The singular propositions may be expressed as products:
   −
e1  ...  en where ei = ai  or  ei = (ai).
+
: e1  ...  en where ei = ai  or  ei = (ai).
    
The linear propositions may be expressed as sums:
 
The linear propositions may be expressed as sums:
   −
e1 + ... + en  where  ei = ai  or  ei = 0.
+
: e1 + ... + en  where  ei = ai  or  ei = 0.
    
The simple propositions may be expressed as products:
 
The simple propositions may be expressed as products:
   −
e1  ...  en where ei = ai  or  ei = 1.
+
: e1  ...  en where ei = ai  or  ei = 1.
    
In each case the rank k ranges from 0 to n and counts the number of positive appearances of coordinate propositions ai in the expression.  For example, with n = 3:  the singular proposition of rank 0 is (a1)(a2)(a3);  the linear proposition of rank 0 is "0";  the simple proposition of rank 0 is "1".
 
In each case the rank k ranges from 0 to n and counts the number of positive appearances of coordinate propositions ai in the expression.  For example, with n = 3:  the singular proposition of rank 0 is (a1)(a2)(a3);  the linear proposition of rank 0 is "0";  the simple proposition of rank 0 is "1".
Line 799: Line 805:  
Finally, two things are important to keep in mind with regard to the singularity, linearity, and simplicity of propositions.  First, these properties are all relative to a particular basis.  That is, a singular proposition with respect to a basis A will not remain singular if A is extended by a number of new and independent features.  Second, the singular propositions Bn -> B, picking out as they do a single cell or vector of Bn, are the vehicles or carriers of a certain type-ambiguity, vacillating between the duals Bn and (Bn -> B) and infecting the whole system of types.
 
Finally, two things are important to keep in mind with regard to the singularity, linearity, and simplicity of propositions.  First, these properties are all relative to a particular basis.  That is, a singular proposition with respect to a basis A will not remain singular if A is extended by a number of new and independent features.  Second, the singular propositions Bn -> B, picking out as they do a single cell or vector of Bn, are the vehicles or carriers of a certain type-ambiguity, vacillating between the duals Bn and (Bn -> B) and infecting the whole system of types.
   −
Logical Boundary Operator
+
===Logical Boundary Operator===
    
I think it may be useful at this point to say a few words about the form of the bound connective, which I also call the boundary operator of this calculus.
 
I think it may be useful at this point to say a few words about the form of the bound connective, which I also call the boundary operator of this calculus.
Line 807: Line 813:  
To understand this connection, consider a set of k propositional expressions, for example:  e1, e2, e3.  Now ask what would be the derivative p' of their logical conjunction p, which in EG becomes the multiplicative product of functions:  p = e1.e2.e3.  By a time-honored rule one would expect:
 
To understand this connection, consider a set of k propositional expressions, for example:  e1, e2, e3.  Now ask what would be the derivative p' of their logical conjunction p, which in EG becomes the multiplicative product of functions:  p = e1.e2.e3.  By a time-honored rule one would expect:
   −
p'   =   e1'e2.e3  +  e1.e2'e3  +  e1.e2.e3'.
+
: p' = e1'e2.e3  +  e1.e2'e3  +  e1.e2.e3'.
   −
Extended Universe of Discourse
+
===Extended Universe of Discourse===
    
The time has come to try and determine appropriate analogues in PC of tangent vectors and differential forms.  I am adapting terminology to the extent possible from (Flanders, 1989) and (Bott & Tu, 1982).  There are propositions p: U' -> B which are essentially no more than propositions p: U -> B in disguise.  These are the p for which every p'(x) is already determined to B, that is, those p for which all the p" are constant maps on dU.  These propositions are the differential forms of degree 0 on U and make up the space of 0-forms, F0(U).
 
The time has come to try and determine appropriate analogues in PC of tangent vectors and differential forms.  I am adapting terminology to the extent possible from (Flanders, 1989) and (Bott & Tu, 1982).  There are propositions p: U' -> B which are essentially no more than propositions p: U -> B in disguise.  These are the p for which every p'(x) is already determined to B, that is, those p for which all the p" are constant maps on dU.  These propositions are the differential forms of degree 0 on U and make up the space of 0-forms, F0(U).
Line 815: Line 821:  
With the above definitions and distinctions in mind the type of a tangent vector can be expressed more clearly as
 
With the above definitions and distinctions in mind the type of a tangent vector can be expressed more clearly as
    +
<pre>
 
v: (Dn -> B) -> B.
 
v: (Dn -> B) -> B.
   Line 820: Line 827:     
v:  F0(U)  -> B. ???
 
v:  F0(U)  -> B. ???
 +
</pre>
    
This indicates that v acts on a domain of functions q: Dn -> B in the normal (co-tangent) space of U.  A basis for such functions is provided by the differential alphabet dA = {da1,...,dan}.  v(q) = ?
 
This indicates that v acts on a domain of functions q: Dn -> B in the normal (co-tangent) space of U.  A basis for such functions is provided by the differential alphabet dA = {da1,...,dan}.  v(q) = ?
Line 825: Line 833:  
Consequently, a vector field should be a certain kind of map of type
 
Consequently, a vector field should be a certain kind of map of type
   −
w: Bn -> ((Dn -> B) -> B),
+
: w : Bn -> ((Dn -> B) -> B),
 +
 
 +
or
   −
or w: (Bn x (Dn -> B)) -> B,
+
: w : (Bn x (Dn -> B)) -> B,
    
and this is isomorphic to a derivation of type
 
and this is isomorphic to a derivation of type
   −
z: (Dn -> B) -> (Bn -> B).
+
: z : (Dn -> B) -> (Bn -> B).
    
The tangent vectors at a point x in U collectively form the tangent space at a point, Tx(U).  The tangent vectors at all points of U collectively form the tangent space of U, also called the tangent bundle T(U) or UT.
 
The tangent vectors at a point x in U collectively form the tangent space at a point, Tx(U).  The tangent vectors at all points of U collectively form the tangent space of U, also called the tangent bundle T(U) or UT.
Line 841: Line 851:  
To define the differential extension of a propositional universe, it is necessary to define tangent spaces and differential forms.  To do this we extend the alphabet A to include differential features.  On intutive terms these may be construed as primitive features of change, or propositions about changes in the original set of features.  Hence, let dA = {da1,...,dan} and dU = <dA> = <da1,...,dan>.  Let U' = U x dU = <A + dA> = <a1,...,an, da1,...,dan>.
 
To define the differential extension of a propositional universe, it is necessary to define tangent spaces and differential forms.  To do this we extend the alphabet A to include differential features.  On intutive terms these may be construed as primitive features of change, or propositions about changes in the original set of features.  Hence, let dA = {da1,...,dan} and dU = <dA> = <da1,...,dan>.  Let U' = U x dU = <A + dA> = <a1,...,an, da1,...,dan>.
    +
<pre>
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
  
12,080

edits