I have a couple of questions about the notion of "external" vs "internal" in context of models of ZFC.
Following "generic" statement which says when one says Given a model $M$, then it's possible that it has "internal naturals", denoted by $\omega^M$, which are "countable by definition". But it's possible to construct a model such that these $\omega^M$
is "internally" countable (…so far I understand that's a tautology; as far as $M$ recognizes $\omega^M$ as "it's natural", these are by definition internally countable), but (surprisingly) "externally" uncountable.
Questions:
(1) Can it be formalized what it means that a model $M$ "recognizes" a set – suggestively written $\omega^M$ – as "its internal integers"? How to decide under which conditions a set living in $M$ has this property? Can it be made precise?
(2) Concerning the "internal" vs "external" issues. Now we turn from "internal" to "external": What does it mean that to say that it's possible to find a model $M$ which has/"recognizes" a set $\omega^M$ "internally" as it's integers, but which "externally" are uncountable.
Pricisely, what means here "externally" or "in real world" uncountable?
This suggests that there exist a kind of "distinguished overmodel" (…not sure if it's correct to use term "universe" synonymously is strictly correct) in background with the "universal" property that the properties the objects living there are have are regarded as to be "absolutely true" (in contrast to properties of objects inside any other model are only "internally true").
Noah Schweber described this issue with "backgound model" where as statements can be regarded as "externally true" here as follows:
for simplicity, I'm adopting a Platonist stance here and assuming there is a "true" universe of sets in the background. (Of course we can phrase everything in terms of ZFC-deductions, so the Platonism is unnecessary, but it makes things much easier to think about at least at first.)
So as far understand Noah correctly, this Platonic view would resolve the "external" vs "internal" issue as follows:
Say again a set $\omega^M$ "internally" in model $M$ is countable, but which "externally" are uncountable should mean just that the interpretation of this set inside this "universal model" (=universe of sets) is recognized as in contrast to be uncountable. That's what should be mean that $\omega^M$ "externally" uncountable.
Firstly, is my interpretation of Noah's comment correct? If yes, this would suggest, that there is a kind hierarchy between models, where the properties of objects inside some arbitrary model $M$ are only "internally" true, ie only wrt/"inside" $M$, but in contrast the properties of objects inside this "distinguished" universe of sets in the background – which at all i I'm not confusing something also a model – are regarded as "true" in "absolute sense", orsynonymously "externally true". Does it make sense? Is this a kind of higher-order "unique" model?
If yes, this would fully answer my question (2), but this comment has a subtlety so far I see. Noah also states that in fact it is not neccessary to impose this "unverse of sets" as kind of "universal model in background", but one "can phrase everything in terms of ZFC-deductions".
What does the last phrase mean in detail? Why it is seemingly equivalent to inpose such universal "overmodel" in background where all "internally true" statements are actually "absolutely true", to that the concerned statements are "ZFC deducible", so "model independent",so far I understand. This leads me to
(3) Can the equivalence of these two viewpoints be eloborated?
An attempt to understand this leads me to some nonsensish conclusion: my interpreting of that a statement is "ZFC deducible" is just that this statement phrased in language of ZFC can be deduced by a finite sequence of rules of internal deduction system (sequent, modus ponens). But this rases following more general problem:
Say $S,S′$ are two statements/ propositions expressed in language of a theory $T$ and $M$ a model of $T$.
One says $S$ is true in $M$ ("internally) – notion $M \models S$ – what means just that $S$ (as proposition)
is mapped to "true" wrt evaluation of functions, relations of $T$ in $M$ (note by definition if $M$ is model of $T$ means that all axioms of $T$ are mapped to "true", and so all derivable staements to)
But note that this not means that $S$ is provable in $T$, just it's true in this specific model $M$.
But in contrast if $S′$ can be proved from axioms of $T$, then $S′$ is true in every model of $T$
, right?
Applied to above this would cause following paradoxical situation: Assume as before $M$ is a ZFC model where "internally" $\omega$ is countable – so $M\models \text{"}\omega^M\text{ is countable"}$– but "externally" externally uncountable.
If I understand the concept of "external" correctly, this would mean that the statement "$\omega^M$ is uncountable" can be dediced from ZFC axioms. But in turn by reasonings above this would imply (as for every model) also $M\models \text{"}\omega^M\text{ is uncountable"}$.
Isn't this strange, or do I missing something in my reasings?
user267839
Commented19 mins ago Delete
imply M⊨"ωM is countable"
( by choice of model) but also automatically M⊨"ωM is uncountable"
for even every model as well, due to what I wrote in prev comment, or not? Does it make sense? –
Best Answer
This is one of the rare cases where I disagree with Noah Schweber - in my experience, taking a Platonist stance and assuming there is a "true" universe of sets in the background makes things way harder to think about, especially for students, and doubly so for students who have to study set theory before taking rigorous courses in proof theory and in model theory.
a.) Yes, it can be formalized what it means for a model $M$ to recognize a set as its set of integers. We say that a set $x$ is the set of natural numbers precisely if it is the intersection of all sets containing $\emptyset$ and closed under the successor operation $n \mapsto n \cup \{n\}$. We can state this definition as a first-order formula $\varphi(x)$ with one free variable $x$ in the language of set theory.
Since $\exists! x. \varphi(x)$ is derivable from the $ZFC$ axioms of set theory, each model $M$ of set theory has a unique element $\omega_M \in M$ that satisfies the interpretation of $\varphi$ in $M$. This particular $\omega_M$ is the element that $M$ regards as the set of natural numbers.
b.) The object theory is just the theory you want to study. The metatheory is just the theory you work in while you study the object theory.
When you investigate $ZFC$ set theory, your object theory is $ZFC$. Your metatheory can be anything you choose, even ZFC itself. Potentially, you could choose a metatheory that differs greatly from $ZFC$, such as a homotopy type theory. But for simplicity, let's assume that we do work inside $ZFC$ itself as our metatheory.
Then our metatheory proves the existence of a unique set $\omega$ that is the intersection of all sets containing $\emptyset$ and closed under the successor operation $n \mapsto n \cup \{n\}$, i.e. the set of natural numbers.
Our metatheory also proves that if $ZFC$ has any model at all, then it has a specific model $M$, which includes an uncountable set $\omega_M \in M$ that $M$ considers its set of natural numbers. The metatheory can also establish that $\omega_M$ differs from $\omega$: for instance, $\omega_M$ is uncountable, while $\omega$ is countable.
Given a formula $\Psi$ in the language of $ZFC$ with parameters from some model $M$, you can claim that "$\Psi$ is true externally" when you proved $\Psi$ in the metatheory; you can say that "$\Psi$ is true internally to $M$" when you proved $M \models \Psi$ in the metatheory. This does not require assuming any kind of distinguished background model: everything we do boils down to a bunch of $ZFC$ proofs in the end.
The set of natural numbers is just the set that our metatheory says has the defining property $\varphi$ of the set of natural numbers, and our metatheory knows that this does not coincide with the set $\omega_M \in M$ that $M$ believes to have this property. In other words, you can prove $M \models \varphi(\omega_M)$ in the metatheory, but you cannot prove $\varphi(\omega_M)$ in the metatheory.
c.) Alternatively, we can work in a metatheory stronger than ZFC. For instance, we could use the metatheory $ZFC^+$ whose language is the usual language $(\in)$ of $ZFC$ set theory extended with an additional constant symbol $M$, and whose axioms are the axioms of ZFC extended with the additional axiom $``M\text{ is a model of }ZFC"$.
Proving "there is a weird model of $ZFC$ such that blah" in the extended theory $ZFC^+$ is exactly the same process as proving the implication "if there is a model of $ZFC$ then there is a weird model of $ZFC$ such that blah" in $ZFC$ itself: a proof translation can eliminate the additional axiom by weakening the conclusion into a conditional implication. One can work as if one had access to some distinguished model of ZFC, then convert everything into ZFC deductions in the end. These viewpoints are in this sense equivalent.
However, set theorists usually do not do this: instead of working in something like $ZFC^+$, they prefer to work in more powerful metatheories that give access to technically nice models of ZFC, e.g. transitive models. But this is somewhat tangential to your question.