Corrections and Elaboration
I made a bunch of mistakes in the original question. I am preserving the original question, but adding additional explanation and corrections here.
The post below uses inner model, which has a meaning specific to set theory, incorrectly. When I wrote the post, I used "inner model" because I thought I needed to take special care.
ZFCP is supposed to be ZFC with a dedicated ordered pair construction $P$, which is a predicate symbol.
Ordered pairs are more typically described in terms of a function symbol, let's use $p$ as our ordered pair function symbol.
$p$ satisfies the following axioms.
$$ p(x, y) = p(z, w) \iff x = z \land y = w $$
Additionally, ordered pairs are not sets.
$$ \forall x \forall y \, (\lnot \exists z \mathop. z \in p(x, y)) $$
Our relation $P$ is defined as
$$ P(x, y, z) \;\; \text{if and only if} \;\; p(x, y) = z $$
The ordered pair is a construction that frequently comes up when talking about set theory, in particular when talking about how to build objects out of sets. There's also frequently some discussion about how elegant the Kuratowski pair is.
I can't remember where exactly I've heard people say that ZFC with a dedicated ordered pair construction (ZFCP) is consistent if ZFC is consistent, but I'm sure I've heard it before.
I think I have a way to construct a new model of ZFCP with an intepretation for an is-an-ordered-pair relation, but I'm not sure whether it works or not. (since ZFCP is not exactly the same thing as ZFC, I'm going to call it a model not an inner model. I don't know whether this is the right terminology or not.)
My question is twofold.
- Does the following construction work for producing a model of ZFCP? In particular, is the $g$ function below, which "canonicalizes" domain elements valid?
- Is there a simpler way to show that a model of ZFCP exists?
Suppose ZFC is consistent.
Let $\mathbb{N}$ refer to the integers greater than zero. Elements of $\mathbb{N}$ are thought of as sets in the traditional way, i.e. $1 = \{\{\}\}$. $\pi_n$ is the $n$th projection out of a tuple, defined below.
Let $f(x, y)$ be a Kuratowski pair of $x$ and $y$, i.e.
$$ f(x, y) = \{\{x\}, \{x, y\}\} $$
Let $\langle x_1, x_2, \cdots, x_n \rangle $ be a tuple, defined as follows.
$$ \langle x_1, x_2, \cdots, x_n \rangle = \{f(1, x_1)\} \cup \{f(2, x_2)\} \cup \cdots \cup \{f(n, x_n)\} $$
Additionally, if $W$ is an $n$-ary predicate symbol, let its interpretation have the form $\{ \langle c_1, c_2, \cdots, c_n \rangle \cdots \} $. This just means that $\langle\cdots\rangle$ is the kind of tuple we are using to give meaning to predicates.
ZFC has an inner model $(M, R)$ where $R$ is the interpretation of $\in$.
Let's suppose ZFCP has an additional predicate symbol $P$. $P(x, y, z)$ holds if and only if $z$ is the ordered pair whose first element is $x$ and whose second element is $y$.
I will now attempt to build a model of ZFCP out of the pieces of the inner model of ZFC.
On a high level, I will use $1$, $2$, and $3$ as type tags. I am stealing the idea of type tags from Lisp Machines. $1$ is the type tag for non-pairs and $2$ is the type tag for pairs. $3$ is the type tag for sets where the $v$ in $\langle 3, v \rangle$ is meant to be interpreted as an actual set, rather than an arbitrary element of $M$ ... because the names of the elements of the domain of our inner model of ZFC are arbitrary.
First, we seed our universe of our new model.
$$ M_1 = \{ \langle 1, x \rangle : x \in M \} $$
Next, we seed the value of the new $\in$
$$ R_1 = \{ \langle \langle \pi_1(v) \rangle, \langle \pi_2(v) \rangle \rangle : v \in R \} $$
Next, we seed the value of our new pairing predicate.
$$ P_1 = \{ \langle x, y, \langle 2, x, y \rangle \rangle : x \in M_1 \land y \in M_1 \} $$
Then, we say how to construct the next generation of $M$. I'm iterating over all pairs of elements in $P_n$ and $R_n$ instead of iterating over one then the other because I think it looks nice notationally.
$$ M_{n+1} = \bigcup \bigg\{ \{ \pi_1(u), \pi_2(u), \pi_1(v), \pi_2(v), \pi_3(v) \} : u \in P_n \land v \in R_n \} \bigg\} $$
When defining the next generation of $R$, we take the previous generation and add a new type tag $\langle 3, \cdots \rangle$ which represents a "verbatim set". This is different because in our original inner model, the actual sets for each element of the domain is arbitrary. There is no guarantee that our original $R$ respects the true $\in$ in any way, shape, or form. $\text{pow}$ denotes the powereset.
$$ R_{n+1} = R_{n} \cup \{ \langle x, \langle 3, y \rangle \rangle : x \in M_{n+1} \land y \in \text{pow}(M_{n+1}) \land x \in y \} $$
Next, we construct the next generation of $P$. The $P_{n}$ that is being unioned in is technically unnecessary, but including it drives the point home that we're growing our universe and all our predicates with each generation.
$$ P_{n+1} = P_{n} \cup \{ \langle x, y, \langle 2, x, y \rangle \rangle : x \in M_{n+1} \land y \in M_{n+1} \} $$
Now, let's union together everything.
$$ M' = \bigcup_{\alpha \in \mathbb{N}} M_\alpha $$ $$ R' = \bigcup_{\alpha \in \mathbb{N}} R_\alpha $$ $$ P' = \bigcup_{\alpha \in \mathbb{N}} P_\alpha $$
However, we're still not done because of some of the elements with tag $1$ are equivalent to elements with tag $3$.
Let the function $g$ send every set that hereditarily lacks the type tag $2$ to the equivalent set with type tag $1$ (and hence no interior type tags). This function $g$ is the sketchiest step and the one I am having the most trouble with.
Extend $g$ to apply recursively to all sets, regardless of what they are headed by.
Now, we define $M''$, $R''$, and $P''$ in the following way.
$$ M'' = \{ g(x) : x \in M' \} $$ $$ R'' = \{ \langle g(\pi_1(v)), g(\pi_2(v)) \rangle : v \in R' \} $$ $$ P'' = \{ \langle g(\pi_1(v)), g(\pi_2(v)), g(\pi_3(v)) \rangle : v \in P' \} $$
I claim that $(M'', R'', P'')$ is a model of ZFCP.
You are making this much much much more complicated than it needs to be.
First of all, a comment on terminology: I think you mean "model" here, not "inner model".
Ok, so we want to take a model of $\text{ZFC}$ and turn it into a model of $\text{ZFCP}$. You haven't actually specified what you mean by $\text{ZFCP}$, but from context I guess you mean the theory in the language $\{\in,P\}$ axiomatized by $\text{ZFC}\cup \{\forall x\forall y\exists^! z\, P(x,y,z)\}$, or something equivalent?
Note that there is a formula $\varphi(x,y,z)$ in the language of set theory which expresses "$z$ is the Kuratowski ordered pair $(x,y)$".
Ok, now suppose $(M,R)$ is a model of $\text{ZFC}$. We can expand $(M,R)$ to a structure in the language $\{\in,P\}$ by interpreting $P^M = \{(a,b,c)\in M^3\mid M\models \varphi(a,b,c)\}$. Since $\text{ZFC}$ proves $\forall x\forall y\exists^! z\, \varphi(x,y,z)$, we will have $(M,R,P^M)\models \text{ZFCP}$. That's all there is to it!
The point is that $\text{ZFC}$ proves that every pair of elements has a Kuratowski ordered pair, so this is true in any model $(M,R)$, and thus we are free to add new structure to $M$ identifying these ordered pairs. This is a special case of the very general notion of definitional expansion / extension by definitions.