1. Is there a mathematical specification of R0?
Unfortunately, there is another research project which causes a delay in the publication of a full specification (and philosophical treatment) of R0, which is expected for 2021. The draft of the R0 thesis (2015) is available upon request (to: mail@kenkubota.de, please expect a processing time of one or two weeks as the number of incoming emails is very high). For a preliminary description, please read the tutorial of the R0 Software Implementation.
2. Have any interesting theorems been proven yet using R0? For example, one of these: cs.ru.nl/~freek/100/ [link to original tweet]
Yes, The Principle of Mathematical Induction (no. 74), which Andrews calls The Induction Theorem in Q0 (Theorem 6102) [Andrews 2002 (ISBN 1-4020-0763-9), p. 262].
In the R0 print publication Proof A6102 begins on p. 179, the established theorem itself can be found on p. 196 (wff 6723), and the definition of P5 (Principle of Mathematical Induction) can be found on p. 369 (wffs 271, 275).
In order to verify the proof and to see the definition details, run
make A6102.r0.out.html && open $_
make natural_numbers.r0.out.html && open $_
on any Mac after downloading the software (license restrictions apply) at http://doi.org/10.4444/100.10.3.
But the question doesn’t fully address the intention R0 was created for (and the fact that Theorem 6102 is the last of Andrews’ theorems that was formalized in the software implementation is a mere incident). Due to its design following Andrews’ notion of expressiveness, in principle all of mathematics can be expressed (for restrictions see p. 12). However, being a Hilbert-style system (i.e., with the inability to symbolically express metatheorems), R0 is not suited for interactive theorem proving and automation, which means that formalizing theorems is quite a time-consuming project. For a practical approach, a natural deduction variant of R0 should be implemented as suggested here and here.
3. Does R0 have further restrictions on type quantification (or type abstraction) like other logics (e.g., HOL-Omega or Isabelle/HOL)?
No.
Paradoxes (antinomies) are caused by both
- self-reference and
- negation
as discussed here.
For formal logic and mathematics, this means that paradoxes (antinomies) are the result of the violation of type restrictions. All restrictions should be “encoded” within the types, and any further regulations should avoided. Russell’s concept of type theory is to shape the formal language itself such that paradoxes cannot be expressed.
In particular, circularity (self-reference) alone is not a problem (without negation). Hence, additional restrictions (additional checks) to avoid a “circularity” are not necessary. Any use of means to avoid paradoxes beyond those of the formal language itself misses the point of Russell’s concept of type theory.
This leads to a critique of such approaches described here:
To avoid inconsistency, this overloading mechanism is regulated by syntactic checks for orthogonality and termination. Examples like the above should be allowed, whereas examples like the following encoding of Russell’s paradox [28, Sect. 1] should be forbidden:
consts c : α
typedef T ≡ {True, c}
definition c : bool ≡ ¬ (∀(x:T) y. x = y)The above would lead to a proof of false taking advantage of the circularity T ~~> c_bool ~~> T in the dependency relation introduced by the definitions: one first defines the type T to contain precisely one element just in case c_bool is True, and then defines c_bool to be True just in case T contains more than one element. [Kuncar/Popescu, Comprehending Isabelle/HOL’s Consistency, p. 2]
To ensure the soundness of the HOL-Omega logic, in addition to being well-typed, a term must also be well-ranked. In HOL-Omega, every type has a rank. The rank of a type is a natural number 0, 1, 2, …; it can never be negative. This is essentially a measure of how deeply universal (or existential) types are nested within the type. […]
The purpose of ranks is to restrict what types can properly be the argument in a type application term. If one could apply a type abstraction term to its own type as an argument, this would introduce a circularity that could imperil the soundness of the logic. To prevent this, for every type application term t[:τ:], where t has type !α.σ, it is required that the rank of τ be less than or equal to the rank of α. If it is greater than the rank of α, this will be caught and reported as an error. [Peter Homeier, The HOL-Omega System TUTORIAL, p. 71]
