 Note that in the general case a formula \(\varphi(x_1,\ldots,x_j,X_1,\ldots, X_k)\) of \(\mathcal{L}^2_a\) may have both free number variables \(x_1,\ldots, x_j\) and free set variables \(X_1,\ldots,X_k\). If \(R \subseteq \mathbb{N}^j \times \mathcal{P}(\mathbb{N})^k\) is defined by such a formula, then it is said to be analytical. Kleene (1955a) proved a normal form theorem for analytical relations which shows that if \(R\) is analytical then it is definable by an \(\mathcal{L}^2_a\)-formula of the form 