 for quantifier-free formulas F(x0). As Gödel remarks (Gödel 1990, p. 247), the axioms for T are essentially those of primitive recursive arithmetic, except that the variables can be of any finite type.