jeffrey-predicates

CGraph predicates

This is a continuation of my previous post about CGraph, the Choiceless Grapher, which creates custom diagrams of consequences of the axiom of choice. The original project “Consequences of the Axiom of Choice” by Prof. Paul Howard and Prof. Jean E. Rubin, which project this app visualises, is currently hosted here.

In this post I will describe how the Choiceless Grapher decides whether there is an arrow from A to B, and whether this arrow should be gray (A implies B and we don’t know whether B implies A) or boldfaced (A implies B and B does not imply A).

Starting data

I took a matrix of implications: book1, which also comes with the diskette of the book. This contains a 431×431 matrix, in which each cell (row , column) encodes the answer to the question “does form number row imply form number column ?”. The codes are:

  • 0 = unknown,
  • 1 = directly implies (a result in a paper),
  • 2 = indirectly implies (follows from a path of implications with codes 1 or 2),
  • 3 = directly not implies (a result in a paper),
  • 4 = indirectly not implies (follows from paths of implications with codes 1, 2, 3, 4),
  • 5 – 6 = like 3 – 4 for untransferable results in ZFU (ZF with Urelements, here ignored), and
  • 7 = unknown and there is a question in the literature about this implication.

I read the information on codes 1 and 3 only, so I can verify codes 2 and 4 with the predicates described below.

Internal structure

The information about each form, say A, is held in  a Common Lisp structure I called node, which has fields:

  • name, the Howard-Rubin (HR) number of A,
  • edges a list of edges, where an edge represents an implication from A (“does A imply …?”), and is a structure itself called edge with two properties:
    • relation, true (T) for code 1 and false (NIL) for code 3,
    • destination, a pointer to the implication’s (or non-implication’s) destination node.
  • parents, a list of the forms which imply A, made using only code 1 implications,
  • LaTeX, the full LaTeX formatted statement of the form, parsed from a tex file,
  • references, the references to where this form was first mentioned,
  • and a still unused attributes.

The predicates

The predicate (graph-implies-p A B) checks if A is a member of the ancestors of B, which ancestors are collected by recursion on the parents of each node.

The predicate (graph-implies-not-p B A) collects the destinations of the edges of the ancestors of B with edge-relation property = NIL, and checks if one of these destination is a descendant of A. If this happens, then we have a situation as depicted below:

jeffrey-predicates

If such a “NIL-edge” between B-ancestor and A-descendant exists, then B cannot imply A, because if it did, then we’d have:

B-ancestor \Rightarrow B \Rightarrow A \Rightarrow A-descendant,

therefore B-ancestor \Rightarrow A-descendant, which is a contradiction to the NIL-edge from B-ancestor to A-descendant. So in this case (graph-implies-not-p B A) returns T, i.e., B does not imply A. If moreover (graph-implies-p A B) returns T, then CGraph draws a boldfaced arrow from A to B.

If (graph-implies-not-p B A) returns NIL, i.e., we don’t know whether B implies A, and (graph-implies-p A B) returns T, then CGraph draws a gray arrow from A to B.

Directed acyclic graphs (DAGs)

Some forms are removed from the data, due to later discovered equivalences. Equivalent forms (usually forms with the same HR numbers, and possibly extra identifiers ([A], [B], [C], …)) are not depicted yet. These diagrams are modulo equivalences, and thus directed acyclic graphs (DAGs).

Complexity

These predicates are quite slow on their own, \text{O(N)} for graph-implies-p and \text{O(N}^2\text{)} for graph-implies-not-p (not considering compiler optimisation). This means that drawing large graphs (of size almost the full graph) has complexity \text{O(N}^3\text{)}. To improve this I use a memoization matrix, which works like book1. A cell (row, col) in the memoization matrix gets filled in when one of the predicates is asked for an empty cell, and returns T. In test.lisp you can compare the answers of my predicates to the codes in book1, they match exactly (disregarding the four removed forms).

Using the core of CGraph to visualise other data

It is possible, with little effort*, to use CGraph as is, in a Common Lisp REPL, to visualise any implication data for statements in axiomatic systems of classical logic. With some tweaking of the predicates, non-classical logics could be supported as well.

And in a similar way to what I did for CGraph’s website, it’s quite straightforward to put up a website to create custom diagrams in your database. You are very welcome to contact me if you are interested in doing this, and feel free to copy, modify, and redistribute CGraph’s code.

(*) When I say “with little effort” I am excluding the effort of gathering the data, of course.

2 thoughts on “CGraph predicates”

  1. I would suggest to also track some data and create some caching mechanism for “common forms”.

    And this whole thing sends me back to my freshman year, learning about BFS and DFS algorithms. In this case, I’d go with a mix of the two, breaking the depth into chunks of several implications at a time (ranked from “most directly implied” to least) and going through each of them BFS-style.

    1. Implementing depths was on the to do list for a while, but I removed it because I’m not convinced it’s worth the trouble, since the diagrams are relatively short and wide (see the full diagram). I might experiment with that when I find the time. Most directly implied are the parents, which are searched first:


      (defun ancestors (node) ;; => list
      "Returns the list of strict ancestors of NODE."
      (when (node-parents node)
      (remove-duplicates
      (apply #'append
      (node-parents node)
      (map 'list #'ancestors (node-parents node))))))

      (defun graph-implies-p (X Y)
      (member X (cons Y (ancestors Y))))

      I say I’m not convinced because `graph-implies-p` is only \text{O(N)}, and N is only 427. Most time is spent on `graph-implies-not-p`, which also searches direct descendants/ancestors first, but seems to be necessarily \text{O(N}^2\text{)}. What I think might make a difference (when drawing very large graphs) is only graphing direct implications of the subgraph, instead of graphing everything and having `dot tred` remove the extra edges. Perhaps depths will help there. Correctness of the predicates is most important, so I’m reluctant to complicate the code. Since very large graphs seem to only have an aesthetic use (they aren’t really readable), taking care of this is not high in my priority list. :)

      Could you elaborate on your suggestion to ‘track some data and create some caching mechanism for “common forms”‘?

Leave a Reply

Your email address will not be published. Required fields are marked *