Internally Finite but Externally Infinite Set

I would like to understand the mechanism of following statement from this answer by Noah Schweber:

We could work in a non-$$\omega$$ model of ZFC. In such a model, there are sets the model thinks are finite, but which are actually infinite; so there's a distinction between "internally infinite" and "externally infinite."

How a set could be "internally", ie inside appropriate model be regarded as "finite", but be "externally" infinite? (btw, what means "externally"? An "overmodel" containing the submodel which regards this set as finite)

Eg, could somebody present an illuminative "toy example"? I know so far how construct models with "converse" phenomena, ie where eg the naturals $$\omega^M$$ of the fixed model $$M$$ (which tautologically trough the lens of this model are seen as countable) appear internally uncountable, see eg here for idea. Thank's to @Alex Kruckman for pointing out the correct phrasing of this phenomenon.
Here I'm also not 100 percently sure what is meant in by "externally" as contrast to internally (= inside fixed model) A guess: A kind of "distinguished overmodel" which contains all ordinals?

But the converse construction that some set is internally finite but externally infinite appears to me to be less plausible/ intuitive. Could somebody elaborate the phenomenon behind?

• A minor aside: "the naturals apear internally uncountable" is not a very accurate description of what's going on in the linked construction. There we have an object which externally is "related to" the naturals but internally isn't, so it's fairer to say "there is a set which appears uncountable but is secretly the natural numbers in disguise." Of course a model $M$ won't believe that (something it recognizes as) the naturals will be uncountable, by definition! Commented Jul 23 at 21:51
• "Note, that I know that how construct models ... where eg the naturals apear internally uncountable". I suspect you have "internally" and "externaly" flipped here. Given a model $M$, the naturals of $M$, denoted $\omega^M$, are always internally countable by definition. What we can do is find models in which $\omega^M$ is internally countable but externally uncountable. Commented Jul 23 at 21:51
• @NoahSchweber: What do you mean precisely by "object which externally is "related to" the naturals but internally isn't"? (is implicitly a kind of "overmodel/true universe in background" fixed where we can relate certain object - in our case an ordinal - with the naturals in "usual way", via an "classical" inclusion of ordinals (-is this inclusion what you mean by "related externally"), which in turn in a spefic model might not exist? Is this the point you intend to emphasise above? Commented Jul 23 at 22:53
• @NoahSchweber: Also, could the phrase that certain fixed model "recognizes an object as blabla" - in example above a model "recognizing some set as naturals" - be made mathematically presise? What does mean this "recognizing" formally? Commented Jul 23 at 23:03
• "Externally" refers to what's true, "internally" refers to what's true in the model. Commented Jul 24 at 0:48

Remember that "appear finite" just means "has an injection (in the model) into an element of the thing the model thinks is $$\omega$$." The point is that we can have a "nonstandard $$\omega$$," with elements which are - externally - infinite (but internally finite by virtue of literally being elements of the model's $$\omega$$). E.g. any model of ZFC+"ZFC is inconsistent" must be such a model, since it will need to have a "number" which codes a proof of a contradiction in ZFC and no such truly finite number exists (hopefully!).

I think this becomes much simpler if we shift from set theory to arithmetic. Consider a nonstandard model $$\mathcal{M}$$ of (say) first-order Peano arithmetic, $$\mathsf{PA}$$. We have the obvious initial segment embedding $$i:\mathbb{N}\rightarrow\mathcal{M}$$ whose image (by nonstandardness) is proper; any $$m\in\mathcal{M}\setminus ran(i)$$ is "externally infinite but internally finite." Set theory makes the picture messier by having lots of additional "stuff" going on, but it's ultimately the same.

• @RobArthan No, Alex was right - check the edit history. (Hence the ":P" in my previous comment.) Commented Jul 23 at 22:14
• How can the formulation that a model $M$ "thinks" that certain object inside is is $\omega^M$, ie the "naturals of $M$" be formally phrased? Commented Jul 23 at 23:33
• Moreover, what do you mean by "a number, which codes a proof of a contradiction in ZFC"? A naïve guess: Is here some kind of philosophy involved which allows to express proof as "honest numbers"? Commented Jul 23 at 23:38
• You seem to have finally hit upon "truly finite" numbers and you may want to communicate this to Hamkins' oracle. Commented Jul 29 at 6:57

By Gödel's incompleteness theorem, there is a sentence $$S$$ of ZFC that encodes the assertion that ZFC is inconsistent and such that the theory $$ZFC \cup \{S\}$$ has a model $$\cal M$$. $$\cal M$$ must include a set $$P$$ that purports to be a proof of $$S$$ and so, as far as $$\cal M$$ is concerned, $$P$$ is a hereditarily finite set (because proofs are hereditarily finite structures), but $$P$$ can't actually be hereditarily finite because otherwise it would be a proof in ZFC of the inconsistency of ZFC. So tucked inside $$P$$, there is a set that is (externally) infinite, but that $$\cal M$$ (internally) thinks is finite.

• Could you clarify the part on " ...so far $\mathcal M$ is concerned, $P$ is hereditary finite set, but actually it cannot be (h.f. set). Could you elaborate a bit this beeing h.f. set concerning/ insidemodel $\mathcal M$ vs beeing actually not ("externally"?) Commented Jul 23 at 23:53
• As a non-standard model, $\cal M$ contains objects that purport to be positive integers but are greater than any of $1, 2, \ldots$. So $\cal M$ contains sets that it thinks are finite because they are in 1-1 correspondence with one of these non-standard positive integers, but in our metalanguage we know that such sets are infinite. Commented Jul 24 at 20:37
• what I not understand, how can a 'bare' set $P$ in a fixed model of ZFC + $\{S \}$ be a "proof of $S$? A "proof" is a finite sequence of implications which are "legal" wrt the deduction system of the theory. A proposition in language of a theory is true in a model if it evaluates to "truth value" under $M$. But what do you mean by "that a set can be a proof"? Or did I misunderstood what you mean there? So I not understand this "set as proof" interpretation you seemingly invoke in your answer Commented Jul 25 at 15:30
• You can write down in the language of ZFC a formula $\phi(p, s)$ which in the standard model asserts that $p$ is a number representing a proof of a statement represented by the number $s$. (If this is unfamilar to you see en.wikipedia.org/wiki/Gödel_numbering.) In a model of ZFC together with the assertion $S$ that ZFC is inconsistent, there $\phi(p, s)$ holds for some numbers $p$ and $s$ such that $s$ represents $S$. The only way this can happen is for $p$ to a non-standard number. Commented Jul 26 at 21:47

Here's a "toy model" with the feature you want, but phrased in the language of topoi. There are subtleties here about converting between these "sheaf models" and honest models of ZFC, but I'm going to ignore them to keep this answer simple$${}^1$$.

There's a topos called $$\mathcal{M} = \mathsf{Set}^{\omega}$$, and a "set" in this topos is actually the product of $$\omega$$-many "real world" sets (here I'm fixing some model of ZFC to consider "the real world"). Now one can compute $$\mathbb{N}^\mathcal{M}$$ is a product of $$\omega$$-many copies of $$\mathbb{N}$$, and $$n^\mathcal{M} = \{ x \in \mathbb{N} \mid x < n \}^\mathcal{M}$$ is the product of $$\omega$$-many copies of the real-world-set $$n$$. In particular, we living outside of $$\mathcal{M}$$ can see that $$n^\mathcal{M}$$ is uncountable, but it "looks finite" to people living inside $$\mathcal{M}$$. For any reasonable $$\mathtt{isFinite}$$ predicate you write, we'll have $$\mathcal{M} \vDash \mathtt{isFinite}(n)$$.

1: note that $$\mathcal{M}$$ is actually a boolean topos, so we don't need to worry about the usual subtleties here. You can think of $$\mathcal{M}$$ as a boolean-valued model taking truth values in the algebra of subsets of $$\omega$$. There are standard techniques for building an honest-to-goodness two-valued model from one of these, and truth in the two-valued model is closely related to truth in the boolean-valued model.

I hope this helps ^_^

• Just to clarify: The formulation that this $n^M$ "looks finite" to people inside $M$, what does this formally? A guess, ok you could say, this is equivalent to that there is an injection inside $M$ into $\Bbb N^M$ - the "naturals of $M$ - so it we regard latter as naturalls inside $M$ then it's plausible that its any broper subset "looks like" finite set. But then the question is why inside your model the $\omega$-product of $\Bbb N$ is exactly the object which should be regard as "the naturals" internal to $M$. This appears to be "plausible", but how to verify it formally? Commented Jul 24 at 0:04
• You can pick your favorite axiomatization of $\mathbb{N}$ (for instance, you might ask for a smallest model of PA, an initial algebra for $0$ and $\text{Succ}$, a smallest infinite set, etc). Whatever you choose, you can syntactically write down some theory $T$, and ask if $\mathcal{M} \vDash \ulcorner \mathbb{N} \vDash T \urcorner$. Similarly, you can write down any definition of finite you want (for instance, it injects into a member of $\mathbb{N}$, every injection to itself is also a surjection, etc) and we'll have $\mathcal{M}$ will think that definition is true of $n$. Commented Jul 24 at 2:23
• As for how to "verify it formally", there's a completely mechanical translation you can do in order to turn questions about $\mathcal{M}$ into (more delicate) questions about "the real world". This is the business of forcing, and you can read more about how it works in the topos setting in, for instance, chapter VI of Mac Lane and Moerdijk's Sheaves in Geometry and Logic Commented Jul 24 at 2:25
• This example is interesting, but is a rather different phenomenon than the “non-standard”/“non-ω” models in the quotation OP is asking about. “Non-standard” (whether for models of first-order set theory, or arithmetic, or elementary topoi) is typically understood to mean that the numerals don’t exhaust the model’s naturals — categorically, that there’s some $1 \to N$ that’s larger than every numeral, or something similar to this. In this example (and any Grothendieck topos), $N$ is standard; what you’re observing here is that the global sections functor doesn’t preserve finiteness. Commented Jul 24 at 12:44
• @PeterLeFanuLumsdaine -- I agree with what you're saying, but I wasn't trying to provide an example of a model with nonstandard naturals. I was answering this question "How a set could be "internally", ie inside appropriate model be regarded as "finite", but be "externally" infinite?", particularly the request for a "toy example" of this situation. I think it's easier to get your hands on a sheaf model like this and experiment than it is to do the same with a nonstandard model of PA. Plus, when I got here, Noah had already given a characteristically excellent answer through that lens! Commented Jul 24 at 17:16