Model unspecific Witness of an Existence Proposition

Question

Let $T$ be some first order theory ( eg ZFC; feel free to assume this for the next), $\varphi(x)$ is a well- formed formula in $T$'s underlying language, and assume that the proposition $\exists^! x\, \varphi(x)$ is provable in this theory.

This has as consequence that for every model $M$ of $T$ $M\models \exists^! x\, \varphi(x)$, what implies there exist for every such model a set $\omega^M $ in $M$ witnessing $M\models \exists^! x\, \varphi(x)$.

Question: In this answer Alex Kruckman wrote following part which confuses me a bit:

[...] (1) Let $\varphi(x)$ be the formula "$x$ is a minimal inductive set". $\newcommand{\ZFC}{\mathsf{ZFC}}\ZFC$ proves $\exists^! x\, \varphi(x)$ (there exists a unique minimal inductive set). We call this unique inductive set $\omega$. If $(M,E)$ is a model of $\ZFC$, then $M\models \exists^! x\, \varphi(x)$. The unique witness is an element of $M$, which we denote by $\omega^M$.

While I understand so far what it means for $\omega^M$ to be the unique element of model $M$ witnessing the truth of $\exists^! x\, \varphi(x)$ in $M$, beeing in $M$ exactly the unique set such that the ( by definition boolean-valued) predicate $\varphi(x)$ evaluates exactly in $\omega^M$ to 'true'.

But what I not understand is the "nature & affiliation" of $\omega$ which Alex introduced above in quoted paragraph. On which "level" it exists at all? It seems not to be affiliated to some specific model like this is the case with the $\omega^M$. On the other hand it appears to me that in order to be able to talk about "a witness of some existence proposition" we need to pin down a model where this proposition is true and which actually contains such "witnessing element" as element. Or does notion of "witnessing element" still make sensewithout fixing a model?

If the latter is the case, can it made be more precise to what $\omega$ actually belongs appearing a bit to "be floating in nowhere"? Is it regarded as an element of some say "universe" we have fixed for all the time in background; andso in order to give actually a meaning to such "model unspecific witness" $\omega$ we actually have to assume tacitly Platonic picture?

In other words, what is meant precisely by an "external object" $\omega$ witnessing proposition of shape $\exists^! x\, \varphi(x)$ contrasting from pretty clearly declared "internal objects" $\omega^M$ existing as unique elements of a particular models witnessing truthness of $\exists^! x\, \varphi(x)$ there?

Answer 1

Let's say we want to reason logically about fraggles. You and I may have different philosophical convictions about the nature and reality of fraggles, but we have a shared interest in proving things about them. So we agree on some basic assumptions about fraggles, and we start proving things from these axioms.

Now let's say we prove "among the fraggles, there is a unique greatest explorer". Then we can agree to give that fraggle a name. We decide to call him Gobo. Now we can continue proving things about fraggles, and in our proofs, we can make reference to Gobo if we want to. Every time we mention Gobo in a proof, we could just as well replace the name Gobo with its definition. For example, if I assert "Gobo has purple hair", we could just as well expand that to "there is a fraggle who is the greatest explorer, and that fraggle has purple hair".

Now, maybe you believe that there's actually a community of fraggles living in a cave below your workshop, which satisfy our axioms. Then you believe that there's a real fraggle down there who is the greatest explorer, and he's the one we're calling Gobo. Our axioms give us some partial information that allows us to make conclusions about the real fraggles. But, for example, it's possible that Gobo has purple hair, but we can't prove it from our axioms!

On the other hand, I think that fraggles are just imaginary creatures we're telling stories about. Then I don't think Gobo is real in any sense. In particular, I don't think Gobo has have any specific properties (like purple hair) beyond the ones we can prove from our axioms.

Our friend Jim points out another perspective: Maybe there are actually lots of communities out there in the world that satisfy our axioms about the fraggles. Then in every such community $C$, there must be a unique greatest explorer. We could call the members of $C$ "fraggles$^C$" and call the unique greatest explorer "Gobo$^{C}$". Then, Jim says, when we reason about Gobo, what we're really doing is simultaneously reasoning about all the Gobo$^{C}$s at once. If we can't prove "Gobo has purple hair", it could be that if $C$ and $C'$ are different communities, Gobo$^{C}$ has purple hair and Gobo$^{C'}$ has green hair.

As you can see, our three perspectives on what we're doing when we talk about Gobo are all pretty radically different. But that's ok! It doesn't stop us from having productive discussions about fraggles together, once we decide on our basic axioms.

If someone asks us "what kind of object is Gobo?", we can all sincerely answer "he's a fraggle, what else?".

To summarize my analogy into an answer to your question:

What is meant precisely by an "external object" $\omega$?

That depends on your philosophical convictions. There are many points of view on this, including several which (to my mind) are all very reasonable. Personally, I think that if one is going to devote a big part of their life to doing mathematics, it would be very strange not to spend some effort developing a personal philosophical view about the subject. But for the purposes of actually doing mathematics, it doesn't matter.

Answer 2

The way it shakes out in a formalist perspective is that any time we have proven a statement of the form $\exists !x\psi(x)$, that entitles us to definitionally extend our background theory with a new constant symbol $c$ and a new axiom $\psi(c).$ So $\omega$ is just this for the formula $\varphi(x).$

Note that from this perspective, when we write, e.g. $M\models \exists ! x\varphi(x)$ or $M\models \sf ZFC$ in explaining what $\omega_M$ is, this is an abuse of notation. Here $\varphi$ is not a formula, but rather an analogue of a formula formalized in our background theory (and similarly the reference to "$\sf ZFC$" is to a formalized version of this set of formulas). It just so happens that our background theory is $\sf ZFC$ (or something close enough to it) so the formula $\varphi$ in our background language has a corresponding formal object $\ulcorner \varphi\urcorner$ that our background theory can talk about $M$ satisfying.