 The next step up the analytical hierarchy involves the characterization of the \(\Pi^1_1\)-definable sets. S. Kleene (1955a) originally established his normal form theorem for \(\mathcal{L}^2_a\)-formulas using a variant of the language of second-order arithmetic which contains function quantifiers \(f,g,h,\ldots\) which are intended to range over \(\mathbb{N} \rightarrow \mathbb{N}\) instead of set quantifiers intended to range over \(\mathcal{P}(\mathbb{N})\) (Rogers 1987, ch. 16.2). In this setting, it is possible to show the following: