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:

https://github.com/ioannad/jeffrey#choiceless-grapher

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:

https://github.com/ioannad/jeffrey/tree/master/sneak-preview

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.

Also the arrow from Form 25 to Form 34 should be boldfaced (many ZF models satisfy 34 but not 25), something that is missing from the database. Diagrams are so much easier to stare at and find missing information than lists of implications with codes.

Please do comment with any observations on this featured diagram if you see something!

There’s an arrow missing from 208 to 170.

It’s not clear to me why 104 and 182 are not equivalent (cofinality of an ordinal is always regular).

There is a parenthesis mismatch in 58.

It’s not hard to show that 365 implies 170, but not vice versa.

108 seems a bit odd, since $\omega_2$ is itself never the countable union of countable sets (it could be the countable union of countable unions of countable sets), so it’s power set certainly isn’t either.

And that’s all from the image appearing on this post… :)

Thank you so much for the observations, I agree with all of it! I think Form 108 has a typo, and instead of “denumerable union of denumerable sets” it should be “denumerable union of sets of cardinality $\aleph_\alpha$” (given that this form is taken from Gitik’s “Regular cardinals in models of ZF”, see page 67, question 6).

All this from one featured image, exactly! :) Just imagine what will come out while staring at the wallpaper version of the full diagram! :D