The following diagrams, generated by the Zoo, summarize the current database, last updated April 2018. Throughout, arrows indicate implications provable in RCA0, and double arrows indicate implications known to be strict.
- Implications and strict implications
- Implications and non-redundant non-implications (red)
- Implications and strict implications (primary only)
- Implications and strict implications that hold in omega models
- Implications and strict implications that hold in omega models (primary only)
- Implications, strict implications, and weak open implications (green)
- Implications, strict implications, and strong open implications (orange)
For comparison, the following diagrams were created by hand using various TeX graphing packages.