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 2028. 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 and Metatheory of Q0:
    • Prooftoys by Cris Perdue (a natural deduction variant; logic description)
    • Metatheory of Q0 by Javier Díaz (formalization of the metatheory of Q0 in Isabelle/HOL; proof document, announcement)
    • Metamath/Q0 by Thierry Arnoux (in the logical framework Metamath; source, announcement)
    • Soundness of the Q0 proof system for higher-order logic by Anders Schlichtkrull (proof document, announcement)
  • Archived Homepage of Peter B. Andrews (obituary)

 

Kubota – R0 Logic
doi.org/10.4444/100.10