About
The Reverse Mathematics Zoo is a program to help organize relations among various mathematical principles, particularly those that fail to be equivalent to any of the big five subsystems of second-order arithmetic. Its primary goal is to make it easier to see known results and open questions, and thus hopefully to serve as a useful tool to researchers in the field. As a secondary goal, the Zoo should provide an interactive annotated bibliography of the field, collecting results in a standard machine-readable format.
The present version of the RM Zoo is a complete rewrite of the original, and features many improvements. The program has been heavily optimized and extended; the run time should generally be faster, and more true facts should be inferred from most starting results files. In addition, the RM Zoo can now handle implications, reducibilities (including Weihrauch reducibility, computable reducibility, and their strong and generalized variants), and conservation facts.
The program is divided into two parts: a database updater/compiler, which derives all inferences from the provided results file, and a database query system, which can answer specific questions about reverse-mathematical relations or produce diagrams on request.
Under the reverse-mathematical interface, the Zoo is actually a specialized inference engine, designed to reason with facts of the form “a implies b in context Q” (implication facts), “if a implies p, and p has form F, then b implies p” (conservation facts), or the negations thereof.
Installation
To use the RM Zoo, download rmzoo.zip and unzip the package.
You will need to install a distribution of Python, version 2.7 or later. (The Zoo will perform best if run in either PyPy2.7 or Python 3.4+.)
You will also need the Pyparsing module.
If not using Python 3.4+, you will need to install the enum34 module, and if not using Python 3.2+, you will also need the repoze.lru module.
To install each of these modules, run the appropriate commands below:
pip install pyparsing
pip install enum34
pip install repoze.lru
To view/render the diagrams produced by the Zoo, you will need to install Graphviz, or another program capable of reading DOT files.
Credits
The RM Zoo was originally developed by Damir Dzhafarov, inspired by Joe Miller‘s command-line version of the Computability Menagerie. Recently, the Zoo has been largely rewritten by Eric Astor to improve performance, expand the library of available inference rules, and move to a more maintainable/upgradeable architecture.
Many people have helped with the RM Zoo, by commenting on the code, contributing facts, suggesting new features, or just expressing their interest. Thanks in particular to David Belanger, Peter Cholak, Stephen Flood, Denis Hirschfeldt, Steffen Lempp, Joe Miller, Antonio Montalbán, Carl Mummert, Ludovic Patey, Sam Sanders, and Ted Slaman.