-
Notifications
You must be signed in to change notification settings - Fork 4
Description
I would like to include results for stronger systems in a pull request (e.g. equivalences to Pi^1_1-CA_0).
RT appears to be the strongest system currently here (according to this output of rmzoo), and RT is itself below ATR in strength (Patey, "The reverse mathematics of Ramsey-type theorems", p.28), so it appears that all theories here currently are below ATR. Is there a guideline against adding theories stronger than RT or ATR to rmzoo (e.g. if the focus is on the detail of the hierarchy around RCA through ACA), or is it allowed?
The Contributing guidelines page contains the following quote:
For example, if anyone wants to transcribe the relevant results of Simpson’s SOSOA into our format, the maintainers would be eternally grateful!
If there is a guideline against adding theories stronger than RT, should the results from SOSOA be cut off to only include theories weaker than ATR?