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 2020. 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.

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

  1. self-reference and
  2. 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.

In particular, circularity (self-reference) alone is not a problem (without negation). Hence, additional restrictions (additional syntactic checks) to avoid a “circularity” are not necessary.

This leads to a critique of such approaches described here:

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]

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]