:6626408 Ad "metatheory and background theory are just names." Sure, but it still not completely clear to me from above in which relation you see these two terms to one another. Firstl you wrote: "the "metatheory" is what I'm referring to as the "background theory"." So one may think at this stage you treat these synonymously. But next - that exactly the part I not completely got - you wrote "However, if we're talking formalism, what I'd call the "metatheory" is the

@spaceisdarkgreen theory we use to talk about the background theory, namely to talk about its syntax and formal proofs (the terminology here is not very standardized, though)." Aren't these contradicting statements? First sentence suggests you want to use metatheory" and "background theory" synonymously, but in second that "metatheory" is used to talk about backgrnd theory", so a "meta-object theory relation" between these two.

@spaceisdarkgreen So which relation between "metatheory" and "background theory" you consider above?

@spaceisdarkgreen Could you eaborate this a bit? Say we state with some theory $T$ - so a datum consisting of an alphabet, syntax rules for building wff formulae, deductive apparatus, etc - and we want to "formalize" it in set theory. How should one think of it? That we should think of this proceducure as "coding into set theory"? Roughtly, does it mean that we associate to each wf formula of this theory a set in "compatible" way? (Ie consitent with syntactical building rules of the theory)

@spaceisdarkgreen But at all, in down to earth terms, to say we "formalize $T$(in set theory)" in its gist associates just certain sets to formulae of $T$, right? (...the picture I had in mind here is the Gödel numbering)

@user267839 yes to your last two

To the others I explained what I perceive as the two levels for the platonist vs the 3 levels of the formalist. The platonist’s first and second level correspond to the formalist’s second and third.

For the formalist I’m calling it 1) metatheory 2) background theory 3) object theory. For the platonist, 1) metatheory 2) object theory

But then I reverted to calling background theory metatheory since it’s confusing as it corresponds to the platonist’s metatheory

And you can call 1) for the formalist “metameta theory” if you like

It’s just that i tend to use metatheory to mean the top level, regardless. You can call them what you want, as I say, it’s not very standardized

@spaceisdarkgreen Correct me if I'm thinking to simple here, but isn't then when we say we "formalize a theory $T$ in set theory" equivalent to just picking a model of this theory, but subjected to specific condition that all elements of this model are sets (as a "set valued model")?

@user267839 no, it’s completely different

A model associates the semantic stuff to sets, not the syntactical stuff.

@spaceisdarkgreen Hmmm, I see, what I wrote also elready not make any sense as eg a model assoctates to a predicate symbol a boolean valued function, etc. But, so far I understand what in "formalizing theory $T$ in set theory" is really going on is that it's really a map from all wf formulae of this theory $T$ to class of sets (+ compatibility conditions wrt syntax of $T$). Is this correct?

@spaceisdarkgreen At least, drawing inspiration from Gödel numbering, where the latter even more restrictively maps formulae to finite sequences of integers

@spaceisdarkgreen But isn't it stange? Say $x,y$ are abstract free variables in language of our theory and we want to encode in sets its conjunction. You suggested to take string $(3,x,y)$. But what is the set where such string should live? Especially, why should it "know" what is $x$ and $y$?

@spaceisdarkgreen #Un update to sumarize the aspects of the problem: Googling around a bit for term "formalize a theory" there seemingly a plenty of different - and a priori unrelated - procedures associated with this. In most simple minded version this just refers just to procedure to "translate" an informal theory - eg as those written in "informal natural language" into strict formal theory: en.m.wikipedia.org/wiki/Theory_(mathematical_logic)

@spaceisdarkgreen In concrete this mean we translate informal sentences in syntact well def strings of such formal theory. Presumable something completely different should be mean to "formalize model theory" (...what I not know what it should actually mean) ...and if it has some conceptional links to what you used when saying "formalizing a theory in set theory"

@spaceisdarkgreen Can the concept of "formalizing a theory (in Bla)" be precisely described what it should actually mean? (where "Bla" should be expected to be some "foundational" structure) In case of Bla= set theory you wrote that loosely this should be sothing like "coding the cosidered theory somehow in set theory". Can it be made more precise in which way this carried out?

Do we really do this by just finding some set and looking for a map which maps formulae of the considered theory to elements of this set? (...this is at how Gödel numbering work) and if we manage this we call the theory "formalized in set theory"?

@spaceisdarkgreen Could you maybe recomend sources discussing this? Is it standard?

Update #2: Maybe I see what "formalize model theory" (...what I mentioned in prev comment) should be: Is it equivalent to existence of a formal background theory (...so "stage 2 structure" in formalist's hierarchy you adressed above) which is "able to express" statements about models of the object theory, eg like $M \models \phi$ as wf formula. Is this what it means "formalize model theory"?

@spaceisdarkgreen ...if that's correct so far, think my confusion reduces to pin down what it should mean to say "to coding concepts ( or sentences of a theory) into definitions involving sets." What does it mean?

@spaceisdarkgreen Update #3: Or, think I see. You mean "coding concepts into definitions involving sets" precisely in sense described in the link caicedoteaching.wordpress.com/…, right?