Usage

The RM Zoo consists of two Python scripts, rmupdater.py and rmzoo.py, along with a results file, a compiled database, and some assorted libraries.

rmupdater

rmupdater.py compiles results files into databases of known facts, and is typically run as follows:

  • python rmupdater.py [results file],

where [results file] is a text file containing facts; the results file included in this distribution is results.txt. If using multiple results files (for testing purposes), you may keep them in separate databases by adding a database title:

  • python rmupdater.py [results file] [database title]

For example, one would typically run

  • python rmupdater.py results.txt;

If maintaining an alternate results file in test.txt, one might separately run the command

  • python rmupdater.py test.txt testDatabase.

rmzoo

rmzoo.py then takes the database built by rmupdater.py, and carries out various tasks as controlled by its options. The basic command is

  • python rmzoo.py [options];

however, if you need to specify a database title, add it to the command as follows:

  • python rmzoo.py [database title] [options]

Generating diagrams

To generate a diagram from the database, run

  • python rmzoo.py [diagram options] > [destination],

where [destination] is a DOT file. The [diagram options] must include one or more of the following:

  • -i: show implications as black arrows;
  • -n: show non-implications as red arrows;
  • -f: color-codes principles by their syntactic form; currently, this uses a pink box for Π11 principles, and a cyan box for restricted Π12 principles. Other forms do not yet have a color code.
  • -c: show conservation facts, using color-coded arrows (as for the forms) to represent each form of conservation;
  • -w: show the weakest open implications as green arrows;
  • -s: show the strongest open implications as green arrows.
    In addition, the options may include any of the following:
  • -o: show facts that hold in ω-models;
  • -t [REDUCIBILITY]: show facts relative to implications over the given REDUCIBILITY (options include sW, W, gW, sc, c, w [also known as gc], and RCA);
  • -p: show only one primary principle from each group of equivalent principles;
  • -r "[CLASS]": restrict the diagram to just the principles contained between the quotation marks (and any sub-principles of conjunctions in the list). For example, the option -r "RT22 COH+WKL SRT22 RCA" will show only relations between the principles RT22, COH+WKL, SRT22, RCA0, COH, and WKL.

For instance,

  • python rmzoo.py -i -o -w > diagram.dot

will produce a diagram of all implications between principles that hold in ω-models, along with the weakest open implications (in ω-models). Generally speaking, the more options that are selected, the more information is shown on the diagram; this tends to make it harder to read.

It would probably be of very limited use to select all the options, for instance.

Querying

To query the database for a fact (which will determine whether it is known or contradicted, and give the justification in either case), run the command

  • python rmzoo.py -q "[fact]".

For example,

  • python rmzoo.py -q "RT22 -> CRT22"

will print a justification of the fact that RT22 implies CRT22 over RCA0.

Facts

Facts understood by the Zoo consist of relations between principles, and statements on the form of a principle.

Principles

Principles are named by simple alphanumeric strings (using only the characters A-Z, a-z, and 0-9) resembling the normal acronyms in the literature. It should be noted that the Zoo understands (and has special handling for) compound principles, formed by taking conjunctions of simpler principles. These are created by adding a + between principle names. For example, one can ask about the principle SRT22+COH, which the Zoo knows is equivalent to COH+SRT22. In some instances, the Zoo may not recognize a new compound principle (such as ADS+COH); in these instances, by adding the --force option when invoking rmzoo.py, we may force the Zoo to recompute its database in order to find all it can about this novel conjunction. (Please be warned that this process can take some time.)

Relations

The most basic relation in the Zoo is implication between principles in a given context, specified using the operator ->. The context, if not otherwise specified, is assumed to be reverse-mathematical consequence over the weak base system RCA0. Thus, RT22 -> CRT22 references the claim (a true theorem) that RT22 (Ramsey’s theorem for pairs) implies CRT22 (cohesive Ramsey’s theorem for pairs) over RCA0; that is, any model of both RCA0 and RT22 is also a model of CRT22.

To specify a different context, one prepends its descriptor to the implication operator. To specify implication over ω-models, for instance, we use the operator w->. As such, COH w-> StCOH represents the claim that COH implies StCOH over ω-models; i.e., any ω-model of COH is also a model of StCOH. The Zoo supports all contexts/reducibilities listed above as possible parameters for the -t [REDUCIBILITY] diagrammatic option.

The Zoo also understands non-implication in a similar fashion, using the operator -|>. For example, RT22+WKL -|> ACA represents the claim that RT22+WKL fails to imply ACA over RCA0; that is, there is a model of RT22+WKL and RCA0 that is not a model of ACA. Furthermore, one could instead reference the stronger fact RT22+WKL w-|> ACA, which makes the claim that there is an ω-model with this property.

For some facts, another format is more natural. To support this, the Zoo also understands reducibility (operator <=) and non-reducibility (operator </=) between principles, in various contexts and under assorted constraints, with the type of reducibility appended to the operator. For example:

  • DNR <=_c SRT22 is the claim that there is a computable reduction of DNR to SRT22.
  • COH </=_W SRT22 is the claim that there is no Weihrauch reduction of COH to SRT22.

The Zoo supports many standard reducibilities, including all those listed above as possible parameters for the -t [REDUCIBILITY] diagrammatic option. In particular, it supports all of:

  • (strong) Weihrauch reduction [sW or W]
  • generalized Weihrauch reduction [gW]
  • (strong) computable reduction [sc or c]
  • generalized computable reduction [gc, equivalent to implication over ω-models]

A fact can assert that a principle can be put into a given syntactic form by using the form operator; for example, we could assert that RT22 form rPi12 (i.e., that RT22 can be written as a restricted Π12 statement), or that BSig2 form Pi11 (that BSig2 can be written as a Π11 statement). The Zoo currently understands the following syntactic forms:

  • Sig02, Pi02, Sig03, Pi03, Sig04, and Pi04: three levels of the arithmetic hierarchy
  • Pi11, Pi12, and Pi13: the first three universal levels of the analytic hierarchy
  • uPi03: Pi03 with a single universally-quantified set parameter; defined as “twiddle-Π03” in Patey and Yokoyama (preprint)
  • rPi12: restricted Π12 statements, as defined in Hirschfeldt and Shore (2007) [Corollary 2.21]

Finally, the Zoo also supports conservation facts (claims that one principle is conservative over another for consequences of a given form). To do so, we use the c operator, prepending the form in question; for instance, we can consider claims such as:

  • AMT+BSig2 Pi11c BSig2: AMT+BSig2 proves no more Π11-consequences than BSig2 alone.
  • AMT rPi12c RCA: AMT proves no restricted Π12-statements that cannot be proven in RCA0.

We can also ask about non-conservation facts, asserting that one principle has consequences of a given form that do not follow from another principle. This is done by adding an n before the conservation operator, as follows:

  • RT22 nPi04c RCA: RT22 proves a Π04 statement that cannot be proven in RCA0.