Contributing

Contributions and/or feedback are, of course, welcome! If you are comfortable working with GitHub, the best way to contribute is as follows:

  1. Go to the RMZoo on Github.
  2. Fork the code.
  3. Create your feature branch: git checkout -b my-new-feature
  4. Commit your changes: git commit -am 'Add some feature'
  5. Push to the branch: git push origin my-new-feature
  6. Submit a pull request.

Otherwise, don’t hesitate to send an e-mail to Eric Astor or Damir Dzhafarov.

Results File

The results file is a simple text file containing relations between reverse-mathematical principles. This is then compiled by the Zoo’s updater to create its database, which is then used by the Zoo to generate its various outputs (whether DOT files or text responses).

Names

Principles should be named by simple plaintext alphanumeric strings that resemble their normal acronyms in the literature; for example, we use RT22 for Ramsey’s theorem for pairs (with 2 colors). Do not use TeX in the names of principles (as in RT^2_2 or \mathsf{RT}^2_2); this will make the diagrams harder to read, as DOT files have no TeX support, and can sometimes cause errors.

Relations

As discussed in the Usage page, relations between principles are given using various operators. For instance:

  • RT22 -> COH

indicates an implication provable in RCA0. By itself, however, this would generate an error; all relations between principles must include a justification. To justify this fact, one would instead write:

  • RT22 -> COH "Mileti (2004) [Claim A.1.3], and independently Jockusch and Lempp"

These justifications are used by the Zoo to keep track of why the facts it derives are true, and as such are important for maintaining a usable database. For simplicity, justifications should also be plaintext; if a principle needs to be mentioned, the same acronyms as for relations should be used. To keep the results file clean, please use the justification format: “Author 1, Author 2, and Author 3 (year) [result citation]”. If possible, citations should be to the authoritative published version of the paper, falling back to an arXiv citation only when the authoritative version is not yet available.

Nearly all facts require a justification, including implications, reducibilities, conservation facts, and their negations; omitting justifications for these will produce an error. Specifications of statements’ syntactic forms are the only exception to this rule, and must remain unjustified. Attempting to justify a statement such as

  • RT22 form rPi12

will result in an error.

Officially, the Zoo supports two types of implication/non-implication (using the -> and -|> operators):

  • implication over RCA0 (RCA, the default when unspecified)
  • implication over ω-models (w)

as well as six types of reducibility/non-reducibility (using the <= and </= operators):

  • strong Weihrauch reducibility (sW)
  • Weihrauch/uniform reducibility (W)
  • generalized Weihrauch reducibility (gW)
  • strong computable reducibility (sc)
  • computable reducibility (c)
  • generalized computable reducibility (gc) [also known as reducibility over omega-models (w)]

The Zoo understands the relations between these notions of implication and reducibility, and makes use of them. Thus, it can conclude from the above examples that SRT22 w-> DNR, and that COH </=_sW SRT22.

Technically, all of these contexts can be used with both implication or reduction operators; however, absent a strong reason to believe that a non-standard choice would improve clarity, contributors should use each context with the operators noted above.

When considering syntactic forms, the Zoo supports the following options:

  • 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 paramater; defined as “twiddle-Pi03” in Patey and Yokoyama (preprint)
  • rPi12: restricted Pi12 statements, as defined in Hirschfeldt and Shore (2007) [Corollary 2.21]

When used appropriately (with statements having specified syntactic form), the Zoo understands the connections between conservation facts and implications, and will use them to extract more relations between the known principles.

Equivalences and Primary Principles

The Zoo can handle implication/reduction cycles without difficulty. For example, it will know that the facts

  • StCOH -> StCADS
  • StCADS -> StCOH

together indicate that the principles StCOH and StCADS are equivalent over RCA0, and will act accordingly. For instance, if rendering a diagram, the Zoo will pick one of the two principles to treat as ‘primary’, in the sense that implications and non-implications will only be shown going to and from the primary principle; this reduces the mess, and keeps the diagram more readable. Of course, the Zoo may occasionally pick the “wrong” primary principle; for instance, we probably want StCOH to be considered primary over StCADS. Since the Zoo has no way of knowing that on its own, we can include the fact

  • StCOH is primary

in our results file, and ensure that the Zoo considers StCOH to be the primary principle. (Note that our choice of primary principles is given no justification; in fact, by the standards of the results file, it cannot be justified.) The order in which this is done matters. For example, if we switch to thinking about omega models, StCOH will be equivalent to COH, but we probably want COH to be considered primary in this case. Entering

  • COH is primary

earlier (i.e., “higher up”) in the results file will achieve the desired result.

Principles can also be declared equivalent by use of dedicated operators, included for convenience. Writing

  • StCOH <-> StCADS

will produce the same result as including both of the two separate implications. (Warning: prepending a w to <-> does work, but does not merely indicate an equivalence that holds over omega models; it in fact asserts that both halves of the implication hold in omega models. One can use the operator <=> in a similar way, subject to the same caveat.)

Compound Principles (i.e., Conjunctions)

As the reader may have noted in the Usage page, the Zoo also understands compound principles; that is, principles that are conjunctions of other principles. For instance, if we add

  • SRT22+COH <-> RT22

as a fact in the results file (with appropriate justification, of course), the Zoo will know that COH+SRT22 is a compound principle, denoting the conjunction of COH and SRT22. It will add any component principles to its internal list, and automatically understands the relations between the compound principle and its components.

Organization and Formatting

Please note that any line in the results file starting with a # symbol is ignored, and considered to be a comment for human readers.

If contributing to the results file, please take note of the organization and formatting used therein; we have organized the results by publication, arranged by publication year when possible (with the noted exception of Simpson’s “Subsystems of Second-Order Arithmetic” [also known as SOSOA], which is listed first). Each publication’s results should be preceded by a comment containing a full authoritative citation, including (if at all possible) a URL and DOI for the authoritative published version.

Contributions to the results file are extremely welcome. For example, if anyone wants to transcribe the relevant results of Simpson’s SOSOA into our format, the maintainers would be eternally grateful! (For context, please note that this textbook is over 450 pages long.)