by Ken Kubota
The Mathematical Logic R0 is a further development of Peter B. Andrews’ logic Q0.
It will be published in three parts:
- Philosophical Treatment
- Mathematical Formulae
- Software Implementation
For details, please read the detailed announcement.
A full specification of the logic will be published with the philosophical treatment expected for 2021. As a preliminary introduction shall serve the tutorial, which is part of the software implementation and also available online. Please see also the R0 FAQ.
- Foundations of Mathematics. Genealogy and Overview (first online 2016, update)
- The higher-order logic Q0 by Peter B. Andrews
- Peter B. Andrews: Q0 (“A Formulation Based on Equality”)
- Ken Kubota: Q0 (short description on the Isabelle mailing list)
- Implementations of Q0: Prooftoys (a natural deduction variant; logic description), Metamath/Q0 (in the logical framework Metamath; source, announcement)
- Homepage of Peter B. Andrews
Kubota – R0 Logic