Difference between revisions of "Directory:Jon Awbrey/Papers/Differential Logic"
Jon Awbrey (talk | contribs) (move material from Directory:Jon Awbrey/Papers/Cactus Language) |
Jon Awbrey (talk | contribs) (→Note 12: markup) |
||
Line 3,077: | Line 3,077: | ||
==Note 12== | ==Note 12== | ||
− | + | '''Erratum''' | |
− | Erratum | ||
Oops! I think that I have just confounded two entirely different issues: | Oops! I think that I have just confounded two entirely different issues: | ||
− | + | ||
− | + | # The substantial difference between right and left regular representations. | |
+ | # The inessential difference between two conventions of presenting matrices. | ||
+ | |||
I will sort this out and correct it later, as need be. | I will sort this out and correct it later, as need be. | ||
− | |||
==Note 13== | ==Note 13== |
Revision as of 18:32, 3 June 2009
Note 1
One of the first things that you can do, once you have a really decent calculus for boolean functions or propositional logic, whatever you want to call it, is to compute the differentials of these functions or propositions.
Now there are many ways to dance around this idea, and I feel like I have tried them all, before one gets down to acting on it, and there many issues of interpretation and justification that we will have to clear up after the fact, that is, before we can be sure that it all really makes any sense, but I think this time I'll just jump in, and show you the form in which this idea first came to me.
Start with a proposition of the form \(x ~\operatorname{and}~ y,\) which is graphed as two labels attached to a root node:
o---------------------------------------o | | | x y | | @ | | | o---------------------------------------o | x and y | o---------------------------------------o |
Written as a string, this is just the concatenation "\(x~y\)".
The proposition \(xy\!\) may be taken as a boolean function \(f(x, y)\!\) having the abstract type \(f : \mathbb{B} \times \mathbb{B} \to \mathbb{B},\) where \(\mathbb{B} = \{ 0, 1 \}\) is read in such a way that \(0\!\) means \(\operatorname{false}\) and \(1\!\) means \(\operatorname{true}.\)
In this style of graphical representation, the value \(\operatorname{true}\) looks like a blank label and the value \(\operatorname{false}\) looks like an edge.
o---------------------------------------o | | | | | @ | | | o---------------------------------------o | true | o---------------------------------------o |
o---------------------------------------o | | | o | | | | | @ | | | o---------------------------------------o | false | o---------------------------------------o |
Back to the proposition \(xy.\!\) Imagine yourself standing in a fixed cell of the corresponding venn diagram, say, the cell where the proposition \(xy\!\) is true, as shown here:
Now ask yourself: What is the value of the proposition \(xy\!\) at a distance of \(dx\!\) and \(dy\!\) from the cell \(xy\!\) where you are standing?
Don't think about it — just compute:
o---------------------------------------o | | | dx o o dy | | / \ / \ | | x o---@---o y | | | o---------------------------------------o | (x + dx) and (y + dy) | o---------------------------------------o |
To make future graphs easier to draw in ASCII, I will use devices like @=@=@
and o=o=o
to identify several nodes into one, as in this next redrawing:
o---------------------------------------o | | | x dx y dy | | o---o o---o | | \ | | / | | \ | | / | | \| |/ | | @=@ | | | o---------------------------------------o | (x + dx) and (y + dy) | o---------------------------------------o |
However you draw it, these expressions follow because the expression \(x + dx,\!\) where the plus sign indicates addition in \(\mathbb{B},\) that is, addition modulo 2, and thus corresponds to the exclusive disjunction operation in logic, parses to a graph of the following form:
o---------------------------------------o | | | x dx | | o---o | | \ / | | @ | | | o---------------------------------------o | x + dx | o---------------------------------------o |
Next question: What is the difference between the value of the proposition \(xy\!\) "over there" and the value of the proposition \(xy\!\) where you are, all expressed as general formula, of course? Here 'tis:
o---------------------------------------o | | | x dx y dy | | o---o o---o | | \ | | / | | \ | | / | | \| |/ x y | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | ((x + dx) & (y + dy)) - xy | o---------------------------------------o |
Oh, I forgot to mention: Computed over \(\mathbb{B},\) plus and minus are the very same operation. This will make the relationship between the differential and the integral parts of the resulting calculus slightly stranger than usual, but never mind that now.
Last question, for now: What is the value of this expression from your current standpoint, that is, evaluated at the point where \(xy\!\) is true? Well, substituting \(1\!\) for \(x\!\) and \(1\!\) for \(y\!\) in the graph amounts to the same thing as erasing those labels:
o---------------------------------------o | | | dx dy | | o---o o---o | | \ | | / | | \ | | / | | \| |/ | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | ((1 + dx) & (1 + dy)) - 1·1 | o---------------------------------------o |
And this is equivalent to the following graph:
o---------------------------------------o | | | dx dy | | o o | | \ / | | o | | | | | @ | | | o---------------------------------------o | dx or dy | o---------------------------------------o |
Note 2
We have just met with the fact that the differential of the and is the or of the differentials.
\(x ~\operatorname{and}~ y \quad \xrightarrow{~\operatorname{Diff}~} \quad dx ~\operatorname{or}~ dy\) |
o---------------------------------------o | | | dx dy | | o o | | \ / | | o | | x y | | | @ --Diff--> @ | | | o---------------------------------------o | x y --Diff--> ((dx)(dy)) | o---------------------------------------o |
It will be necessary to develop a more refined analysis of that 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 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.
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.\!\)
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 : \mathbb{B} \times \mathbb{B} \to \mathbb{B}\) or \(f : \mathbb{B}^2 \to \mathbb{B}.\) 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 \(\{ \texttt{(} x \texttt{)},~ x \} ~=~ \{ \operatorname{not}~ x,~ x \}.\) |
Let \(Y\!\) be the set of values \(\{ \texttt{(} y \texttt{)},~ y \} ~=~ \{ \operatorname{not}~ y,~ y \}.\) |
Then interpret the usual propositions about \(x, y\!\) as functions of the concrete type \(f : X \times Y \to \mathbb{B}.\)
We are going to consider various operators on these functions. Here, an operator \(\operatorname{F}\) is a function that takes one function \(f\!\) into another function \(\operatorname{F}f.\)
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 difference operator \(\Delta,\!\) written here as \(\operatorname{D}.\) |
The enlargement" operator \(\Epsilon,\!\) written here as \(\operatorname{E}.\) |
These days, \(\operatorname{E}\) is more often called the shift operator.
In order to describe the universe in which these operators operate, it is necessary to enlarge the original universe of discourse, passing from the space \(U = X \times Y\) to its differential extension, \(\operatorname{E}U,\) that has the following description:
\(\operatorname{E}U ~=~ U \times \operatorname{d}U ~=~ X \times Y \times \operatorname{d}X \times \operatorname{d}Y,\) |
with
\(\operatorname{d}X = \{ \texttt{(} \operatorname{d}x \texttt{)}, \operatorname{d}x \}\) and \(\operatorname{d}Y = \{ \texttt{(} \operatorname{d}y \texttt{)}, \operatorname{d}y \}.\) |
The interpretations of these new symbols can be diverse, but the easiest option for now is just to say that \(\operatorname{d}x\) means "change \(x\!\)" and \(\operatorname{d}y\) means "change \(y\!\)". To draw the differential extension \(\operatorname{E}U\) of our present universe \(U = X \times Y\) as a venn diagram, it would take us four logical dimensions \(X, Y, \operatorname{d}X, \operatorname{d}Y,\) but we can project a suggestion of what it's about on the universe \(X \times Y\) by drawing arrows that cross designated borders, labeling the arrows as \(\operatorname{d}x\) when crossing the border between \(x\!\) and \(\texttt{(} x \texttt{)}\) and as \(\operatorname{d}y\) when crossing the border between \(y\!\) and \(\texttt{(} y \texttt{)},\) in either direction, in either case.
Propositions can be formed on differential variables, or any combination of ordinary logical variables and differential logical variables, in all the same ways that propositions can be formed on ordinary logical variables alone. For instance, the proposition \(\texttt{(} \operatorname{d}x \texttt{(} \operatorname{d}y \texttt{))}\) may be read to say that \(\operatorname{d}x \Rightarrow \operatorname{d}y,\) in other words, there is "no change in \(x\!\) without a change in \(y\!\)".
Given the proposition \(f(x, y)\!\) in \(U = X \times Y,\) the (first order) enlargement of \(f\!\) is the proposition \(\operatorname{E}f\) in \(\operatorname{E}U\) that is defined by the formula \(\operatorname{E}f(x, y, \operatorname{d}x, \operatorname{d}y) = f(x + \operatorname{d}x, y + \operatorname{d}y).\)
Applying the enlargement operator \(\operatorname{E}\) to the present example, \(f(x, y) = xy,\!\) we may compute the result as follows:
\(\operatorname{E}f(x, y, \operatorname{d}x, \operatorname{d}y) \quad = \quad (x + \operatorname{d}x)(y + \operatorname{d}y).\) |
o---------------------------------------o | | | x dx y dy | | o---o o---o | | \ | | / | | \ | | / | | \| |/ | | @=@ | | | o---------------------------------------o | Ef = (x, dx) (y, dy) | o---------------------------------------o |
Given the proposition \(f(x, y)\!\) in \(U = X \times Y,\) the (first order) difference of \(f\!\) is the proposition \(\operatorname{D}f\) in \(\operatorname{E}U\) that is defined by the formula \(\operatorname{D}f = \operatorname{E}f - f,\) that is, \(\operatorname{D}f(x, y, \operatorname{d}x, \operatorname{d}y) = f(x + \operatorname{d}x, y + \operatorname{d}y) - f(x, y).\)
In the example \(f(x, y) = xy,\!\) the result is:
\(\operatorname{D}f(x, y, \operatorname{d}x, \operatorname{d}y) \quad = \quad (x + \operatorname{d}x)(y + \operatorname{d}y) - xy.\) |
o---------------------------------------o | | | x dx y dy | | o---o o---o | | \ | | / | | \ | | / | | \| |/ x y | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | Df = ((x, dx)(y, dy), xy) | o---------------------------------------o |
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,\!\) that is, at the place where \(x = 1\!\) and \(y = 1.\!\) This evaluation is written in the form \(\operatorname{D}f|_{xy}\) or \(\operatorname{D}f|_{(1, 1)},\) and we arrived at the locally applicable law that is stated and illustrated as follows:
The picture shows the analysis of the inclusive disjunction \(\texttt{((} \operatorname{d}x \texttt{)(} \operatorname{d}y \texttt{))}\) into the following exclusive disjunction:
\(\operatorname{d}x ~\texttt{(} \operatorname{d}y \texttt{)} ~+~ \operatorname{d}y ~\texttt{(} \operatorname{d}x \texttt{)} ~+~ \operatorname{d}x ~\operatorname{d}y.\) |
This resulting differential proposition 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.
Note 3
Last time we computed what will variously be called the difference map, the difference proposition, or the local proposition \(\operatorname{D}f_p\) for the proposition \(f(x, y) = xy\!\) at the point \(p\!\) where \(x = 1\!\) and \(y = 1.\!\)
In the universe \(U = X \times Y,\) the four propositions \(xy,~ x\texttt{(}y\texttt{)},~ \texttt{(}x\texttt{)}y,~ \texttt{(}x\texttt{)(}y\texttt{)}\) 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, 1),~ (1, 0),~ (0, 1),~ (0, 0),\!\) respectively.
Thus we can write \(\operatorname{D}f_p = \operatorname{D}f|p = \operatorname{D}f|(1, 1) = \operatorname{D}f|xy,\) so long as we know the frame of reference in force.
Sticking with the example \(f(x, y) = xy,\!\) let us compute the value of the difference proposition \(\operatorname{D}f\) at all 4 points.
o---------------------------------------o | | | x dx y dy | | o---o o---o | | \ | | / | | \ | | / | | \| |/ x y | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | Df = ((x, dx)(y, dy), xy) | o---------------------------------------o |
o---------------------------------------o | | | dx dy | | o---o o---o | | \ | | / | | \ | | / | | \| |/ | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | Df|xy = ((dx)(dy)) | o---------------------------------------o |
o---------------------------------------o | | | o | | dx | dy | | o---o o---o | | \ | | / | | \ | | / o | | \| |/ | | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | Df|x(y) = (dx) dy | o---------------------------------------o |
o---------------------------------------o | | | o | | | dx dy | | o---o o---o | | \ | | / | | \ | | / o | | \| |/ | | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | Df|(x)y = dx (dy) | o---------------------------------------o |
o---------------------------------------o | | | o o | | | dx | dy | | o---o o---o | | \ | | / | | \ | | / o o | | \| |/ \ / | | o=o-----------o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | @ | | | o---------------------------------------o | Df|(x)(y) = dx dy | o---------------------------------------o |
The easy way to visualize the values of these graphical expressions is just to notice the following equivalents:
o---------------------------------------o | | | x | | o-o-o-...-o-o-o | | \ / | | \ / | | \ / | | \ / x | | \ / o | | \ / | | | @ = @ | | | o---------------------------------------o | (x, , ... , , ) = (x) | o---------------------------------------o |
o---------------------------------------o | | | o | | x_1 x_2 x_k | | | o---o-...-o---o | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / x_1 ... x_k | | @ = @ | | | o---------------------------------------o | (x_1, ..., x_k, ()) = x_1 · ... · x_k | o---------------------------------------o |
Laying out the arrows on the augmented venn diagram, one gets a picture of a differential vector field.
o---------------------------------------o | | | dx dy | | ^ | | o | o | | / \ | / \ | | / \|/ \ | | /dy | dx\ | | /(dx) /|\ (dy)\ | | / ^ /`|`\ ^ \ | | / \``|``/ \ | | / /`\`|`/`\ \ | | / /```\|/```\ \ | | o x o`````o`````o y o | | \ \`````````/ / | | \ o---->```<----o / | | \ dy \``^``/ dx / | | \(dx) \`|`/ (dy)/ | | \ \|/ / | | \ | / | | \ /|\ / | | \ / | \ / | | o | o | | | | | dx | dy | | o | | | o---------------------------------------o |
The Figure shows the points of the extended universe \(\operatorname{E}U = X \times Y \times \operatorname{d}X \times \operatorname{d}Y\) that satisfy the difference proposition \(\operatorname{D}f,\) namely, these:
\(\begin{array}{rcccc} 1. & x & y & dx & dy \\ 2. & x & y & dx & (dy) \\ 3. & x & y & (dx) & dy \\ 4. & x & (y) & (dx) & dy \\ 5. & (x) & y & dx & (dy) \\ 6. & (x) & (y) & dx & dy \end{array}\) |
An inspection of these six points should make it easy to understand \(\operatorname{D}f\) as telling you what you have to do from each point of \(U\!\) in order to change the value borne by the proposition \(f(x, y).\!\)
Note 4
We have been studying the action of the difference operator \(\operatorname{D},\) also known as the localization operator, on the proposition \(f : X \times Y \to \mathbb{B}\) that is commonly known as the conjunction \(x \cdot y.\) We described \(\operatorname{D}f\) as a (first order) differential proposition, that is, a proposition of the type \(\operatorname{D}f : X \times Y \times \operatorname{d}X \times \operatorname{d}Y \to \mathbb{B}.\) Abstracting from the augmented venn diagram that illustrates how the models or satisfying interpretations of \(\operatorname{D}f\) distribute within the extended universe \(\operatorname{E}U = X \times Y \times \operatorname{d}X \times \operatorname{d}Y,\) we can depict \(\operatorname{D}f\) in the form of a digraph or directed graph, one whose points are labeled with the elements of \(U = X \times Y\) and whose arrows are labeled with the elements of \(\operatorname{d}U = \operatorname{d}X \times \operatorname{d}Y.\)
o---------------------------------------o | | | x · y | | | | o | | ^^^ | | / | \ | | (dx)· dy / | \ dx ·(dy) | | / | \ | | / | \ | | v | v | | x ·(y) o | o (x)· y | | | | | | | | dx · dy | | | | | | | | v | | o | | | | (x)·(y) | | | o---------------------------------------o | | | f = x y | | | | Df = x y · ((dx)(dy)) | | | | + x (y) · (dx) dy | | | | + (x) y · dx (dy) | | | | + (x)(y) · dx dy | | | o---------------------------------------o |
Any proposition worth its salt, as they say, has many equivalent ways to look at it, any of which may reveal some unsuspected aspect of its meaning. We will encounter more and more of these alternative readings as we go.
Note 5
The enlargement or shift operator \(\operatorname{E}\) exhibits a wealth of interesting and useful properties in its own right, so it pays to examine a few of the more salient features that play out on the surface of our initial example, \(f(x, y) = xy.\!\)
A suitably generic definition of the extended universe of discourse is afforded by the following set-up: