Changes

It will be necessary to develop a more refined analysis of this statement directly, but that is roughly the nub of it.

It will be necessary to develop a more refined analysis of this statement directly, but that is roughly the nub of it.

If the form of the above statement reminds you of De Morgan's rule, it is no accident, as differentiation and negation turn out to be closely related operations. .Indeed, one can find discussions of logical difference calculus in the Boole-De Morgan correspondence and [[C.S. Peirce]] also made use of differential operators in a logical context, but the exploration of these ideas has been hampered by a number of factors, not the least of which being a syntax adequate to handle the complexity of expressions that evolve.

If the form of the above statement reminds you of De Morgan's rule, it is no accident, as differentiation and negation turn out to be closely related operations. Indeed, one can find discussions of logical difference calculus in the Boole–De Morgan correspondence and [[C.S. Peirce]] also made use of differential operators in a logical context, but the exploration of these ideas has been hampered by a number of factors, not the least of which being a syntax adequate to handle the complexity of expressions that evolve.

For my part, it was definitely a case of the calculus being smarter than the calculator thereof.  The graphical pictures were catalytic in their power over my thinking process, leading me so quickly past so many obstructions that I did not have time to think about all of the difficulties that would otherwise have inhibited the derivation. .It did eventually became necessary to write all this up in a linear script, and to deal with the various problems of interpretation and justification that I could imagine, but that took another 120 pages, and so, if you don't like this intuitive approach, then let that be your sufficient notice.

For my part, it was definitely a case of the calculus being smarter than the calculator thereof.  The graphical pictures were catalytic in their power over my thinking process, leading me so quickly past so many obstructions that I did not have time to think about all of the difficulties that would otherwise have inhibited the derivation. .It did eventually became necessary to write all this up in a linear script, and to deal with the various problems of interpretation and justification that I could imagine, but that took another 120 pages, and so, if you don't like this intuitive approach, then let that be your sufficient notice.

Let us run through the initial example again, this time attempting to interpret the formulas that develop at each stage along the way.

Let us run through the initial example again, this time attempting to interpret the formulas that develop at each stage along the way.

We begin with a proposition or a boolean function ''f''(''x'', ''y'') = ''xy''.

We begin with a proposition or a boolean function <math>f(x, y) = xy.\!</math>

<pre>

<pre>

</pre>

</pre>

A function like this has an abstract type and a concrete type. .The abstract type is what we invoke when we write things like ''f''&nbsp;:&nbsp;'''B'''&nbsp;&times;&nbsp;'''B'''&nbsp;&rarr;&nbsp;'''B''' or ''f''&nbsp;:&nbsp;'''B'''²&nbsp;&rarr;&nbsp;'''B'''. .The concrete type takes into account the qualitative dimensions or the "units" of the case, which can be explained as follows.

A function like this has an abstract type and a concrete type. The abstract type is what we invoke when we write things like <math>f : \mathbb{B} \times \mathbb{B} \to \mathbb{B}</math> or <math>f : \mathbb{B}^2 \to \mathbb{B}.</math> The concrete type takes into account the qualitative dimensions or the "units" of the case, which can be explained as follows.

* Let ''X'' be the set of values {(''x''), ''x''} = {not ''x'', ''x''}.

* Let ''X'' be the set of values {(''x''), ''x''} = {not ''x'', ''x''}.

Then interpret the usual propositions about ''x'', ''y'' as functions of the concrete type ''f''&nbsp;:&nbsp;''X''&nbsp;&times;&nbsp;''Y''&nbsp;&rarr;&nbsp;'''B'''.

Then interpret the usual propositions about ''x'', ''y'' as functions of the concrete type ''f''&nbsp;:&nbsp;''X''&nbsp;&times;&nbsp;''Y''&nbsp;&rarr;&nbsp;'''B'''.

We are going to consider various "operators" on these functions. .Here, an operator ''F'' is a function that takes one function ''f'' into another function ''Ff''.

We are going to consider various "operators" on these functions. Here, an operator ''F'' is a function that takes one function ''f'' into another function ''Ff''.

The first couple of operators that we need to consider are logical analogues of those that occur in the classical "finite difference calculus", namely:

The first couple of operators that we need to consider are logical analogues of those that occur in the classical "finite difference calculus", namely:

These days, ''E'' is more often called the ''shift'' operator.

These days, ''E'' is more often called the ''shift'' operator.

In order to describe the universe in which these operators operate, it will be necessary to enlarge our original universe of discourse. .We mount up from the space ''U'' = ''X''&nbsp; &times;&nbsp;''Y'' to its ''differential extension'',

In order to describe the universe in which these operators operate, it will be necessary to enlarge our original universe of discourse. We mount up from the space ''U'' = ''X''&nbsp; &times;&nbsp;''Y'' to its ''differential extension'',

''EU'' = ''U''&nbsp; &times;&nbsp;''dU'' = ''X''&nbsp;&times;&nbsp;''Y''&nbsp;&times;&nbsp;''dX''&nbsp; &times;&nbsp;''dY'', with ''dX'' = {(''dx''), ''dx''} and ''dY'' = {(''dy''), ''dy''}. .The interpretations of these new symbols can be diverse, but the easiest for now is just to say that ''dx'' means "change x" and ''dy'' means "change y". .To draw the differential extension ''EU'' of our present universe ''U'' = ''X''&nbsp; &times;&nbsp;''Y'' as a venn diagram, it would take us four logical dimensions ''X'', ''Y'', ''dX'', ''dY'', but we can project a suggestion of what it's about on the universe ''X''&nbsp; &times;&nbsp;''Y'' by drawing arrows that cross designated borders, labeling the arrows as ''dx'' when crossing the border between ''x'' and (''x'') and as ''dy'' when crossing the border between ''y'' and (''y''), in either direction, in either case.

''EU'' = ''U''&nbsp; &times;&nbsp;''dU'' = ''X''&nbsp;&times;&nbsp;''Y''&nbsp;&times;&nbsp;''dX''&nbsp; &times;&nbsp;''dY'', with ''dX'' = {(''dx''), ''dx''} and ''dY'' = {(''dy''), ''dy''}. .The interpretations of these new symbols can be diverse, but the easiest for now is just to say that ''dx'' means "change x" and ''dy'' means "change y". .To draw the differential extension ''EU'' of our present universe ''U'' = ''X''&nbsp; &times;&nbsp;''Y'' as a venn diagram, it would take us four logical dimensions ''X'', ''Y'', ''dX'', ''dY'', but we can project a suggestion of what it's about on the universe ''X''&nbsp; &times;&nbsp;''Y'' by drawing arrows that cross designated borders, labeling the arrows as ''dx'' when crossing the border between ''x'' and (''x'') and as ''dy'' when crossing the border between ''y'' and (''y''), in either direction, in either case.

</pre>

</pre>

We did not yet go through the trouble to interpret this (first order) ''difference of conjunction'' fully, but were happy simply to evaluate it with respect to a single location in the universe of discourse, namely, at the point picked out by the singular proposition ''xy'', in as much as if to say, at the place where ''x'' = 1 and ''y'' = 1. .This evaluation is written in the form ''Df''|''xy'' or ''Df''|<1, 1>, and we arrived at the locally applicable law that states that ''f'' = ''xy'' = ''x'' & ''y'' &rArr; ''Df''|''xy'' = ((''dx'')(''dy'')) = ''dx'' or ''dy''.

We did not yet go through the trouble to interpret this (first order) ''difference of conjunction'' fully, but were happy simply to evaluate it with respect to a single location in the universe of discourse, namely, at the point picked out by the singular proposition ''xy'', in as much as if to say, at the place where ''x'' = 1 and ''y'' = 1. This evaluation is written in the form ''Df''|''xy'' or ''Df''|<1, 1>, and we arrived at the locally applicable law that states that ''f'' = ''xy'' = ''x'' & ''y'' &rArr; ''Df''|''xy'' = ((''dx'')(''dy'')) = ''dx'' or ''dy''.

<pre>

<pre>

</pre>

</pre>

The picture illustrates the analysis of the inclusive disjunction ((''dx'')(''dy'')) into the exclusive disjunction: .''dx''(''dy'') + ''dy''(''dx'') + ''dx dy'', a proposition that may be interpreted to say "change x or change y or both". .And this can be recognized as just what you need to do if you happen to find yourself in the center cell and desire a detailed description of ways to depart it.

The picture illustrates the analysis of the inclusive disjunction ((''dx'')(''dy'')) into the exclusive disjunction: .''dx''(''dy'') + ''dy''(''dx'') + ''dx dy'', a proposition that may be interpreted to say "change x or change y or both". And this can be recognized as just what you need to do if you happen to find yourself in the center cell and desire a detailed description of ways to depart it.

We have just computed what will variously be called the ''difference map'', the ''difference proposition'', or the ''local proposition'' ''Df''_''p'' for the proposition ''f''(''x'',&nbsp;''y'') = ''xy'' at the point ''p'' where ''x'' = 1 and ''y'' = 1.

We have just computed what will variously be called the ''difference map'', the ''difference proposition'', or the ''local proposition'' ''Df''_''p'' for the proposition ''f''(''x'',&nbsp;''y'') = ''xy'' at the point ''p'' where ''x'' = 1 and ''y'' = 1.

In the universe ''U'' = ''X''&nbsp;&times;&nbsp;''Y'', the four propositions ''xy'', ''x''(''y''), (''x'')''y'', (''x'')(''y'') that indicate the "cells", or the smallest regions of the venn diagram, are called ''singular propositions''. .These serve as an alternative notation for naming the points <1,&nbsp;1>, <1,&nbsp;0>, <0,&nbsp;1>, <0,&nbsp;0>, respectively.

In the universe ''U'' = ''X''&nbsp;&times;&nbsp;''Y'', the four propositions ''xy'', ''x''(''y''), (''x'')''y'', (''x'')(''y'') that indicate the "cells", or the smallest regions of the venn diagram, are called ''singular propositions''. These serve as an alternative notation for naming the points <1,&nbsp;1>, <1,&nbsp;0>, <0,&nbsp;1>, <0,&nbsp;0>, respectively.

Thus, we can write ''Df''_''p'' = ''Df''|''p'' = ''Df''|<1, 1> = ''Df''|''xy'', so long as we know the frame of reference in force.

Thus, we can write ''Df''_''p'' = ''Df''|''p'' = ''Df''|<1, 1> = ''Df''|''xy'', so long as we know the frame of reference in force.

By inspection, it is fairly easy to understand ''Df'' as telling you what you have to do from each point of ''U'' in order to change the value borne by ''f''(''x'',&nbsp;''y'').

By inspection, it is fairly easy to understand ''Df'' as telling you what you have to do from each point of ''U'' in order to change the value borne by ''f''(''x'',&nbsp;''y'').

We have been studying the action of the difference operator ''D'', also known as the ''localization operator'', on the proposition ''f''&nbsp;:&nbsp;''X''&nbsp;&times;&nbsp;''Y''&nbsp;&rarr;&nbsp;'''B''' that is commonly known as the conjunction ''xy''. .We described ''Df'' as a (first order) differential proposition, that is, a proposition of the type ''Df''&nbsp;:&nbsp;''X''&nbsp;&times;&nbsp;''Y''&nbsp;&times;&nbsp;''dX''&nbsp;&times;&nbsp;''dY''&nbsp;&rarr;&nbsp;'''B'''. .Abstracting from the augmented venn diagram that illustrates how the ''models'', or the ''satisfying interpretations'', of ''Df'' distribute within the extended universe ''EU'' = ''X''&nbsp;&times;&nbsp;''Y''&nbsp;&times;&nbsp;''dX''&nbsp;&times;&nbsp;''dY'', we can depict ''Df'' in the form of a ''digraph'' or ''directed graph'', one whose points are labeled with the elements of ''U'' = .''X''&nbsp;&times;&nbsp;''Y'' and whose arrows are labeled with the elements of ''dU'' = ''dX''&nbsp;&times;&nbsp;''dY''.

We have been studying the action of the difference operator ''D'', also known as the ''localization operator'', on the proposition ''f''&nbsp;:&nbsp;''X''&nbsp;&times;&nbsp;''Y''&nbsp;&rarr;&nbsp;'''B''' that is commonly known as the conjunction ''xy''. We described ''Df'' as a (first order) differential proposition, that is, a proposition of the type ''Df''&nbsp;:&nbsp;''X''&nbsp;&times;&nbsp;''Y''&nbsp;&times;&nbsp;''dX''&nbsp;&times;&nbsp;''dY''&nbsp;&rarr;&nbsp;'''B'''. .Abstracting from the augmented venn diagram that illustrates how the ''models'', or the ''satisfying interpretations'', of ''Df'' distribute within the extended universe ''EU'' = ''X''&nbsp;&times;&nbsp;''Y''&nbsp;&times;&nbsp;''dX''&nbsp;&times;&nbsp;''dY'', we can depict ''Df'' in the form of a ''digraph'' or ''directed graph'', one whose points are labeled with the elements of ''U'' = .''X''&nbsp;&times;&nbsp;''Y'' and whose arrows are labeled with the elements of ''dU'' = ''dX''&nbsp;&times;&nbsp;''dY''.

<pre>

<pre>

</pre>

</pre>

Any proposition worth its salt has many equivalent ways to view it, any one of which may reveal some unsuspected aspect of its meaning. .We will encounter more and more of these variant readings as we go.

Any proposition worth its salt has many equivalent ways to view it, any one of which may reveal some unsuspected aspect of its meaning. We will encounter more and more of these variant readings as we go.

The enlargement operator ''E'', also known as the ''shift operator'', has many interesting and very useful properties in its own right, so let us not fail to observe a few of the more salient features that play out on the surface of our simple example, ''f''(''x'',&nbsp;''y'') = ''xy''.

The enlargement operator ''E'', also known as the ''shift operator'', has many interesting and very useful properties in its own right, so let us not fail to observe a few of the more salient features that play out on the surface of our simple example, ''f''(''x'',&nbsp;''y'') = ''xy''.

: ''Ef''(''x''₁,&nbsp;&hellip;,&nbsp;''x''_''k'', ''dx''₁,&nbsp;&hellip;,&nbsp;''dx''_''k'') = ''f''(''x''₁&nbsp;+&nbsp;''dx''₁,&nbsp;&hellip;,&nbsp;''x''_''k''&nbsp;+&nbsp;''dx''_''k'').

: ''Ef''(''x''₁,&nbsp;&hellip;,&nbsp;''x''_''k'', ''dx''₁,&nbsp;&hellip;,&nbsp;''dx''_''k'') = ''f''(''x''₁&nbsp;+&nbsp;''dx''₁,&nbsp;&hellip;,&nbsp;''x''_''k''&nbsp;+&nbsp;''dx''_''k'').

It should be noted that the so-called ''differential variables'' ''dx''_''j'' are really just the same kind of boolean variables as the other ''x''_''j''. .It is conventional to give the additional variables these brands of inflected names, but whatever extra connotations we might choose to attach to these syntactic conveniences are wholly external to their purely algebraic meanings.

It should be noted that the so-called ''differential variables'' ''dx''_''j'' are really just the same kind of boolean variables as the other ''x''_''j''. It is conventional to give the additional variables these brands of inflected names, but whatever extra connotations we might choose to attach to these syntactic conveniences are wholly external to their purely algebraic meanings.

For the example ''f''(''x'', ''y'') = ''xy'', we obtain:

For the example ''f''(''x'', ''y'') = ''xy'', we obtain:

: ''Ef''(''x'', ''y'', ''dx'', ''dy'') = ''x y'' + ''x dy'' + ''y dx'' + ''dx dy''

: ''Ef''(''x'', ''y'', ''dx'', ''dy'') = ''x y'' + ''x dy'' + ''y dx'' + ''dx dy''

To understand what this means in logical terms, for instance, as expressed in a boolean expansion or a ''disjunctive normal form'' (DNF), it is perhaps a little better to go back and analyze the expression the same way that we did for ''Df''. .Thus, let us compute the value of the enlarged proposition ''Ef'' at each of the points in the universe of discourse ''U'' = ''X''&nbsp;&times;&nbsp;''Y''.

To understand what this means in logical terms, for instance, as expressed in a boolean expansion or a ''disjunctive normal form'' (DNF), it is perhaps a little better to go back and analyze the expression the same way that we did for ''Df''. Thus, let us compute the value of the enlarged proposition ''Ef'' at each of the points in the universe of discourse ''U'' = ''X''&nbsp;&times;&nbsp;''Y''.

<pre>

<pre>

We may understand the enlarged proposition ''Ef'' as telling us all the different ways to reach a model of ''f'' from any point of the universe ''U''.

We may understand the enlarged proposition ''Ef'' as telling us all the different ways to reach a model of ''f'' from any point of the universe ''U''.

To broaden our experience with simple examples, let us now contemplate the sixteen functions of concrete type ''X''&nbsp;&times;&nbsp;''Y''&nbsp;&rarr;&nbsp;'''B''' and abstract type '''B'''&nbsp;&times;&nbsp;'''B'''&nbsp;&rarr;&nbsp;'''B'''. .For future reference, I will set here a few tables that detail the actions of ''E'' and ''D'' and on each of these functions, allowing us to view the results in several different ways.

To broaden our experience with simple examples, let us now contemplate the sixteen functions of concrete type ''X''&nbsp;&times;&nbsp;''Y''&nbsp;&rarr;&nbsp;'''B''' and abstract type '''B'''&nbsp;&times;&nbsp;'''B'''&nbsp;&rarr;&nbsp;'''B'''. For future reference, I will set here a few tables that detail the actions of ''E'' and ''D'' and on each of these functions, allowing us to view the results in several different ways.

By way of initial orientation, Table 1 lists equivalent expressions for the sixteen functions in a number of different languages for zeroth order logic.

By way of initial orientation, Table 1 lists equivalent expressions for the sixteen functions in a number of different languages for zeroth order logic.

<br>

<br>

The next four Tables expand the expressions of ''Ef'' and ''Df'' in two different ways, for each of the sixteen functions. .Notice that the functions are given in a different order, here being collected into a set of seven natural classes.

The next four Tables expand the expressions of ''Ef'' and ''Df'' in two different ways, for each of the sixteen functions. Notice that the functions are given in a different order, here being collected into a set of seven natural classes.

<pre>

<pre>