@RobertShore We’ve already proven existence and uniqueness so just adding $\psi(c)$ works. That axiom works too.

I'm not completely sure if I got what you wrote in 2nd paragraph on that $\varphi$ is not a formula in sense of that the term $M\models \exists ! x\varphi(x)$ taking literally abuses notation. Could clarify it in more details? I understood you as follows: Firstly, $\varphi$, as well $\exists ! x\varphi(x)$ are well defined formulae in a theory $T$ we started with, of which $M$ is a model. When you said that writing $M\models \exists ! x\varphi(x)$ is an "abusion of notation", do you mean by this that this is intrinsically a proposition of "backgronud theory" used to reason about $T$ and

its models, so a "metatheory" about $T$, whose underlying language a priori differs from that of $T$. Is that what you mean there by "abusion of notation"? (...I assume you use "background theory" & "metatheory" synonymously) What would be correct phrasing of this formula to avoid abusion of notation issues there? As $M\models \exists ! x \ulcorner \varphi(x) \urcorner$ ?

In other words, do I understand you correctly that you intended there to emphasise that when writing $M\models \exists ! x\varphi(x)$ we writing an intrinsically metatheoretic statement, and so the language of metatheory a priori "not knows" what $\varphi$ should actually mean, (...just like if one would like to write an essay in English and suddenly insert a Chinese letter), it only recognizes its "duplicate" we calling $\ulcorner \varphi\urcorner$ (...like if we use in prev analogy the Chinese letter as an abbrevitation of something in English). Is that what you mean in 2nd paragraph by

"notation abusement"?

So, should the distinction between $ \ulcorner \varphi\urcorner$ and $\varphi$ serve just to distinct carefully if we talking about $\varphi$ in "object theory" or its background theory?

@user267839 That is a lot of followup questions. Yes, $\omega$ is often referred to as "the natural numbers of the metatheory" and the "metatheory" is what I'm referring to as the "background theory". However, if we're talking formalism, what I'd call the "metatheory" is the 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). The point is "$\varphi(x)$" and "$M\models \exists !x\varphi(x)$" are both formulas in the background language, the latter of which requires a lot to unpack.

@user267839 and yes, by "abuse of notion" I just mean it's important to note a distinction between $\varphi$ and $\ulcorner \varphi\urcorner$ (one of which is a formula in the background language and the other of which is a term in (a definitional extension of) the background language) since I think it's pertinent to the difference between $\omega$ and $\omega_M$ in a formalist perspective.

I see you asked a followup. I initially put the following comment under that, but decided to instead delete it and put it below, as to not deter others from interjecting:

One thing I suspect you're missing is an understanding of what it would entail to actually write "$(M,E)\models \exists !x \varphi(x)$" out as a formula in the language of set theory (using a uniform satisfaction relation) and how that formula would depend on the formula $\varphi$. (And the reason I was emphasizing these formal minutiae is because the upshot of your question seemed to me to be can we make sense of "the real natural numbers" and model theory without Platonism... and if we're going to do that we might as well be somewhat precise about how it works.)

I'm a bit confused, let me try to summarize the setting, maybe this offers where my understanding problem sits. We start with "object theory" $T:=ZFC$ and statements $\varphi(x)$ and $\exists^! x\, \varphi(x)$ are formulae of this theory (more precsly, 1st is a predicate, 2nd a proposition wrt this theory). In contrast, statements like $T \vdash \exists^! x\, \varphi(x)$ (latter provble in $T$ or $M\models \exists^! x\, \varphi(x)$ are intrinsically statements in metatheory of $T$ -say $T'$, which a priori has its own formal language and is used to reason about $T$ as object theory, right?

In context above this metatheory $T'$ of $T$ is also taken to be $ZFC$, this we have to be careful with the formula $\varphi$ as due to this - that we have taken $T$ and $T'$ to have same language $ZFC$, it is a wff (well formed fmla) in object theory $T$, but as well in metatheory $T'$, but as metatheory used to be reason about object theory $T$, we have to distinguish if we consider $\varphi$ as formula in $T$, in $T'$, or as "object" from $T$ about which we reason about through eyes of metatheory $T'$, and so treats $\varphi$ from $T$ also as a term/variable/constant of $T'$. Is this

what you mean above? So, in order to reason in metatheory $T'$ of "object theory" $T$ we indicate a wff formula $\varphi$ $T$ when reasoning about it in metatheory $T'$ as a term and denote it as "term" $\ulcorner \varphi\urcorner$. So for example in metatheory $T'$ we can form wff eg $\ulcorner \varphi\urcorner= 3$, etc. And so, in metatheory the correct (=wff) statement (...so a metatheoretic statement) that in model $M$ of $T$ the statement $\exists ! x\varphi(x)$ of $T$ is true, phrases - if we would insist on avoiding abusion of notation -

as $M\models \ulcorner \exists ! x\varphi(x) \urcorner$, right? Did I now understood your point correctly with the issue on abusion ofnotation in expression $M\models \exists ! x\varphi(x)$ and usage of $ \ulcorner . \urcorner$ to resolve it?

...although, if even if what I wrote before is correct, I not understand what you actually mean in "However, if we're talking formalism, what I'd call the "metatheory" is the theory we use to talk about the background theory [...]" Wouldn't this be a metatheory of metatheory? (so far I understand you correctly that you use background- and metatheory synonymously)?

@user267839 I think you're mostly on the right track, but could we just start again from the top since it's gotten to be a bit of a mess? Let $T$ be ZFC. $T$ proves there is a unique minimal inductive set... call it $\omega$. That's what $\omega$ is... the natural numbers according to $T$.

@user267839 Now, in $T$ we can also develop model theory like we develop any other branch of mathematics by coding concepts into definitions involving sets. In particular, we'll define formulas in the language $\in$ of set theory as a certain collection of sets, and we'll define what it means for a relational structure $(M,E)$ to satisfy a sentence in the language of set theory. We can write down a definition of what it means for a given sentence to be an axiom of ZFC as well.

@user267839 And then, just like we established previously that $T$ proves there is a unique minimal inductive set, we can prove, in $T$, that any relational structure $(M,E)$ that satsifies all of the ZFC axioms (according to our formal definition) will satisfy the sentence "there is a minimal inductive set". Then we can show in $T$ that implies that there is a unique element $\omega_M\in M$ such that "$\omega_M$ is the minimal inductive set" holds in $(M,E)$.

@user267839 And yes, we can refer to $T$ as the "metatheory" and ZFC as the "object theory" here.

@user267839 Then, continuing to work in $T$, we can ask questions, like, "is $(\omega,\in)$ necessarily isomorphic as a relational structure to $(\omega_M, E)$" and prove that that's not always the case, assuming a model of ZFC exists.

@user267839 And to circle back to your question, this does not necessitate any kind of Platonistic commitments, since we are just analyzing the "metatheory" T formally.

@user267839 Now, we could also just forget about $T$, and say there's a real universe of sets satisfying the ZFC axioms and so much more, and say $\omega$ is just the (real) natural numbers, and there are also these things called models of ZFC that necessarily have an element they think are the natural numbers.... that would be Platonism.

@user267839 The formalist thinks that while the Platonist may be incorrect that these things actually exist, their reasoning process is still interesting and can be modeled by proving things in $T$, as we sketched above.

(Which is why I say the formalist’s metatheory is really the meta-meta-theory.)

(And also why I indicate that the formalist is more pedantic about the distinction between the formula in the metatheory and the object theory… they are actively formalizing the platonist’s metatheory rather than leaving it informal like the platonist.)

In last comment I meant something more abstract: Say $T$ is any theory, $\varphi(x)$ any wff in $T$, assume that the proposition $\exists ! x\varphi(x)$ (...we assume that language of $T$ includes all the used symbols) can be proved in $T$ and $M$ a model of $T$ in usual sense. Then in metatheory of $T$ -let call it $T'$ - we expect that we could write down the formula $M\models \exists ! x\varphi(x)$.

Simply, as that's the job of metatheory to reason about $T$ as its "object theory". Now the question is, in which sense the formula $M\models \exists ! x\varphi(x)$ as formula in metatheory $T'$ is "ill posed" or includes "abusion of notation", making it neccessary - if we want to work in full formal rigorosity - to make use of brackets $\ulcorner . \urcorner$?

My guess was that the core problem was that the expressions like $\varphi$ and $\exists ! x\varphi(x)$ are phrased in language of object theory $T$, so its metatheory $T'$ a priori "not knows" $\varphi$ as formulae and the trick with brackets $\ulcorner . \urcorner$ was that in order to keep foull formal rigorousity inside metatheory $T'$ of $T$ only expression $M\models \ulcorner \exists ! x\varphi(x) \urcorner$ would make sense

where inside $T'$ the expression $\ulcorner \exists ! x\varphi(x) \urcorner$ is introduced as constant/term in order to allow the metatheory to do what is expected from it: to reason about $T$ as "object theory".

In other words, the connection between propositions $\psi$ in theory $T$ and expressions \ulcorner \psi \urcorner$ should be that the latter are given as terms in metatheory $T'$ or $T$. Do you agree?

So, refereing to your penultimate comment to above situation that "distinction between $\varphi$ and $\ulcorner \varphi\urcorner$ (one of which is a formula in the background language and the other of which is a term in (a definitional extension of) the background language" I assume that this works only in specific situation where object theory and metatheory have same language - here ZFC, right?

Otherwise I not know what you mean there: Isn't the idea of metatheory to treat formulae of object language as its terms? But here you refer to $\varphi$ living in metatheory, and not object theory, as I would expect keeping in mind that $\ulcorner \varphi\urcorner$ has to be a term in metatheory, conpared to what I wrote in prev comments