@user267839 Having the background theory be "truly formal" doesn't absolve us from formalizing our definitions in it... it obligates us to.

I'm not sure I understand what you're saying

The formulas in the langugage of the background theory aren't "formalized", or even discussed in the background theory... that's the metatheory.

It's the formulas of the object theory that need to be encoded as sets in the background theory... so as to write things like "M\models \exists x\varphi(x)" in the background theory.

Now, in this case we have a particular formula in language of the background theory, that we're going to need to mimic in the object theory. So, in the metatheory (where we talk about the formalization of the background theory), we take that background theory formula (the formula we might abbreviate by "x is a minimal inductive set") and we write, in the language of the background theory, a correponding definition of a formula in the object theory.

Which we can do since they are effectively the same.

@spaceisdarkgreen Essentially, what I was asking for - pinning down the formalist's picture - was about the role & 'raison d'être' of this "mysterious" procedure "encoding formulas as sets". So far I understand your last explanations correctly, here this is applied only to formulas of object theory and the reason to do it, is precisely that this "encoding formulas as sets" serves here as "gadget" to pick formulas of object theory and translate these into terms in background theory, right?

@spaceisdarkgreen More concretely, eg we want that our background theory T' "formalizes" model theory of the object theory T. This would imply that background theory have to be able to include formulas like eg "M\models \exists x\varphi(x)". But a priori it "not understands" what the part "... \exists x\varphi(x)" as a priori $\varphi(x)$ is phrased in language of object theory and not of background theory. Now - so far I understand the "magic" of

@spaceisdarkgreen this "encoding as sets" precedure correctly - it picks this formula $\varphi(x)$ - a prori regarded as object from object theory - and produces a "copy"/ reproduction of $\varphi(x)$ as term in background theory, making the formula "M\models \exists x\varphi(x)" linguistically understandable for background theory's language? Is this the idea & raison d'être for this "encoding as sets" machinery here?

@spaceisdarkgreen Maybe another point ad "It's the formulas of the object theory that need to be encoded as sets in the background theory": What you mean by "sets in background theory"? From formalist's perspective backgrd theory is treated strictly as a formal theory, that consists as any formal theory of a bunch of wf formulas (=axioms) written in certain fixed undrlying formal language ( ie inclding a alphabet, syntax rules apparatus). What does it mean to say that a "formal theory contains sets"?

@spaceisdarkgreen ...Maybe to avoid talking past another: When one says "formal theory" I'm thinking of this datum: en.m.wikipedia.org/wiki/Theory_(mathematical_logic) And so far I understand your point formalists treat object theory and backgrnd theories as formal theories, right? (...to contrast them from informal metatheory) But a formal theory "knows" only formulae phrased in underlying forml language.

Therefore I not understand what you actually mean by "formulas of the object theory that need to be encoded as sets in the background theory" as a formal theory "not knows" sets. Or, do you mean by this an additional step that these "formulas encoded as sets" are implemented into extension of background theory as added NEW constant terms?

A guess:So, say $\varphi(x)$ is a formula in object language, then we as first step we "encode it as certain set" - say $S:=S(\varphi(x))$- which at this stage only lives in metatheory, but then - in next step - associate a constant symbol $c_S$ with this set S and extend now the background theory by this constant $c_S$. Is this the trick you are refering above to when you say "formulae of obj thoery encoded as sets in the background theory"?

@user267839 The background theory is a set theory. The process of "encoding formulas as sets" is formalizing the mathematical definition of formulas in set theory, where literally every mathematical object is a set.

The formal background theory is (semantically) about sets. It knows sets and only sets in that sense.

@spaceisdarkgreen When you say a formal theory (...as formalists we assume background theory is a formal theory) is a "set theory" you mean by this a formal theory (... in sense of the wiki link from prev comnt) subjected to restrictive condition that it's underlying formal language has to be given by only one symbol $\{ \in \}$, right? If yes, then I still not understand the sentence "formulas of the object theory that need to be encoded as sets in the background theory":

But if background theory is a formal theory - independently of if it is additionally also a set theory - it consists by definition of a bunch of formulas phrased in its formal language, or not? (As previously you wrote that from formalist's view object- and background theories are seen as formal theories)

@spaceisdarkgreen More precisely, as you write "The formal background theory is (semantically) about sets". Yes, but itself as "datum" the formal background theory consists of a bunch of formulas, not more not less, do you agree? So even if backgrd theory is about sets, it consist as every formal of theory just of certain formulas, not eg sets. Thus I not understand what you mean in

previously quoted sentence that formulae of object theory are encoded as sets(!) in background theory. Surely, as you said, background theory used to reason about sets, but itself it not contains sets, only some formulae (declared to be its axioms)

@user267839 To quote Alex Kruckman's answer to your question, "Gobo is a fraggle".

@spaceisdarkgreen But here I'm just refering to definition in en.m.wikipedia.org/wiki/Theory_(mathematical_logic). Just that a formal theory consists by definition of some sentences, that's it. On the other hand, where you wrote "formulas of the object theory that need to be encoded as sets in the background theory" raises a "domain error" problem: If a container consists of formulas you cannot put sets in it .

Or, maybe I misunderstood what you actually meant in the quoted sentence...

@user267839 I mean what I said in the last sentence I wrote

write down some long formula in the language of set theory defining what a formula is, along the lines of Andres's notes I sent you earlier

And also, for a specific formula, we can write down a definition in the language of set theory of that formula, which the background theory will be able to prove satisfies the previously mentioned definition of what a formula is

that latter thing would be what \ulcorner \varphi\urcorner varphi is