Quickly add a free MyWikiBiz directory listing!

MyWikiBiz, Author Your Legacy — Friday August 29, 2008

This article develops a differential extension of propositional calculus and applies it to a context of problems arising in dynamic systems. The work pursued here is coordinated with a parallel application that focuses on neural network systems, but the dependencies are arranged to make the present article the main and the more self-contained work, to serve as a conceptual frame and a technical background for the network project.

Review and Transition

This note continues a previous discussion on the problem of dealing with change and diversity in logic-based intelligent systems. It is useful to begin by summarizing essential material from previous reports.

Table 1 outlines a notation for propositional calculus based on two types of logical connectives, both of variable -ary scope.

• A bracketed list of propositional expressions in the form indicates that exactly one of the propositions is false.

• A concatenation of propositional expressions in the form indicates that all of the propositions are true, in other words, that their logical conjunction is true.

All other propositional connectives can be obtained in a very efficient style of representation through combinations of these two forms. Strictly speaking, the concatenation form is dispensable in light of the bracketed form, but it is convenient to maintain it as an abbreviation of more complicated bracket expressions.

This treatment of propositional logic is derived from the work of C.S. Peirce [P1, P2], who gave this approach an extensive development in his graphical systems of predicate, relational, and modal logic [Rob]. More recently, these ideas were revived and supplemented in an alternative interpretation by George Spencer-Brown [SpB]. Both of these authors used other forms of enclosure where I use parentheses, but the structural topologies of expression and the functional varieties of interpretation are fundamentally the same.

While working with expressions solely in propositional calculus, it is easiest to use plain parentheses for logical connectives. In contexts where parentheses are needed for other purposes barred parentheses may be used for logical operators.

The briefest expression for logical truth is the empty word, usually denoted by or in formal languages, where it forms the identity element for concatenation. To make it visible in this text, it may be denoted by the equivalent expression "", or, especially if operating in an algebraic context, by a simple "". Also when working in an algebraic mode, the plus sign "" may be used for exclusive disjunction. For example, we have the following paraphrases of algebraic expressions by bracket expressions:

It is important to note that the last expressions are not equivalent to the triple bracket

Table 1. Syntax and Semantics of a Calculus for Propositional Logic

Expression	Interpretation	Other Notations

Note. The usage that one often sees, of a plus sign "" to represent inclusive disjunction, and the reference to this operation as boolean addition, is a misnomer on at least two counts. Boole used the plus sign to represent exclusive disjunction (at any rate, an operation of aggregation restricted in its logical interpretation to cases where the represented sets are disjoint (Boole, 32)), as any mathematician with a sensitivity to the ring and field properties of algebra would do:

The expression seems indeed uninterpretable, unless it be assumed that the things represented by and the things represented by are entirely separate; that they embrace no individuals in common. (Boole, 66).

It was only later that Peirce and Jevons treated inclusive disjunction as a fundamental operation, but these authors, with a respect for the algebraic properties that were already associated with the plus sign, used a variety of other symbols for inclusive disjunction (Sty, 177, 189). It seems to have been Schröder who later reassigned the plus sign to inclusive disjunction (Sty, 208). Additional information, discussion, and references can be found in (Boole) and (Sty, 177–263). Aside from these historical points, which never really count against a current practice that has gained a life of its own, this usage does have a further disadvantage of cutting or confounding the lines of communication between algebra and logic. For this reason, it will be avoided here.

A Functional Conception of Propositional Calculus

In the general case, we start with a set of logical features that represent properties of objects or propositions about the world. In concrete examples the features commonly appear as capital letters from an alphabet like or as meaningful words from a linguistic vocabulary of codes. This language can be drawn from any sources, whether natural, technical, or artificial in character and interpretation. In the application to dynamic systems we tend to use the letters as our coordinate propositions, and to interpret them as denoting properties of a system's state, that is, as propositions about its location in configuration space. Because I have to consider non-deterministic systems from the outset, I often use the word state in a loose sense, to denote the position or configuration component of a contemplated state vector, whether or not it ever gets a deterministic completion.

The set of logical features provides a basis for generating an -dimensional universe of discourse that I denote as It is useful to consider each universe of discourse as a unified categorical object that incorporates both the set of points and the set of propositions that are implicit with the ordinary picture of a venn diagram on features. Thus, we may regard the universe of discourse as an ordered pair having the type and we may abbreviate this last type designation as or even more succinctly as (Used this way, the angle brackets are referred to as generator brackets.)

Table 2 exhibits the scheme of notation I use to formalize the domain of propositional calculus, corresponding to the logical content of truth tables and venn diagrams. Although it overworks the square brackets a bit, I also use either one of the equivalent notations or to denote the data type of a finite set on elements.

Table 2. Propositional Calculus : Basic Notation

Symbol	Notation	Description	Type
	“”  “”

Qualitative Logic and Quantitative Analogy

These concepts and notations may now be explained in greater detail. In order to begin as simply as possible, let us distinguish two levels of analysis and set out initially on the easier path. On the first level of analysis we take spaces like and at face value and treat them as the primary objects of interest. On the second level of analysis we use these spaces as coordinate charts for talking about points and functions in more fundamental spaces.

A pair of spaces, of types and give typical expression to everything that we commonly associate with the ordinary picture of a venn diagram. The dimension, counts the number of "circles" or simple closed curves that are inscribed in the universe of discourse, corresponding to its relevant logical features or basic propositions. Elements of type correspond to what are often called propositional interpretations in logic, that is, the different assignments of truth values to sentence letters. Relative to a given universe of discourse, these interpretations are visualized as its cells, in other words, the smallest enclosed areas or undivided regions of the venn diagram. The functions correspond to the different ways of shading the venn diagram to indicate arbitrary propositions, regions, or sets. Regions included under a shading indicate the models, and regions excluded represent the non-models of a proposition. To recognize and formalize the natural cohesion of these two layers of concepts into a single universe of discourse, we introduce the type notations to stand for the pair of types The resulting "stereotype" serves to frame the universe of discourse as a unified categorical object, and makes it subject to prescribed sets of evaluations and transformations (categorical morphisms or arrows) that affect the universe of discourse as an integrated whole.

Most of the time we can serve the algebraic, geometric, and logical interests of our study without worrying about their occasional conflicts and incidental divergences. The conventions and definitions already set down will continue to cover most of the algebraic and functional aspects of our discussion, but to handle the logical and qualitative aspects we will need to add a few more. In general, abstract sets may be denoted by gothic, greek, or script capital variants of and so on, with their elements being denoted by a corresponding set of subscripted letters in plain lower case, for example, Most of the time, a set such as will be employed as the alphabet of a formal language. These alphabet letters serve to name the logical features (properties or propositions) that generate a particular universe of discourse. When we want to discuss the particular features of a universe of discourse, beyond the abstract designation of a type like then we may use the following notations. If is an alphabet of logical features, then is the set of interpretations, is the set of propositions, and is the combination of these interpretations and propositions into the universe of discourse that is based on the features

As always, especially in concrete examples, these rules may be dropped whenever necessary, reverting to a free assortment of feature labels. However, when we need to talk about the logical aspects of a space that is already named as a vector space, it will be necessary to make special provisions. At any rate, these elaborations can be deferred until actually needed.

Philosophy of Notation : Formal Terms and Flexible Types

For much of our discussion propositions and boolean functions are treated as the same formal objects, or as different interpretations of the same formal calculus. This rule of interpretation has exceptions, though. There is a distinctively logical interest in the use of propositional calculus that is not exhausted by its functional interpretation. It is part of our task in this study to deal with these uniquely logical characteristics as they present themselves both in our subject matter and in our formal calculus. Just to provide a hint of what's at stake: In logic, as opposed to the more imaginative realms of mathematics, we consider it a good thing to always know what we are talking about. Where mathematics encourages tolerance for uninterpreted symbols as intermediate terms, logic exerts a keener effort to interpret directly each oblique carrier of meaning, no matter how slight, and to unfold the complicities of every indirection in the flow of information. Translated into functional terms, this means that we want to maintain a continual, immediate, and persistent sense of both the converse relation or what is the same thing, and the fibers or inverse images and associated with each boolean function that we use. In practical terms, the desired implementation of a propositional interpreter should incorporate our intuitive recognition that the induced partition of the functional domain into level sets for is part and parcel of understanding the denotative uses of each propositional function

Special Classes of Propositions

It is important to remember that the coordinate propositions besides being projection maps are propositions on an equal footing with all others, even though employed as a basis in a particular moment. This set of propositions may sometimes be referred to as the basic propositions, the coordinate propositions, or the simple propositions that found a universe of discourse. Either one of the equivalent notations, or may be used to indicate the adoption of the propositions as a basis for describing a universe of discourse.

Among the propositions in are several families of propositions each that take on special forms with respect to the basis Three of these families are especially prominent in the present context, the linear, the positive, and the singular propositions. Each family is naturally parameterized by the coordinate -tuples in and falls into ranks, with a binomial coefficient giving the number of propositions that have rank or weight

• The linear propositions, may be written as sums:

• The positive propositions, may be written as products:

• The singular propositions, may be written as products:

In each case the rank ranges from to and counts the number of positive appearances of the coordinate propositions in the resulting expression. For example, for the linear proposition of rank is the positive proposition of rank is and the singular proposition of rank is

The basic propositions are both linear and positive. So these two kinds of propositions, the linear and the positive, may be viewed as two different ways of generalizing the class of basic propositions.

Linear propositions and positive propositions are generated by taking boolean sums and products, respectively, over selected subsets of basic propositions, so both families of propositions are parameterized by the powerset that is, the set of all subsets of the basic index set

Let us define as the subset of that is given by Then we may comprehend the action of the linear and the positive propositions in the following terms:

• The linear proposition evaluates each cell of by looking at the coefficients of with respect to the features that "likes", namely those in and then adds them up in Thus, computes the parity of the number of features that has in yielding one for odd and zero for even. Expressed in this idiom, says that seems odd (or oddly true) to whereas says that seems even (or evenly true) to so long as we recall that zero times is evenly often, too.

• The positive proposition evaluates each cell of by looking at the coefficients of with regard to the features that "likes", namely those in and then takes their product in Thus, assesses the unanimity of the multitude of features that has in yielding one for all and aught for else. In these consensual or contractual terms, means that is AOK or congruent with all of the conditions of while means that defaults or dissents from some condition of

Basis Relativity and Type Ambiguity

Finally, two things are important to keep in mind with regard to the simplicity, linearity, positivity, and singularity of propositions.

First, all of these properties are relative to a particular basis. For example, a singular proposition with respect to a basis will not remain singular if is extended by a number of new and independent features. Even if we stick to the original set of pairwise options to select a new basis, the sets of linear and positive propositions are determined by the choice of simple propositions, and this determination is tantamount to the conventional choice of a cell as origin.

Second, the singular propositions picking out as they do a single cell or a coordinate tuple of become the carriers or the vehicles of a certain type-ambiguity that vacillates between the dual forms and and infects the whole hierarchy of types built on them. In other words, the terms that signify the interpretations and the singular propositions are fully equivalent in information, and this means that every token of the type can be reinterpreted as an appearance of the subtype And vice versa, the two types can be exchanged with each other everywhere that they turn up. In practical terms, this allows the use of singular propositions as a way of denoting points, forming an alternative to coordinate tuples.

For example, relative to the universe of discourse the singular proposition could be explicitly retyped as to indicate the point ‹1, 1, 1›, but in most cases the proper interpretation could be gathered from context. Both notations remain dependent on a particular basis, but the code that is generated under the singular option has the advantage in its self-commenting features, in other words, it constantly reminds us of its basis in the process of denoting points. When the time comes to put a multiplicity of different bases into play, and to search for objects and properties that remain invariant under the transformations between them, this infinitesimal potential advantage may well evolve into an overwhelming practical necessity.

The Analogy Between Real and Boolean Types

There are two further reasons why it useful to spend time on a careful treatment of types, and they both have to do with our being able to take full computational advantage of certain dimensions of flexibility in the types that apply to terms. First, the domains of differential geometry and logic programming are connected by analogies between real and boolean types of the same pattern. Second, the types involved in these patterns have important isomorphisms connecting them that apply on both the real and the boolean sides of the picture.

Amazingly enough, these isomorphisms are themselves schematized by the axioms and theorems of propositional logic. This fact is known as the propositions as types analogy or the Curry–Howard isomorphism [How]. In another formulation it says that terms are to types as proofs are to propositions. See [LaS, 42–46] and [SeH] for a good discussion and further references. To anticipate the bearing of these issues on our immediate topic, Table 3 sketches a partial overview of the Real to Boolean analogy that may serve to illustrate the paradigm in question.

Table 3. Analogy Between Real and Boolean Types

	"
	"

The Table exhibits a sample of likely parallels between the real and boolean domains. The central column gives a selection of terminology that is borrowed from differential geometry and extended in its meaning to the logical side of the Table. These are the varieties of spaces that come up when we turn to analyzing the dynamics of processes that pursue their courses through the states of an arbitrary space Moreover, when it becomes necessary to approach situations of overwhelming dynamic complexity in a succession of qualitative reaches, then the methods of logic that are afforded by the boolean domains, with their declarative means of synthesis and deductive modes of analysis, supply a natural battery of tools for the task.

It is usually expedient to take these spaces two at a time, in dual pairs of the form and In general, one creates pairs of type schemas by replacing any space with its dual for example, pairing the type with the type and with The word dual is used here in its broader sense to mean all of the functionals, not just the linear ones. Given any function the converse or inverse relation corresponding to is denoted and the subsets of that are defined by taken over in are called the fibers or the level sets of the function

Theory of Control and Control of Theory

In the boolean context a function is tantamount to a proposition about elements of and the elements of constitute the interpretations of that proposition. The fiber comprises the set of models of or examples of elements in satisfying the proposition The fiber collects the complementary set of anti-models, or the exceptions to the proposition that exist in Of course, the space of functions is isomorphic to the set of all subsets of called the power set of and often denoted or

The operation of replacing by in a type schema corresponds to a certain shift of attitude towards the space in which one passes from a focus on the ostensibly individual elements of to a concern with the states of information and uncertainty that one possesses about objects and situations in The conceptual obstacles in the path of this transition can be smoothed over by using singular functions as stepping stones. First of all, it's an easy step from an element of type to the equivalent information of a singular proposition and then only a small jump of generalization remains to reach the type of an arbitrary proposition perhaps understood to indicate a relaxed constraint on the singularity of points or a neighborhood circumscribing the original This is frequently a useful transformation, communicating between the objective and the intentional perspectives, in spite perhaps of the open objection that this distinction is transient in the mean time and ultimately superficial.

It is hoped that this measure of flexibility, allowing us to stretch a point into a proposition, can be useful in the examination of inquiry driven systems, where the differences between empirical, intentional, and theoretical propositions constitute the discrepancies and the distributions that drive experimental activity. I can give this model of inquiry a cybernetic cast by realizing that theory change and theory evolution, as well as the choice and the evaluation of experiments, are actions that are taken by a system or its agent in response to the differences that are detected between observational contents and theoretical coverage.

All of the above notwithstanding, there are several points that distinguish these two tasks, namely, the theory of control and the control of theory, features that are often obscured by too much precipitation in the quickness with which we understand their similarities. In the control of uncertainty through inquiry, some of the actuators that we need to be concerned with are axiom changers and theory modifiers, operators with the power to compile and to revise the theories that generate expectations and predictions, effectors that form and edit our grammars for the languages of observational data, and agencies that rework the proposed model to fit the actual sequences of events and the realized relationships of values that are observed in the environment. Moreover, when steps must be taken to carry out an experimental action, there must be something about the particular shape of our uncertainty that guides us in choosing what directions to explore, and this impression is more than likely influenced by previous accumulations of experience. Thus it must be anticipated that much of what goes into scientific progress, or any sustainable effort toward a goal of knowledge, is necessarily predicated on long term observation and modal expectations, not only on the more local or short term prediction and correction.

Propositions as Types and Higher Order Types

The types collected in Table 3 (repeated below) serve to illustrate the themes of higher order propositional expressions and the propositions as types (PAT) analogy.

Table 3. Analogy Between Real and Boolean Types

	"
	"

First, observe that the type of a tangent vector at a point, also known as a directional derivative at that point, has the form where is the chosen ground field, in the present case either or At a point in a space of type a directional derivative operator takes a function on that space, an of type and maps it to a ground field value of type This value is known as the derivative of in the direction [Che46, 76–77]. In the boolean case has the form of a proposition about propositions, in other words, a proposition of the next higher type.

Next, by way of illustrating the propositions as types idea, consider a proposition of the form One knows from propositional calculus that this is logically equivalent to a proposition of the form But this equivalence should remind us of the functional isomorphism that exists between a construction of the type and a construction of the type The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows "" and products "" with the respective logical arrows "" and products "". 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 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 that assigns to each point of the space a tangent vector to at that point, namely, the tangent vector [Che46, 82–83]. If is of the type then is of the type This has the pattern with and

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 4. Observe how the function associated with the place of in the pattern, moves through its paces from the second to the first position. In this way, the vector field initially viewed as attaching each tangent vector to the site where it acts in now comes to be seen as acting on each scalar potential like a generalized species of differentiation, producing another function of the same type.

Table 4. An Equivalence Based on the Propositions as Types Analogy

Reality at the Threshold of Logic

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 5. A Bridge Over Troubled Waters

The left side of the Table collects mostly standard notation for an -dimensional vector space over a field 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 with a special interest in the continuous line to the qualitative and discrete situations that are instanced and typified by

I now proceed to explain these concepts in more detail. The most important ideas developed in Table 5 are these:

• The idea of a universe of discourse, which includes both a space of points and a space of maps on those points.

• The idea of passing from a more complex universe to a simpler universe by a process of thresholding each dimension of variation down to a single bit of information.

For the sake of concreteness, let us suppose that we start with a continuous -dimensional vector space like The coordinate system is a set of maps also known as the coordinate projections. Given a "dataset" of points in there are numerous ways of sensibly reducing the data down to one bit for each dimension. One strategy that is general enough for our present purposes is as follows. For each we choose an -ary relation on that is, a subset of and then we define the threshold map, or limen as follows:

In other notations that are sometimes used, the operator or the corner brackets can be used to denote a characteristic function, that is, a mapping from statements to their truth values in Finally, it is not uncommon to use the name of the relation itself as a predicate that maps -tuples into truth values. Thus we have the following notational variants of the above definition:

Notice that, as defined here, there need be no actual relation between the -dimensional subsets and the coordinate axes corresponding to aside from the circumstance that the two sets have the same cardinality. In concrete cases, though, one usually has some reason for associating these "volumes" with these "lines", for instance, is bounded by some hyperplane that intersects the axis at a unique threshold value Often, the hyperplane is chosen normal to the axis. In recognition of this motive, let us make the following convention. When the set has points on the axis, that is, points of the form ‹  › where only the coordinate is possibly non-zero, we may pick any one of these coordinate values as a parametric index of the relation. In this case we say that the indexing is real, otherwise the indexing is imaginary. For a knowledge based system this should serve once again to mark the distinction between acquaintance and opinion.

States of knowledge about the location of a system or about the distribution of a population of systems in a state space can now be expressed by taking the set as a basis of logical features. In picturesque terms, one may think of the underscore and the subscript as combining to form a subtextual spelling for the threshold map. This can help to remind us that the threshold operator acts on by setting up a kind of a "hurdle" for it. In this interpretation the coordinate proposition asserts that the representative point resides above the threshold.

Primitive assertions of the form may then be negated and joined by means of propositional connectives in the usual ways to provide information about the state of a contemplated system or a statistical ensemble of systems. Parentheses may be used to indicate logical negation. Eventually one discovers the usefulness of the -ary just one false operators of the form , as treated in earlier reports. This much tackle generates a space of points (cells, interpretations), and a space of functions (regions, propositions), Together these form a new universe of discourse of the type which we may abbreviate as or most succinctly as

The square brackets have been chosen to recall the rectangular frame of a venn diagram. In thinking about a universe of discourse it is a good idea to keep this picture in mind, graphically illustrating the links among the elementary cells the defining features and the potential shadings all at the same time, not to mention the arbitrariness of the way we choose to inscribe our distinctions in the medium of a continuous space.

Finally, let denote the space of linear functions, which has in the finite case the same dimensionality as and let the same notation be extended across the Table.

We have just gone through a lot of work, apparently doing nothing more substantial than spinning a complex spell of notational devices through a labyrinth of baffled spaces and baffling maps. The reason for doing this was to bind together and to constitute the intuitive concept of a universe of discourse into a coherent categorical object, the kind of thing, once grasped, that can be turned over in the mind and considered in all its manifold changes and facets. The effort invested in these preliminary measures is intended to pay off later, when we need to consider the state transformations and the time evolution of neural network systems.

Tables of Propositional Forms

To prepare for the next phase of discussion, Tables 6 and 7 collect and summarize all of the propositional forms on one and two variables. These propositional forms are represented over bases of boolean variables as complete sets of boolean-valued functions. Adjacent to their names and specifications are listed what are roughly the simplest expressions in the cactus language, the particular syntax for propositional calculus that I use in formal and computational contexts. For the sake of orientation, the English paraphrases and the more common notations are listed in the last two columns. As simple and circumscribed as these low-dimensional universes may appear to be, a careful exploration of their differential extensions will involve us in complexities sufficient to demand our attention for some time to come.

Propositional forms on one variable correspond to boolean functions In Table 6 these functions are listed in a variant form of truth table, one in which the axes of the usual arrangement are rotated through a right angle. Each function is indexed by the string of values that it takes on the points of the universe The binary index generated in this way is converted to its decimal equivalent and these are used as conventional names for the as shown in the first column of the Table. In their own right the points of the universe are coordinated as a space of type this in light of the universe being a functional domain where the coordinate projection takes on its values in

Table 6. Propositional Forms on One Variable

Propositional forms on two variables correspond to boolean functions In Table 7 each function is indexed by the values that it takes on the points of the universe Converting the binary index thus generated to a decimal equivalent, we obtain the functional nicknames that are listed in the first column. The points of the universe are coordinated as a space of type as indicated under the heading of the Table, where the coordinate projections and run through the various combinations of their values in

Table 7. Propositional Forms on Two Variables