Recently, I attempted to generalize the fixed-point lemma and proved the following:

Let $ F_n $ be the set of all formulas with $ n $ free variables in $L_{PA}$.<br>

Let us define the unary function $ f $ by $ f(\sigma) = \ulcorner \sigma \urcorner $, where $\sigma$ will be any element of $F_n$​, i.e., where $\sigma$ will be any formula in $L_{PA}$ with $n$ free variables, and $\ulcorner \sigma \urcorner$ will be its Gödel number. Therefore, $ f $ is not a function within $ L_{PA} $.<br>

Let $ \mu $ be the smallest set of unary functions，each of which domain is $F_n$ , that satisfies:<br>
$(1). f \in \mu $<br>
$(2).$For any $f_1, f_2, \ldots ,f_n \in \mu$, let unary function $g$ defined by $  g(\sigma) = \ulcorner \sigma(f_1(\sigma), f_2(\sigma), \ldots, f_n(\sigma)) \urcorner $, where $\sigma$ will be any element of $F_n$​, then we have $g \in \mu $.


Then: for any $ \psi \in F_m $ and any $ n + m $ functions $  f_1, f_2, \ldots, f_{n+m} \in \mu $, there exists $ \varphi \in F_n $ such that:

$$ PA\vdash \varphi(f_1(\varphi), \ldots, f_n(\varphi)) \leftrightarrow \psi(f_{n+1}(\varphi), \ldots, f_{n+m}(\varphi)) $$

The proof itself is straightforward, but I am unsure under which existing research this result is covered, that is, what is the limit to which the fixed point lemma can be generalized? Recently, I have been reading C. Smorynski's article "Fixed Point Algebras." Am I heading in the right direction with my research?