Changes

The above definition of <math>\operatorname{d}x_i : X^2 \to \mathbb{B}</math> is equivalent to defining <math>\operatorname{d}x_i : (\mathbb{B} \to X) \to \mathbb{B}</math> in the following way:

The above definition of <math>\operatorname{d}x_i : X^2 \to \mathbb{B}</math> is equivalent to defining <math>\operatorname{d}x_i : (\mathbb{B} \to X) \to \mathbb{B}</math> in the following way:

:{| cellpadding=2

: <p><math>\begin{array}{lcrcl}

| d''x''_''i''(''q'')

\operatorname{d}x_i (q) & = & (\!|\ x_i (q_0) & , & x_i (q_1)\ |\!) \\

| =

                        & = &  x_i (q_0)     & + & x_i (q_1)       \\

| <font face=system>(</font> ''x''_''i''(''q''₀) , ''x''_''i''(''q''₁) <font face=system>)</font>

                        & = &  x_i (q_1)     & - & x_i (q_0).      \\

\end{array}</math></p>

| &nbsp;

| =

| ''x''_''i''(''q''₀) + ''x''_''i''(''q''₁)

| &nbsp;

| =

| ''x''_''i''(''q''₁) &ndash; ''x''_''i''(''q''₀),

where ''q''_''b'' = ''q''(''b''), for each ''b'' in '''B'''.  Thus, the proposition d''x''_''i'' is true of the path ''q'' = ‹''u'',&nbsp;''v''› exactly if the terms of ''q'', the endpoints ''u'' and ''v'', lie on different sides of the question ''x''_''i''.

In this definition ''q''_''b'' = ''q''(''b''), for each ''b'' in '''B'''.  Thus, the proposition d''x''_''i'' is true of the path ''q'' = ‹''u'',&nbsp;''v''› exactly if the terms of ''q'', the endpoints ''u'' and ''v'', lie on different sides of the question ''x''_''i''.

Now we can use the language of features in 〈d<font face="lucida calligraphy">X</font>〉, indeed the whole calculus of propositions in [d<font face="lucida calligraphy">X</font>], to classify paths and sets of paths.  In other words, the paths can be taken as models of the propositions ''g''&nbsp;:&nbsp;d''X''&nbsp;&rarr;&nbsp;'''B'''.  For example, the paths corresponding to ''Diag''(''X'') fall under the description <font face=system>(</font>d''x''₁<font face=system>)</font>&hellip;<font face=system>(</font>d''x''_''n''<font face=system>)</font>, which says that nothing changes among the set of features {''x''₁,&nbsp;&hellip;,&nbsp;''x''_''n''}.

Now we can use the language of features in 〈d<font face="lucida calligraphy">X</font>〉, indeed the whole calculus of propositions in [d<font face="lucida calligraphy">X</font>], to classify paths and sets of paths.  In other words, the paths can be taken as models of the propositions ''g''&nbsp;:&nbsp;d''X''&nbsp;&rarr;&nbsp;'''B'''.  For example, the paths corresponding to ''Diag''(''X'') fall under the description <font face=system>(</font>d''x''₁<font face=system>)</font>&hellip;<font face=system>(</font>d''x''_''n''<font face=system>)</font>, which says that nothing changes among the set of features {''x''₁,&nbsp;&hellip;,&nbsp;''x''_''n''}.