@spaceisdarkgreen Just to avoid confusions about the machanism presented in the linked script: Strictly speaking there happens several steps. Firstly, there is introduced an inductive process associating to formulas from object theory(!) cerain sets (in a compatible way), so something like $\phi(x) \to S(\phi(x)) \in SETS. Then the formulas from background theory,eg like Form(x) which "detects" if the inputed x is a wf formula of the object theory is strictly speaking

are evaluated in sets. Eg if under above map we map an object language fmla \phi(x) to a set S(\phi(x)), then strictly speaking the predicate Form(x) is evaluated in sets(!) and what it does is that it feedbacks if a set S where it is evaluated comes from a fmla from object theory via the above map \phi(x) to S(\phi(x)). Did I understood it correctly?