In this paper we consider a fonnal system of second-order Peano arithmetic with a rule of inference stronger than the ω-rule [3]. We also consider the relation to a class of models for analysis (i.e. second-order arithmetic) which lies between the class of ω-models and the class of β-models [5].

The notation used is largely that of [3] and [5]. We assume that the reader has some familiarity with at least the ideas of the former. The formal system (A) of Peano arithmetic employed in [3] includes the comprehension axioms and the second-order induction axiom.

In this paper, we shall state some results concerning ℵ0-complete cardinals and the transcendency of cardinals which is proposed by G. Takeuti [6]. The main purpose of this paper is to prove the following theorems.

Theorem 1. Let ℵ1, be the first ℵ0-complete cardinal number. Then the transcendency of cardinals holds for Δ11-functions of ℵ1-language.

A theory T is axiomatizable by a schema if there is a formula Γ, involving symbols of T plus a new relation symbol R, such that the set of all (universal closures of) instances of Γ in T is a set of axioms for T. (It is understood that, if R has n places, an instance of Γ in T is obtained by properly substituting for R in Γ a formula of T which has n selected free variables and is allowed to have any number of other free variables as parameters.) Obviously, the notion is unchanged if finitely many Γ's, each involving several new R's, are allowed instead. All theories we consider are assumed to be theories in the first-order logic with equality (as in [8]), to have finitely many nonlogical symbols, and to be recursively axiomatizable.

The “traditional” method of presenting the subject-matter of symbolic logic involves setting down, first of all, a basis for a propositional calculus—which basis might be a system of natural deduction, an axiom system, or a rule concerning tautologous formulas. The next step, ordinarily, consists of the introduction of quantifiers into the symbol-set of the system, and the stating of axioms or rules for quantification. In this paper I shall propose a system somewhat different from the ordinary; this system has rules for quantification and is, indeed, equivalent to classical quantification theory. It departs from the usual, however, in that it has no primitive quantifiers.

The class of primitive recursive functions may be defined as the closure of certain initial functions, namely the zero, successor and identity functions, under two schemes, namely composition (sometimes called “substitution”) and recursion. For a detailed definition the reader is referred to any standard work, for instance p. 219 of [2], by Kleene.