Let $M$ be a countable model of arithmetic (that satisfies PA). Can we have two numbers $c_1, c_2 \in M$ such that $c_1$ can not be defined in terms of $c_2$, and $c_2$ can not be defined in terms of $c_1$?
(When I say that $a$ can be defined in terms of $b$, I mean that we have a predicate in the language of arithmetic $\phi(x,y)$ such that only $a$ satisfies $\rho(z)=\phi(z,b)$.)
Start with $PA$, and add two symbols $c_1$, $c_2$. For each arithmetical predicate $\phi$, add the axiom $\phi(c_1,c_2) \implies (\exists c \neq c_1 \phi(c,c_2) \land \exists c \neq c_2 \phi(c_1,c))$. My question is equivalent then becomes equivalent to the question of whether this theory is consistient.
Interesting side note: I can show that the negation of continuum hypothesis implies this is true. Let $M$ be a model of PA equinumerous with real numbers. For each $c$ in $M$, there is a countable set $Def(c)$ of numbers definable in terms of $c$ (in the language of arithmetic). By the axiom of symmetry, there will be $c_1, c_2$ such that $c_1 \notin Def(c_2)$ and $c_2 \notin Def(c_1)$. Now take all the true statements of $M$ in the language of arithmetic plus symbols for $c_1$ and $c_2$ (we discard all the true statements involving the other nonstandard numbers). This will have a countable model $M'$, and since $c_1$ and $c_2$ cannot be defined in terms of each other in $M$, this will also be true in $M'$.
Yes. Your use of the "axiom of symmetry" is totally unnecessary: just take $M$ to be any model of cardinality greater than $\aleph_1$, and the same argument works with no additional assumptions. Explicitly, if $A\subset M$ is a set of cardinality $\aleph_1$, then there are at most $\aleph_1$ elements of $M$ that are definable from an element of $A$. So there is some $c_1 \in M$ which is not definable from any element of $A$. Since only countably many elements of $M$ are definable from $c_1$, some $c_2 \in A$ is not definable from $c_1$. So neither of $c_1$ and $c_2$ is definable from the other.
Alternatively, instead of using uncountable models, you can just use compactness. By compactness, it suffices to consider finitely many possible definitions at a time. The argument above can then be carried out in any infinite model, taking $A$ to be a finite set of cardinality greater than the number of definitions you are considering.