Regarding scenario 3. I would like to clarify to following:. Say we consider a theory (so as a collection of formulas phrased in certain underlying formal language (=alphabet + grammar/ syntax rules) and want that the formal language allows us to to write down formulas refering explicitly to natural numbers or write down formulas with them. In which way the natural numbers should be "included" in the underlying formal language in order to be able to write formulas refering to integers? As constant symbols $0,1,2,...$? Or is to do this in that way in general problematic?

This is a bit motivated by vague question "when can I write a formula refering to natural numbers"?

@user267839 If by "formula" you mean well-formed formula, then I do not understand why you chose scenario 3 to ask about formulae referring to natural numbers. Are you asking about if we have a formal theory (either a formal metatheory, or formal object theory) and if it seems that the language allows us to talk about natural numbers (via constant symbols or otherwise), how to know for sure (in a very strong sense of sure) that the formal theory is referring to THE natural numbers? If this is the case, we never really know. (1/2)

(2/2) An analogous question: Is the formal theory of first-order logic contradiction-free? It's provable that it is, in a sense. Its proof (formulated in Platonistic logic) shows that if there were a syntactic contradiction in FOL, then there'd be a contradiction in Platonistic logic which is in turn assumed absurd. How do we really know that there's no contradiction in Platonistic logic? Point being that there are no free lunches, you need to make clear what you consider to be "THE natural numbers" first and only then can you hope to reason about whether your theory is talking about them.

(3/2) Whether this mission to pin down THE naturals can succeed, is a different question, and may be impossible depending on the background and criteria for "succeeding".

yes, I mean a "formula" as an "element" of a theory ( recall a theory is a collection of formulas phrased in certain underly formal language), so especially beeing syntactically correct wrt this language ( ...I assume that's what you mean by well- formed; if yes, then my answer is also yes). What I meant by "formula refering to integers" ( more precisely the reason for it's non existence) is meant in the sense of the 7th comment below this answer by Alex Kruckman, where he wrote that it "is impossible to

form sentences in language of ZFC using references to external $\omega$" and my concern was what is the formal reason why that's indeed not possibe. Aspecially I' m not completely sure what it all encompasses to say that a formula refers to external integers (following your answer I conjecture that Alex meant there "external integers" in the 2nd sense in terms of our answer)

(2/2) for $\varphi^{(M, E)}$ the same unique existence, more precicely $\exists ! x E M : \varphi^{(M, E)}$ which is the aforementioned relativization. Denote this unique set by $\omega^{(M, E)}$. Elements of this set are the "internal naturals of (M, E)". We (tend to) view our "external naturals" from $\omega$ as the true naturals, insofar as ZFC "truly" describes "(a subset of) the Platonistic world of sets", if there is such a thing.

On "Namely, define "the set of natural numbers" to be any set that is a minimal inductive set". Minimal with respect to which inductive sets, where do they live, don't we need some domain, ie to take an explicit model first to make the phrase "minimal among sth" meaningful? Indeed, if $M$ is a model then a set $m \in M$ is minimal inductive, if there is no smaller inductive set in $M$(!) which is contained in $m$, and if $M$ is a model of ZFC then such minimal induct set $m := \omega^M \in M$ is even unique because $M \models \exists! x: \varphi(x)$.

Due to uniqueness $\omega^M$ can be formed as intersection of inductive sets living in $M$ as sets. But note that that we are talking about sets inside $M$. And that's my point: I not understand how one can say that certain set - say $\omega$ - can be called "integers" before we haven't explicitly picked a model where it lives, in other words it seems to me to be meaningless to say "$\omega$ are some integers or nat numbers etc" before haven't picked a model of ZFC where it lives as set, ie $\omega \in M$.

Recall that to say that ZFC (or any other formal theory) "proves" a proposition - say $\Psi :=\exists! x: \varphi(x)$ just means that we can derive this proposition from given axioms of the theory via "legal" deductive rules/ "rules of inference" which the theory includes. At this stage we cannot really "take a set of integers", only that the proposition is deducable from ZFC theory axioms. So far I understand we can only have a set "in our hands" which are actually "integers" after having picked a model of this theory, which would actually contain a concrete set of integers.

Or, is what we actually call "internal integers" also just those from at all tacitly specified model, say the "platonic model" - say $M_P$ - of ZFC? ( Not sure, cannot we use term "model" and " universe" synonymously; I not see a reason why not) So "external" $\omega$ means just $\in M_P$ as honest set, but I not sure maybe I misunderstand the point hardly.

In terms of ZFC, which is a formal syntactic theory, with its alphabet, formula definition, derivable objects (can be formulae but need not be), proofs and so on, "exists unique minimal inductive set" is a well-formed formula which can be proven from the axioms using the rules of inference. The word "set" there is superfluous. It is the useful narrative we tell ourselves that ZFC is talking about sets, not part of the formal language. There is no "x is a set" predicate; the formal deductions don't use "is a set" anywhere; we humans informally interpret ZFC as talking about sets.

@user267839 (The platonic model of ZFC, I denote this by U (or V), is not a set model, it is a proper class model. In the context of ZFC, it is actually a syntactic conceptual shorthand for the formula $x = x$. One can analogously view other definable-with-parameters classes within ZFC, but there can be further classes if you consider some true class theory. But this is beside the point here, I think.)

On "In terms of ZFC" part: Yes, exactly that was my point, from ZFC axioms we can derive certain formula $\exists! x \varphi(x)$ and that's it. To talk about certain existing sets make sense only once we having choosed a model $M$ whose underlying domain ("bare" $M$ forgetting signatues) contains sets as its elements. That's exactly why I was confused about term " external integers" which seemingly was introduced without specifying a model of the theory. Ok, if we allow the models to have a class as domain ("class models"), then

what Alex called " internal integers" $\omega$ lives as element there, so we tacitly passed at this moment to the Platonic model, right? If this so far make sense, do you see why it is the case what Alex wrote in 7 th comment below the answer I linked in previous comments that itis impossible to form sentences in language of ZFC using references to "external $\omega$? My conjecture: Just bcause this external $\omega$ isn't part of the language of ZFC, in the sence thata sentence refering to it would be invalid wrt underlying language, and that's it? In plain wrds, the language don't know it?

@user267839 Yes, ZFC derives derivable objects which very commonly are formulae. The point is not that you need to start fixing models to talk about sets. The point is that the talk about sets is "just in your head", a helpful but removable fictional narrative to make sense of what you are doing. Whether you take the further truly platonistic view is up to you, not really crucial (you could pretend to be platonistic, you could pretend to be playing a game, be a formalist etc). But depending on the situation, the narrative can also help to come up with results which otherwise'd be hidden.

Further, you cannot extend ZFC with the axiom that $\exists x: \varphi(x) \wedge |x| > |\omega|$. This would be a syntactically inconsistent system to begin with.

It is best to ask Alex what exactly he meant. We, of course, can talk about the set of natural numbers as the smallest inductive set in ZFC (in fragments, such as ZFC minus Inf we'd need an alternative formula). And if we call these "external naturals" then via the defining formula we can indeed talk about the unique ω.

Regarding: "The point is not that you need to start fixing models to talk about sets. The point is that the talk about sets is "just in your head", a helpful but removable". Not completely persuaded. Say we pick two models $M, N$ of theory ZFC with their "integers" $\omega_M, \omega_N$ ( ie the sets in $M$ resp $N$ witnessing the truth of formla $\exists! x: \varphi(x)$ from

before). As sets these can behave extremely different ( eg one externally countble, other uncountable, etc), so it seems having this example in mind (... at least if I'm not making some thinking error) that before we haven't fixed a concrete model it might be dangerous to talk about sets (like "integers") as these could show extremely different behaviour in dependence of choosen model, or does this example with different integers missing the point you intended to emphasise?

Therefore I have the problem to realize what is actually meant by "smallest inductive set" in the theory ZFC, before haven't actually choosen a model where have actually a honest smallest inductive set. Maybe I'm reasoning from wrong viewpoint, do you see how resolve this confusion? Ie that it still "makes somehow sense to talk about a concrete set - eg the like smallest inductive set - in theory without specified a model?

This issue reminds me a bit (...maybe a complete wrong analogy, but not sure) if we want to talk about a number $n$ and we consider the polynomial ring $\Bbb Z[X]$ and would talk about the indeterminant $X$ as kind of "generic" $n$ before actually specified $X \mapsto n$. Is this scenario/analogy similar to what in going on above with to refer to a "small inductive set" inside a concrete model of ZFC, vs. a "small inductive set" inside ZFC without

specifying a model (...with what I have problems to grasp due to example I sketched in prev comment)