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

3 thoughts on “Choiceless Grapher app”

    1. I think Paul Howard is planning such a feature for a new website of the Consequences of the Axiom of Choice Project, but I’m really not sure.

      We can test such a feature for CGraph with another (smaller?) dataset of implications, for example large cardinals in ZFC? Or even reverse mathematics, but I bet that’s definitely not a smaller dataset.

      I suppose the issue would be mostly who gets to and has time to decide which forms should be added and which results are incorporated.

      1. I propose the Vogons.

        But of course that this decision has to be ratified by a majority of 3/4th before we can even approach the Vogons with this offer, which will then require several dozen forms and committees to process this through until they are able to debate whether or not they want to populate this additional committee for deciding what gets into the Choiceless Dictionary.

Leave a Reply

Your email address will not be published. Required fields are marked *