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.
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.
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”.