@spaceisdarkgreen A nitpick: You refered a couple of times to "formalize the model theory (of a theory) in a language". Could you sketch what this procedure means? A guess: Say we have a formal theory T. Then, does it mean to "formalize the model theor of this T in certain (formal) language L' - which, a priori has noting to do with language of T itself - a procedure assuring that formulas of this language L' can evaluate in their variables statements about metatheory of T? Eg,

the language L' would be expressible enough to incluee a statement like $M\models \psi$ where $M$ is a model of T and \psi a wf proposition in language of T?

@spaceisdarkgreen Another point ad: "By "encode formulas as sets" I mean the same thing "write formal definitions of formulas from logic/model theory in the language of set theory" ": So you mean by this that we there produce formulas in language of set theory which accept as arguments formulas from logic/model theory and carry information if the inserted argument (=formula from logic\model theory) is well formed? Eg, \psi(x):=" x is well formed formula in object language".

Is this what you mean in quoted sentence?

In other words, that this $\psi(x)$ is a predicate formula phrased in background language - which "accepts" as arguments evaluated in x formulas from object theory and which decides if the input x is syntactically well formed as formula ob object theory?

If what I wrote in 2nd part is wrong then - passing a step back - what is meant by "to write formal definition of a formula"? Write as what, and where? As a predicate in background language?

@user267839 Yes. write a formula Form(x) in the background language that expresses "$x$ is a formula".

says "x is an ordered pair whose first element is 1 and whose second element is a formula or an ordered triple whose first element is 2 and whose second two elements are formulas or..." etc, with the recursiveness of the definition handled formally as usual.