This is a followup to a previous question: Not Skolem's Paradox.
Assume we have a countable, non-standard model of Peano Arithmetic in ZFC.
Let $N^*$ be the universe of this model and let $p \in N^*$ be a non-standard natural number larger than any standard natural number. In ZFC we can define the set $X = \{x : x \in N^* \land x < p\}$. Let $Y = X \cup \{p\}$. $X$ and $Y$ are both countably infinite sets and we can easily define a bijection between $X$ and $Y$ in ZFC. For example, we can define the set of ordered pairs:
$F = \{(0,p), (1,0), (2,1), (3,2), ...\}$.
My question is why doesn't the bijection $F$ exist inside the model?
In my previous question there was some confusion about how I was defining sets inside the model. We can encode any "finite" set of natural numbers as a natural number using powers of 2. For example, we can encode the set $\{1,2,3\}$ as $2^1+2^2+2^3=14$. Similarly, we can encode a bijection as a natural number. First, we define a method to encode an ordered pair as a natural number. Encode $(a,a)$ as $2^a$. Encode $(a,b)$ as $2^{a+1} + 2^{b+1}$ if $a<b$. If $b<a$ encode $(a,b)$ as $2^{a+1} + 2^{b+1} + 1$. Now that we can encode ordered pairs, we can define a bijection between two sets of natural numbers using Godel's beta function.
My question becomes why doesn't some natural number in our model encode a function such that $F$ is an initial segment of this function?
Edit:
I want to thank Andres Caicedo for correcting my question. I do want to define my bijection as he suggests:
$F = \{(0,p)\} \cup \{(t+1,t) | t \in \aleph \} \cup \{ (s,s) | s \in X \backslash \aleph \}$
As he points out, I can't define $\aleph$, the set of standard natural numbers, inside the model. However, I can define $\aleph$ in my meta-theory. Can I come up a with beta function for $F$ inside ZFC? If so, does the encoding of this beta function exist in my model? If not, there is a natural number of the form $2^{a+1} + 2^{b+1} + 1$ that is missing from the model where $(a,b)$ is my beta function. If the encoding does exist in the model we have a definable violation of induction. Considering the alternatives, I am guessing there is some reason I can't define a beta function for $F$ in ZFC.
Before going any further, note that $F$, as written, is most likely not what you meant it to be. It appears as if $F$ is a bijection between the standard part $\mathbb N$ of $N^*$, and the set $\mathbb N\cup\{p\}$. Note that this is a bijection, and it is the initial segment of some bijection between $X$ and $Y$ (for example, the one in paragraph 3). This is not a problem. The issue is that the initial segment that codes $F$ is not definable in the model, it is not itself coded. The thing is, if $G$ is a function coded in $N^*$, with domain an initial segment of $N^*$, then for any initial segment $I$ that is definable in $N^*$, we have that in $N^*$ there is a code for $G\upharpoonright I$. But $I$ in this case is $\mathbb N$, and this is not definable in $N^*$. In fact, the only definable initial segments are those of the form $\{y\mid y<t\}$ for some $t$, and $\mathbb N$ definitely does not have this form. (This is proved by induction: "For any proper initial segment there is a least number not in it." The problem is that there is no least non-standard integer: IF $K$ is infinite, so is $K-1$.) The obstacle here is the restriction to definable initial segments, but this is unavoidable: If $G\upharpoonright I$ is coded in $N^*$, certainly $I$ is definable in $N^*$.
I imagine this $F$ is not what you intended. Rather, you probably meant something like $F=\{(0,p)\}\cup\{(t+1,t)\mid t<p\}$. But note that $(p,p-1)\in F$, so $F$ is a bijection alright, and certainly one coded inside $N^*$, but it is just a bijection from $Y$ to itself, which again is not what you intended.
Or maybe you meant $F=\{(0,p)\}\cup\{(t+1,t)\mid t\in\mathbb N\}\cup\{(s,s)\mid s\in X\setminus\mathbb N\}$. This is definitely a bijection between $X$ and $Y$, but it is not definable in $N^*$, it is not encoded in there. If it were, we could from it define $\mathbb N$, and obtain a definable violation of induction.
In fact, no matter how we try, any bijection between $X$ and $Y$ cannot be coded within the model. This is because $N^*$, being a model of $\mathsf{PA}$, proves the appropriate facts about coded finite sets, such as there not being a bijection from a finite set to a proper superset. (This is proved by induction, of course.)
(If you find these explanations not quite satisfactory, and if you indicate any issues you may have, I'll try to clarify/expand/add as appropriate.)
Let me address your edit. The function $F$ in paragraph 3 is definitely an object in $\mathsf{ZFC}$. It is countable, so it can be coded as a set of numbers. However, we cannot code it inside the model. As Andreas Blass remarks, each value $(a,F(a))$ is certainly codable, but of course this is not enough. To have a coding of $F$ within $N^*$, via Gödel's approach or otherwise, we would need definability of $F$. As explained above, this gives us definability of $\mathbb N$ inside $N^*$. But this is impossible. In a sense, this is related to your previous question: $N^*$ can refer (via codes) only to sets that are fairly explicitly presented, and most sets are not. Even if "from the outside" we have a good understanding of $F$, this is simply an external object to our model $N^*$, it is "invisible" to it, and it is not possible to change this, because the induction schema prevents the presence of "Dedekind infinite integers".