The Mathematical Logic R0

by Ken Kubota

The Mathematical Logic R0 is a further development of Peter B. Andrews’ logic Q0.

It will be published in three parts:

1. Philosophical Treatment
2. Mathematical Formulae
3. 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.

Further Resources

• 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
https://doi.org/10.4444/100.10