Mathematical Formulae

This work contains the formula part of the presentation of the mathematical logic R₀, a further development of Peter B. Andrews’ logic Q₀. The syntactic features provided by R₀ are type variables (polymorphic type theory), the binding of type variables with the abstraction operator and single variable binder λ (type abstraction), and (some of) the means necessary for dependent types (dependent type theory).

For more information, please see: http://doi.org/10.4444/100.10