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.

Choiceless Grapher app

The Choiceless Grapher (CGraph in short) is a common-lisp program with a common-lisp website, which can produce any size of graph of the implication relationships between any collection of consequences of the axiom of choice (AC) in Zermelo-Fraenkel set theory (ZF). I talked about it a bit in this and in this previous post.

The website is hosted thanks to Max Rottenkolber at cgraph.inters.co, under the website of our team, Interstellar Ventures. The code for the program creating these graphs can be found at this GitHub repository, along with some details about what each package does.

I will briefly explain how the predicates work in the next post, along with my idea of how one can use this program to visualise similar data on implications between axioms in an axiomatic system.

Website features

Basic usage

Until now, one could only use CGraph via a Common Lisp REPL (Read Evaluate Print Loop), which is often not what the target audience, logicians, and in particular set theorists, are willing to do. With this app, you just enter the numbers of the weak choice principles (forms), as found in the Consequences of the Axiom of Choice Project, and you get a diagram depicting the known implications between these principles, according to that project.

Why use it?

A gray arrow from A to B in a diagram means that A implies B but we don’t know if B implies A or not. Until you construct a model of ZF+B+¬A, this arrow will remain gray.

There are many results, ranging from obvious results to difficult projects, which have not been studied. These diagrams can help you find these open questions, and hopefully fill in the missing arrows.

For example, check out Asaf Karagila’s comment on one of the diagrams.

Current options

You can request diagrams with either fancy labels, which are the full statements of the forms in LaTeX format, or with just number labels, which are the Howard-Rubin (HR.) numbers of the forms.

You can also automatically include the top and bottom nodes of the graph. The top node is HR.1, the axiom of choice, and the bottom node is HR.0, “0=0”, meaning just ZF.

Features to appear

During this week I will add the features of graphing the descendants of a form (the diagram of everything a certain form implies), the ancestors of a form (the diagram of everything that implies a certain form), and graphing a (pseudo) random collection of a given amount of forms (if you’re looking for a fun short-term or long-term project).

At the same time I’ll start taking care of concurrency issues, which might appear for example when two people request the same diagram at the same time. For now, if you get a result page but the diagram is missing, please just refresh the page.

After that I’ll tackle the current limitation of the web version, that is graphing only 70-80 forms. For this i just have to encode very long strings into strings of filename acceptable length.

I am considering adding the feature “show all negative implications”, so that it is clear when two forms, which do not have arrows between them, have been proven to be different.

Including shorthand names for the forms will take a bit more time, because not all forms have shorthand names, and it seems I would have to manually enter and, in some cases, come up with such names.

I am also considering including a matrix where you can choose the forms to graph by clicking on them but this will probably turn out a long list, if no shorthand names are available.

Any suggestions for extra features will be very much appreciated! You can also follow the to-do list on GitHub.

Example diagrams included

I included examples of the diagrams you can create using this app. Of particular interest and, I think, beauty, is the full diagram, which depicts all the ZF-related information gathered in the Consequences of the Axiom of Choice Project.

Please test it!

I will be grateful for any comments or corrections you sent me, in particular, do send me any issues you see with the fancy labels, i.e., the full LaTeX formatted statements of each form. But I would be happy to hear from you if anything at all appears the wrong size or an image is not appearing.

If you see any arrows “clearly missing”, then you possibly found something easy you can publish or a topic for a masters thesis!

 

Coming up as a next post: “How do CGraph’s predicates work and how can we use this program to visualise other implication data, of axioms in other axiomatic systems”.