Last year I said that I am learning Common-Lisp with a grapher for relationships between consequences of the Axiom of Choice in mind. A year later, the core of a first version of this program is finished and uploaded on GitHub:
I am very thankful to Prof. Paul Howard for the permission to use the data of his and Prof. Jean Rubin’s encyclopedia of choiceless set theory: “Consequences of the Axiom of Choice”, and for sending me the latest implications data and the tex statements of the forms.
An example diagram is the featured image, depicting the relationships between the forms in the category “Alephs and their properties”. Some more examples of diagrams can be found here:
An arrow from A to B means that A implies B and a boldfaced arrow is non-reversible, i.e., there is a model of ZF where B holds and A doesn’t. Note that this diagram is made with the old implication data.
Since I uploaded this program on GitHub, I have decided that it might better (faster) to store the graph information as a matrix instead of the current graph structure. This is the structure of the data that Paul Howard sent me (book1). As soon as I finish checking my predicates against this book1, I shall upload the next version, with some drawing functionality. I will also include the complete full graph, which, judging from past experiments, I estimate to be about 3 meters wide and 2 meters tall (wallpaper anyone?).
If you can’t wait until that (my concentration is more on natural-isabelle at the moment), do send me an email with the form numbers that are of interest to you, and I will have the choiceless grapher draw a diagram with your forms, as soon as I find some time.
PS. I did notice the obvious missing arrow between Form 208 and 170. That arrow is also missing in the latest data, and it is one of my strongest arguments why we need such diagrams. :)
PS-2. All the bottom forms point to “Form 0. 0 = 0”. Right-click on the featured image and select “View Image” to see the whole diagram.