Inquiry Into Inquiry

Re: Theme One Program • Exposition (1) (2) (3) (4)
Re: Theme One Program • Discussion (7)
Re: Ontolog Forum • Alex Shkotin (1) (2)
Re: Logical Graphs • Animated Proofs

AS:

The animation is mesmerizing:  I would watch and watch.  But without the pause, next frame, and playback speed settings, it’s just a work of art that calls to see it step by step.

And on [the following] page you start with the double negation theorem.

• Propositional Equation Reasoning Systems

Have a look at a few of my comments as a reader, and only on the graph topic taken separately.

Dear Alex,

Thanks for viewing the animations and taking the time to work through that first proof.  Clearly a lot could be done to improve the production values — what you see is what I got with whatever app I had umpteen years ago.

For the time being I’m focusing on the implementation layer of the Theme One Program, which combines a learning component and a reasoning component.  The first implements a two‑level sequence learner and the second implements a propositional calculator based on a variant of Peirce’s logical graphs.  (I meant to say more about the learning function this time around but I’m still working up to tackling that.)

To address your comments and questions we’ll need to step back for a moment to a more abstract, implementation-independent treatment of logical graphs.  There’s a number of resources along that line linked on the following Survey page.

• Survey of Animated Logical Graphs

The post “Logical Graphs • Formal Development” gives a quick but systematic account of the formal system I use throughout.  The OEIS wiki article “Logical Graphs” gives a more detailed development.

Here’s an excerpt from the above discussions, giving the four axioms or “initials” which serve as graphical transformation rules, in effect, the equational inference rules used to generate proofs and establish theorems or “consequences”.

Axioms

The formal system of logical graphs is defined by a foursome of formal equations, called initials when regarded purely formally, in abstraction from potential interpretations, and called axioms when interpreted as logical equivalences.  There are two arithmetic initials and two algebraic initials, as shown below.

Arithmetic Initials

Algebraic Initials

The statement of the Double Negation Theorem is shown below.

C₁.  Double Negation Theorem

The first theorem goes under the names of Consequence 1 (C₁), the double negation theorem (DNT), or Reflection.

The following proof is adapted from the one given by George Spencer Brown in his book Laws of Form (LOF) and credited to two of his students, John Dawes and D.A. Utting.

That should fill in enough background to get started on your questions …

Resources

• Theme One Program • Overview
• Theme One Program • Exposition
• Theme One Program • User Guide
• Theme One Program • Survey Page

cc: Conceptual Graphs • Cybernetics • Laws of Form • Ontolog Forum
cc: FB | Theme One Program • Structural Modeling • Systems Science

Re: Theme One Program • Exposition (1) (2) (3) (4)
Re: Ontolog Forum • Alex Shkotin

AS:

As we both like digraphs and looking at your way of rendering, let me share my lazy way of using Graphviz on one of the last pictures produced.

This is a picture of a derivation tree (aka AST) for the text of four statements of context-free grammar of some kind.  It is important that this is a digraph with ordered children, and nodes have some attributes.  In your case attributes are   In my case attributes are:

• node id,
• nonterminal,
• for syntactic nonterminal:  rule id used for derivation,
• for lexical nonterminal:  value taken from text.

Dear Alex,

Many thanks, the Graphviz suite looks very nice and I will spend some time looking through the docs.  I kept a few samples of my old ASCII graphics, mostly out of a sense of nostalgia, but I’ve reached a point in reworking my Theme One Exposition where I need to upgrade the graphics.  My original aim was to have the program display its own visuals, but it doesn’t look like I’ll be the one doing that.  Visualizing proof requires animation — I used to have an app for that bundled with CorelDraw but it quit working in a previous platform change and I haven’t gotten around to hunting up a new one.  At any rate, there’s a sampler of animated proofs in logical graphs on the following page.

• Proof Animations

Resources

• Theme One Program • Overview
• Theme One Program • Exposition
• Theme One Program • User Guide
• Theme One Program • Survey Page

cc: Conceptual Graphs • Cybernetics • Laws of Form • Ontolog Forum
cc: FB | Theme One Program • Structural Modeling • Systems Science

Lexical, Literal, Logical

Theme One puts cactus graphs to work in three distinct but related ways, called lexical, literal, and logical applications.  The three modes of operation employ three distinct but overlapping subsets of the broader species of cacti.  Accordingly we find ourselves working with graphs, expressions, and files of lexical, literal, and logical types, depending on the task at hand.

The logical class of cacti is the broadest, encompassing the whole species described above, of which we have already seen a typical example in its several avatars as abstract graph, pointer data structure, and string of characters suitable for storage in a text file.

Being a logical cactus is not just a matter of syntactic form — it means being subject to meaningful interpretations as a sign of a logical proposition.  To enter the logical arena cactus expressions must express something, a proposition true or false of something.

Fully addressing the logical, interpretive, semantic aspect of cactus graphs normally requires a mind-boggling mass of preliminary work on the details of their syntactic structure.  Practical, pragmatic, and especially computational considerations will eventually make that unavoidable.  For the sake of the present discussion, however, let’s put that on hold and fast forward to the logical substance.

Resources

• Theme One Program • Overview
• Theme One Program • Exposition
• Theme One Program • User Guide

cc: Conceptual Graphs • Cybernetics • Laws of Form • Ontolog Forum
cc: FB | Theme One Program • Structural Modeling • Systems Science

Parsing Logical Graphs

It is possible to write a program that parses cactus expressions into reasonable facsimiles of cactus graphs as pointer structures in computer memory, making edges correspond to addresses and nodes correspond to records.  I did just that in the early forerunners of the present program, but it turned out to be a more robust strategy in the long run, despite the need for additional nodes at the outset, to implement a more articulate but more indirect parsing algorithm, one in which the punctuation marks are not just tacitly converted to addresses in passing, but instead recorded as nodes in roughly the same way as the ordinary identifiers, or paints.

Figure 3 illustrates the type of parsing paradigm used by the program, showing the pointer graph structure obtained by parsing the cactus expression in Figure 2.  A traversal of this graph naturally reconstructs the cactus string that parses into it.

The pointer graph in Figure 3, namely, the parse graph of a cactus expression, is the sort of thing we’ll probably not be able to resist calling a cactus graph, for all the looseness of that manner of speaking, but we should keep in mind its level of abstraction lies a step further in the direction of a concrete implementation than the last thing we called by that name.  While we have them before our mind’s eyes, there are several other distinctive features of cactus parse graphs we ought to notice before moving on.

In terms of idea-form structures, a cactus parse graph begins with a root idea pointing into a by‑cycle of forms, each of whose sign fields bears either a paint, in other words, a direct or indirect identifier reference, or an opening left parenthesis indicating a link to a subtended lobe of the cactus.

A lobe springs from a form whose sign field bears a left parenthesis.  That stem form has an on idea pointing into a by‑cycle of forms, exactly one of which has a sign field bearing a right parenthesis.  That last form has an on idea pointing back to the form bearing the initial left parenthesis.

In the case of a lobe, aside from the single form bearing the closing right parenthesis, the by‑cycle of a lobe may list any number of forms, each of whose sign fields bears either a comma, a paint, or an opening left parenthesis signifying a link to a more deeply subtended lobe.

Just to draw out one of the implications of this characterization and to stress the point of it, the root node can be painted and bear many lobes, but it cannot be segmented, that is, the by‑cycle corresponding to the root node can bear no commas.

Resources

• Theme One Program • Overview
• Theme One Program • Exposition
• Theme One Program • User Guide

cc: Conceptual Graphs • Cybernetics • Laws of Form • Ontolog Forum
cc: FB | Theme One Program • Structural Modeling • Systems Science

Coding Logical Graphs

My earliest experiments coding logical graphs as dynamic “pointer” data structures taught me that conceptual and computational efficiencies of a critical sort could be achieved by generalizing their abstract graphs from trees to the variety graph theorists know as cacti.  The genesis of that generalization is a tale worth telling another time, but for now it’s best to jump right in and proceed by way of generic examples.

Figure 1 shows a typical example of a painted and rooted cactus.

Figure 2 shows a way to visualize the correspondence between cactus graphs and cactus strings, demonstrated on the cactus from Figure 1.  By way of convenient terminology, the polygons of a cactus graph are called its lobes.  An edge not part of a larger polygon is called a 2‑gon or a bi‑gon.  A terminal bi‑gon is called a spike.

The correspondence between a cactus graph and a cactus string is obtained by an operation called traversing the graph in question.

• One traverses a cactus graph by beginning at the left hand side of the root node, reading off the list of paints one encounters at that point.  Since the order of elements at any node is not significant, one may start the cactus string with that list of paints or save them for the end.  We have done the latter in this case.
• One continues by climbing up the left hand side of the leftmost lobe, marking the ascent by means of a left parenthesis, traversing whatever cactus one happens to reach at the first node above the root, that done, proceeding from left to right along the top side of the lobe, marking each interlobal span by means of a comma, traversing each cactus in turn one meets along the way, on completing the last of them climbing down the right hand side of the lobe, marking the descent by means of a right parenthesis, and then traversing each cactus in turn, in left to right order, that is incident with the root node.

The string of letters, parentheses, and commas one obtains by this procedure is called the traversal string of the graph, in this case, a cactus string.

Resources

• Theme One Program • Overview
• Theme One Program • Exposition
• Theme One Program • User Guide

cc: Conceptual Graphs • Cybernetics • Laws of Form • Ontolog Forum
cc: FB | Theme One Program • Structural Modeling • Systems Science

The previous post described the elementary data structure used to represent nodes of graphs in the Theme One program.  This post describes the specific family of graphs employed by the program.

Painted And Rooted Cacti

Figure 1 shows a typical example of a painted and rooted cactus.

The graph itself is a mathematical object and does not inhabit the page or other medium before our eyes, and it must not be confused with any picture or other representation of it, anymore than we’d want someone to confuse us with a picture of ourselves, but it’s a fair enough picture, once we understand the conventions of representation involved.

Let be the set of nodes in a graph and let be a set of identifiers.  We often find ourselves in situations where we have to consider many different ways of associating the nodes of with the identifiers in   Various manners of associating nodes with identifiers have been given conventional names by different schools of graph theorists.  I will give one way of describing a few of the most common patterns of association.

• A graph is painted if there is a relation between its node set and a set of identifiers, in which case the relation is called a painting and the identifiers are called paints.
• A graph is colored if there is a function from its node set to a set of identifiers, in which case the function is called a coloring and the identifiers are called colors.
• A graph is labeled if there is a one-to-one mapping between its node set and a set of identifiers, in which case the mapping is called a labeling and the identifiers are called labels.
• A graph is said to be rooted if it has a unique distinguished node, in which case the distinguished node is called the root of the graph.  The graph in Figure 1 has a root node marked by the “at” sign or amphora symbol “”.

The graph in Figure 1 has eight nodes plus the five paints in the set   The painting of nodes is indicated by drawing the paints of each node next to the node they paint.  Observe that some nodes may be painted with an empty set of paints.

The structure of a painted and rooted cactus can be encoded in the form of a character string called a painted and rooted cactus expression.  For the remainder of this discussion the terms cactus and cactus expression will be used to mean the painted and rooted varieties.  A cactus expression is formed on an alphabet consisting of the relevant set of identifiers, the paints, together with three punctuation marks:  the left parenthesis, the comma, and the right parenthesis.

Resources

• Theme One Program • Overview
• Theme One Program • Exposition
• Theme One Program • User Guide

cc: Conceptual Graphs • Cybernetics • Laws of Form • Ontolog Forum
cc: FB | Theme One Program • Structural Modeling • Systems Science