After a major restructuring to make the predicates faster, and to process the LaTeX statements, the Choiceless Grapher is now installable and usable for Linux, and can produce any size of graph of the implication relationships between the consequences of the axiom of choice (428 in total), as found in Consequences of the Axiom of Choice Project, by Prof. Paul Howard and Prof. Jean E. Rubin, with an option on the style of nodes: you can either have the Howard-Rubin (HR) numbering of the forms (“numbers”), or the full LaTeX-formatted statements (“fancy”).
A diagram with about 10 nodes takes a minute or so to get created because the predicates are being calculated from the original implication information. In the package :jeffrey.test you can find functions which verify that the derived implications exactly match the ones derived originally by Howard and Rubin (book1).
The full diagram takes about 15-45 minutes to be created, depending on your machine. But thankfully you don’t have to do that, since you can download it, with the number labels only at the moment. Note that it’s quite large, measuring at 3,76m x 1,89m. I suppose it’s not very readable, due its size, but it could make a wonderful wallpaper or art installation. The full diagram with fancy labels, is too large to handle for my laptop at the moment, and I’m estimating its size will be around 20×10 m. I’m working on it.
You can also draw random graphs! If you are looking for a fun project, or just a nice picture, do try out the random-graph function, which draws the implications of a pseudo-random collection of forms, of any size from 1 to 428. Random graphs always include the top and bottom node (HR 1. and HR 0. respectively), otherwise they may well turn out completely disconnected. The featured image is a random graph with 6 nodes (not counting 0 and 1), and with fancy labels. Just imagine the endless possibilities for random research projects, theses, and papers, filling or boldfacing those arrows! :)
The ratio of these graphs is set to 0.5 for better readability. You can change that, and other attributes of the graphs by editing the resulting .dot file (see dot manual) and running tred and dot manually with
tred filename.dot | dot -Tpng -o filename.png
in a Linux terminal.
Installation and usage instructions can be found at the project’s website: https://github.com/ioannad/jeffrey
Next up on the to-do list for now are to create a website so that you don’t have to install this program, and to have it output LaTeX code, so you can nicely import the graphs in your papers. As always, feel free to suggest additions, improvements, or corrections. Windows and Macintosh compatibility is also on the list, but if you can’t wait you can still use the Choiceless Grapher to produce the dot file and then run tred and dot yourself.
Finally, expect regularly small additions and improvements here and there, by “watching” the repositoty on GitHub. I’ll be very happy if you give it a try, so please let me know if you do, and if something is not working as you expected/would like.