CGraph predicates

This is a continuation of my previous post about CGraph, the Choiceless Grapher, which creates custom diagrams of consequences of the axiom of choice. The original project “Consequences of the Axiom of Choice” by Prof. Paul Howard and Prof. Jean E. Rubin, which project this app visualises, is currently hosted here.

In this post I will describe how the Choiceless Grapher decides whether there is an arrow from A to B, and whether this arrow should be gray (A implies B and we don’t know whether B implies A) or boldfaced (A implies B and B does not imply A).

Starting data

I took a matrix of implications: book1, which also comes with the diskette of the book. This contains a 431×431 matrix, in which each cell (row , column) encodes the answer to the question “does form number row imply form number column ?”. The codes are:

  • 0 = unknown,
  • 1 = directly implies (a result in a paper),
  • 2 = indirectly implies (follows from a path of implications with codes 1 or 2),
  • 3 = directly not implies (a result in a paper),
  • 4 = indirectly not implies (follows from paths of implications with codes 1, 2, 3, 4),
  • 5 – 6 = like 3 – 4 for untransferable results in ZFU (ZF with Urelements, here ignored), and
  • 7 = unknown and there is a question in the literature about this implication.

I read the information on codes 1 and 3 only, so I can verify codes 2 and 4 with the predicates described below.

Internal structure

The information about each form, say A, is held in  a Common Lisp structure I called node, which has fields:

  • name, the Howard-Rubin (HR) number of A,
  • edges a list of edges, where an edge represents an implication from A (“does A imply …?”), and is a structure itself called edge with two properties:
    • relation, true (T) for code 1 and false (NIL) for code 3,
    • destination, a pointer to the implication’s (or non-implication’s) destination node.
  • parents, a list of the forms which imply A, made using only code 1 implications,
  • LaTeX, the full LaTeX formatted statement of the form, parsed from a tex file,
  • references, the references to where this form was first mentioned,
  • and a still unused attributes.

The predicates

The predicate (graph-implies-p A B) checks if A is a member of the ancestors of B, which ancestors are collected by recursion on the parents of each node.

The predicate (graph-implies-not-p B A) collects the destinations of the edges of the ancestors of B with edge-relation property = NIL, and checks if one of these destination is a descendant of A. If this happens, then we have a situation as depicted below:

jeffrey-predicates

If such a “NIL-edge” between B-ancestor and A-descendant exists, then B cannot imply A, because if it did, then we’d have:

B-ancestor \Rightarrow B \Rightarrow A \Rightarrow A-descendant,

therefore B-ancestor \Rightarrow A-descendant, which is a contradiction to the NIL-edge from B-ancestor to A-descendant. So in this case (graph-implies-not-p B A) returns T, i.e., B does not imply A. If moreover (graph-implies-p A B) returns T, then CGraph draws a boldfaced arrow from A to B.

If (graph-implies-not-p B A) returns NIL, i.e., we don’t know whether B implies A, and (graph-implies-p A B) returns T, then CGraph draws a gray arrow from A to B.

Directed acyclic graphs (DAGs)

Some forms are removed from the data, due to later discovered equivalences. Equivalent forms (usually forms with the same HR numbers, and possibly extra identifiers ([A], [B], [C], …)) are not depicted yet. These diagrams are modulo equivalences, and thus directed acyclic graphs (DAGs).

Complexity

These predicates are quite slow on their own, \text{O(N)} for graph-implies-p and \text{O(N}^2\text{)} for graph-implies-not-p (not considering compiler optimisation). This means that drawing large graphs (of size almost the full graph) has complexity \text{O(N}^3\text{)}. To improve this I use a memoization matrix, which works like book1. A cell (row, col) in the memoization matrix gets filled in when one of the predicates is asked for an empty cell, and returns T. In test.lisp you can compare the answers of my predicates to the codes in book1, they match exactly (disregarding the four removed forms).

Using the core of CGraph to visualise other data

It is possible, with little effort*, to use CGraph as is, in a Common Lisp REPL, to visualise any implication data for statements in axiomatic systems of classical logic. With some tweaking of the predicates, non-classical logics could be supported as well.

And in a similar way to what I did for CGraph’s website, it’s quite straightforward to put up a website to create custom diagrams in your database. You are very welcome to contact me if you are interested in doing this, and feel free to copy, modify, and redistribute CGraph’s code.

(*) When I say “with little effort” I am excluding the effort of gathering the data, of course.

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

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

choiceless grapher is now Linux installable

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.

choiceless grapher

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.

natural isabelle

For the past year at the mathematical logic group of Bonn, I’ve been learning a lot about formal mathematics, and in particular, developing ideas with Peter Koepke to strengthen formal mathematics here in Bonn, and to expand on the developments concerning (controlled) natural language proof checking made during the Naproche project.

Last May we started, together with Peter Koepke and Regula Krapf, a voluntary formal mathematics work group, where we looked at the proof assistant Isabelle, and the student turn out was with 12 students  very motivating indeed! Six of them gave detailed presentations and six of them joined another five bachelor’s students for this semester’s internship in mathematical Logic,  under the title
“Natural Isabelle”.

In this project we are looking at Isabelle-formalised proofs and theory files, starting with the beginnings of set theory, rewriting them in the language Isar (Intelligible Semi-Automatic Reasoning) with an eye toward naturalising them, and we plan to write parsers in OCaml from a controlled natural language for mathematical proofs to the Isar language. I am personally delighted at the amount of interest this project has generated, and I can only say,

stay tuned for upcoming naturalised formal proofs!

The featured image is taken from the Isabelle website.

A toolkit for the Dodd-Jensen core model

I just finished a note with some black boxes for the Dodd-Jensen core model $K^\text{DJ}$, the core model that cannot have a measurable cardinal. I am not an expert on core model theory, so this is just a  presentation of $K^\text{DJ}$, like painter A. Dürer’s presentation of a Rhinoceros (in the featured image), just by the descriptions of others, never having seen one himself. And perhaps my note is not as detailed as Dürer’s painting is, but I hope it’s a sufficient presentation for someone who just wants to get consistency strength from $K^{\text{DJ}}$ without having to go through all its glorious detail. One could say this is a note on applied set theory.

This note includes the trick to construct $K^{\text{DJ}}$ inside a model of ZF, by using the fact that  for any set of ordinals $x$, $(K^\text{DJ})^{\text{HOD}}=(K^\text{DJ})^{\text{HOD}[ x] }$ and this equality holds for every level of the $K^\text{DJ}$-construction.

There’s also a running example,  the proof that if $V$ is a model of ZF in which the Chang conjecture $(\omega_5,\omega_4)\twoheadrightarrow (\omega_3,\omega_1)$ holds,  $\omega_4$ is a regular cardinal, and cf$\omega_3>\omega$ then in $(K^\text{DJ})^{\text{HOD}}$, an Erdős cardinal exists, and in particular, $(K^\text{DJ})^{\text{HOD}}\models\omega_5^{V}\to(\omega_3^V)^{<\omega}_2$. This is an example of how to use these black boxes, and I think it helps clarify how this Rhinoceros model looks like. As always, there are pictures included – now in pgfpicture.

I’d be happy to get suggestions, corrections, and more $K^\text{DJ}$-black boxes and examples.