Is there a Leibnizian model with no definable elements, in a finite language? A first-order structure $M$ is Leibnizian, if any two distinct
elements $a,b\in M$ satisfy different $1$-types; that is, if there
is some formula $\varphi$ such that $M\models\varphi(a)$ and
$M\models\neg\varphi(b)$. Thus, a Leibnizian model is one in which
you can distinguish any two elements by properties expressible in
the language, or to put it differently, a Leibnizian model is one
in which indiscernibles are identical.
In contrast, a structure $M$ is pointwise definable, if every
individual element $a\in M$ is definable in $M$, so that there is
some formula $\varphi(x)$ which is satisfied in $M$ only at $x=a$.
Every pointwise definable model is Leibnizian, of course, since
elements can be distinguished by their defining characteristics.
But in general, the concepts are distinct:


*

*A Leibnizian model with non-definable elements (infinite language).
In the language with infinitely many constant symbols
$c_0,c_1,\ldots$, consider a model $M$ interpreting them all
differently and having exactly one additional point, which is not
the interpretation of any constant. This model is Leibnizian,
since for any two points, one of them is one of the constants and
hence definable. But the single extra point is not definable in
$M$, because any formula $\varphi$ uses only finitely many of the
constant symbols, and hence cannot define that point, because in
the reduct of the model to the language of $\varphi$, there are
automorphisms that permute all the other points not named by a
constant in $\varphi$. Note that most of the elements of this
model are definable. (Alternatively, one could take an elementary
extension of the model and note that all the unnamed points will
be automorphic.)

*A Leibnizian model with no definable elements (infinite language). Consider the
model $\langle
2^\omega,U_s\rangle_{s\in 2^{<\omega}}$, where the domain is
Cantor space $2^\omega$, the set of all infinite binary sequences, and the
predicate $U_s(z)$ holds exactly when $z$ begins with the finite
string $s$. So this is Cantor space with predicates for the basic
open sets. The model is Leibnizian, since any two distinct $y,z$
in Cantor space must disagree on some $U_s$. But the model has no
definable elements at all, because any formula $\varphi(x)$ uses
only finitely many predicates $U_s$, and the reduction of the
model to that language has numerous automorphisms with no fixed
points: one can flip bits on any coordinate beyond the length of
any $s$ that appears in $\varphi$.

*A Leibnizian model with non-definable elements (finite
language). Consider the language with just one unary function
symbol $S$, and form the CandyLand model (named by Arden Koehler), which has 
one lollipop of every finite size, plus one infinite lollipop stick. More precisely, the model has 
infinitely
many base point elements $x_1,x_2,x_3,\ldots$ plus one more
$x_\infty$, such that none of them is in the range of $S$, and
furthermore, the function $S$ applied to base point $x_n$ iterates
for exactly $n$ steps before finding a fixed point, and where
$S^k(x_\infty)$ never repeats. $$x_1\neq
S(x_1)=S^2(x_1),\qquad x_n\neq S^k(x_n)\neq
S^n(x_n)=S^{n+1}(x_n)\quad(k<n)$$ So $x_n$ is the base of a size $n$ lollipop. Note that every element
on a finite lollipop is definable by the number of times that $S$
may be applied in reverse and the number of forward iterates
necessary to reach the fixed point. So those points can be
distinguished from any other in the model; and any two distinct
points on the infinite lollipop can be distinguished by their
height, the number of times $S$ can be reversed from them. So the
model is Leibnizian. But meanwhile, none of the elements on the
infinite lollipop is definable. To see this, use a
compactness/upward Löwenheim-Skolem argument to find an
elementary extension of $M$ that has at least one additional
infinite lollipop with a base point, and then note that the two
infinite lollipops are automorphic, and so contain no definable
elements. (Alternatively, one can show that the structure admits
elimination of quantifiers down to the language of $S$ together
with the predicates $H_n(x)$ that assert that $x$ has height $n$,
meaning that $S$ can be inverted exactly $n$ times but not more
from $x$, but no quantifier-free assertion in this language can
define the base point of the infinite lollipop.)
My question is whether we can have it all:
Question. Is there a first-order structure $M$ in a finite
language, such that $M$ is Leibnizian, but has no definable
elements?
Having an elementary example would help to clarify a
certain issue on which Arden Koehler, a graduate student in my seminar this semester, is
writing.
 A: I think a variant of your second example works. Let $S$ (= unary function) be the (left) shift, and define $P$ (= unary relation) by declaring $Px$ to be true if $x_0=0$.
Then $\varphi(x) = PS^n x$ for suitable $n$ will distinguish any two points, but we can't define individual sequences since a first order formula will only talk about finitely many of their elements.
Update: If we want to include equality in our language, I propose to take a single dense (in $\{ 0, 1\}^{\mathbb Z}$) orbit of two-sided sequences as our universe. Then the original argument for non-definability by elimination of quantifiers, as suggested in the comments below, still goes through. The argument is very easy and straightforward in principle, but quite tedious (for me) to write down, so let me try to just illustrate the crucial point somewhat informally. Let me also introduce the unary function symbol $T$, interpreted as right shift (this isn't really needed, but if I don't have $T$ available, I will use a quantifier to express $T$ in terms of $S$, so I am not literally eliminating all quantifiers).
Since I can bring a quantifier free $\varphi$ to DNF, the key step is to look at
$$
\exists y \left(\varphi_1(\overline{x},y)\land \ldots\land \varphi_n(\overline{x},y)\right) ,
$$
where the $\varphi_j$ are literals (atomic or negated atomic).
Let me just illustrate with an example:
$$
\exists z \left( x_0=0\land y_3=0 \land z_0=1 \land Sz=x\land z=S^2y\land S^2z\not= y\right)
$$
Notice that an equality determines one variable in terms of the other since I'm on a single orbit. Start out by using all equalities involving $z$ to express $z$ in terms of the other variables. This might already show that the formula is unsatisfiable. If not, scan for contradictions between the equalities and inequalities. If nothing comes up, the inequalities involving $z$ can be dropped because they can then always be satisfied by changing those components the rest of the formula doesn't talk about. Now everything that is asked of $z$ can be said in terms of $x,y$, and the quantifier has been eliminated. In my example, this procedure gives
$$
x_0=0\land y_3=0\land x_{-1}=1\land y_2=1 \land x=S^3 y
$$
(which I could of course further simplify by dropping the second and fourth conjuncts, but this isn't needed for the general argument).
Update 2: James's example (Joel's version) and mine (the upgraded version) are actually closely related. Joel's structure is $\mathcal J=(\mathbb Z, <, A)$, and mine is $\mathcal C=(\mathbb Z, S, P)$, after identifying $S^na$ with $n$. The following holds: if an element of $\mathcal C$ is definable, then $\mathcal J$, with $An\iff a_n=0$, also has a definable element.
To show this, suppose that $\varphi(x)$ defines $n$ in $\mathcal C$. I can now simply translate what $\varphi$ says into the language of $\mathcal J$, as follows: replace every occurrence of $S^n y$ in $\varphi$ by $\exists z \textrm{''$z$ is the $n$th successor of y''}$, and change $y$ to $z$ in this subformula of $\varphi$. Similarly, replace $PS^n y$ by $AS^n y$ (and further translate $S^ny$ as just described). Then the new formula $\widetilde{\varphi}(x)$ would define the same point $n$ in $\mathcal J$.
A: $\newcommand\Z{\mathbb{Z}}\newcommand\P{\mathbb{P}}$Here is a simple account of a large class of examples.
Theorem. With probability one, the structure
$\langle\Z,<,A\rangle$ is Leibnizian and has no definable
elements, where $<$ is the usual order on the integers and
$A\subset\Z$ is a unary predicate chosen randomly with respect to
the coin-flipping probability measure.
Proof. Almost surely, a random predicate $A\subset\Z$ is not
periodic (since it gets infinitely many independent chances to
violate the pattern of any given period), and for a non-periodic
$A$, the structure $\langle\Z,<,A\rangle$ is Leibnizian, because
with any $n\in\Z$ as a parameter, we may define all the other
$m\in\Z$ as a certain number of steps above or below $n$, and so
since by non-periodicity the pattern of $A$ above and below $n$
will be different than the corresponding pattern of $A$ above and
below $m$, and this will be an expressible property distinguishing
$n$ and $m$. So with probability one, the structure $\Z_A$ is
Leibnizian.
Similarly, almost surely $\langle\Z,<,A\rangle$ has
no definable elements. The basic idea (noted by Emil in the comments) is that if
$\varphi$ defines $n$ with positive probability $\epsilon>0$, then
since the measure is translation invariant, it follows that
$\varphi$ defines any given $m$ with the same probability
$\epsilon$. By considering more than $1/\epsilon$ many points, we
would have a positive probability that two different points are
both defined by the same formula, which is a contradiction.
(Note that for any formula $\varphi$ in the language and any
integers $\vec n$, the set of predicates $A\subset\Z$ for which
$\langle\Z,<,A\rangle\models\varphi(\vec n)$ is indeed a
measurable set in the probability space, since this is true in the
case of an atomic formulas, and the quantifiers of $\varphi$
amount to countable unions and intersections. Thus, the question
of whether a given formula $\varphi$ defines $n$ does have some
probability.) QED
My earlier post showed that if $A\subset\Z$ is arithmetically generic,
then $\langle\Z,<,A\rangle$ is Leibnizian and has no definable
elements. The reason was that (i) it is Leibnizian, because $A$ is
not periodic; and (ii) if $\varphi$ defined $n$, then some finite
condition $A\cap[-m,m]$ would force this situation; but since that
finite pattern would also arise elsewhere in $A$, we would have a
translation $\pi(A)$ also extending that condition, and so we
would have $\varphi$ defining $\pi^{-1}(n)$ as well, a
contradiction.
MathOverflow collaboration is great,
because the original randomness idea appeared in James's answer,
which I then verified with the forcing argument, and then Emil saw
how to do it easily with an elementary probability argument. And Christian is proposing another argument with this structure that may simplify things further.
A: Just an idea:
Consider the language with two suggestively-named sorts, $\mathbb{Z}$ and $\mathcal{P}(\mathbb{Z})$, a binary relation symbol $\leq$ (of type $\mathbb{Z} \times \mathbb{Z}$), and two binary relation symbols $\in^*$ and $R$ of type $\mathbb{Z}\times\mathcal{P}(\mathbb{Z})$
We construct a model as follows. Let f be a "random" function from the power set of the natural numbers to the natural numbers. We populate the sort $\mathbb{Z}$ with the integers, interpreting $\leq$ as their usual order. We populate the sort $\mathcal{P}(\mathbb{Z})$ with a countable collection of ``random" subsets of the integers (e.g., chosen by coin flips).  We then interpret R as $\{(f(X),X) | X \in \mathcal{P}(\mathbb{Z})\}$, and $\in^*$ as $\{(n-f(X),X) | n \in X\}$. Basically, $\in^*$ is the standard element-of relation after a random shift of X.
The reason this should be Leibnizian is as follows:


*

*If two elements n,m of the sort $\mathbb{Z}$ are not equal, then ``with probability 1" there is an element X of the sort $\mathcal{P}(\mathbb{Z})$ such that $n \in^* X$ but $m \not\in^* X$

*With probability 1, no two elements X,Y of the sort $\mathcal{P}(\mathbb{Z})$ are shifts of each other, so they can be distinguished by some formula.


It's also clear no elements should be definable (unless we are extremely unlucky).

EDIT: As JDH points out, the first bullet was wrong!
Here is a (slightly more complicated) example that works (I think):
Consider the language with two sorts, $\mathbb{Z}_1$ and $\mathbb{Z}_2$, binary relation symbols $\leq_i$ (of type $\mathbb{Z}_i \times \mathbb{Z}_i$) (i = 1,2), and two binary relation symbols $=^*$ and $R$ of type $\mathbb{Z}_1\times \mathbb{Z}_2$
We construct a model as follows. Let f be a "random" bijection from the the integers to the integers. We populate the sorts $\mathbb{Z}_i$ with the integers, interpreting $\leq_i$ as their usual order. We then interpret R as $\{(f(n),n) | n \in \mathbb{Z}\}$, and $=^*$ as $\{(n-f(n),n) | n \in \mathbb{Z}\}$. Basically, $=^*$ is the standard relation of equality on the integers, after a random shift of the left entry.
The reason this should be Leibnizian is as follows:


*

*If two elements n,m of the sort $\mathbb{Z}_2$ are not equal, consider for large k the order type of 2k+1-tuple (f(n-k),f(n-k-1),...,f(n),....,f(n+k)). This has low probability of being equal to the order type of the 2k+1 tuple (f(m-k),f(m-k-1),...,f(m),....,f(m+k)) Now take k to $\infty$

*Apply a similar argument to $n \neq m$ of the sort $\mathbb{Z}_1$ by comparing the order type of the 2k+1 tuples (f^{-1}(n-k),....,f^{-1}(n+k)) and (f^{-1}(m-k),....,f^{-1}(m+k))
It's also plausible, at least, that no elements should be definable (unless we are extremely unlucky). The idea is that, if we restrict ourselves to $\leq_1$ and $\leq_2$, we just get two disjoint copies of the integers as an ordered set (so, no elements are definable using these alone). We also expect a random bijection from the integers to the integers to repeat any finite pattern of behavior infinitely often. (I admit this is more a heuristic argument).
A: Here is a different example.
For any irrational $a$, put $\mathcal M_a=\langle\mathbb Q,<,M,I_a\rangle$, where
\begin{align*}
M(x,y,z)&\iff y=\frac{x+z}2,\\
I_a(x)&\iff a<x<a+1.
\end{align*}
In $\mathcal M_a$, we can define the interval $(a,a+1/2)$ by the formula
$$I_a(x)\land\forall u,v\,\bigl(I_a(u)\land u<x\land M(u,x,v)\to I_a(v)\bigr).$$
By iterating this process, we can define the intervals $(a,a+2^{-k})$ for each $k\in\omega$, and then we can flip them around using $M$ to define each interval $\bigl(a+n2^{-k},a+(n+1)2^{-k}\bigr)$ with $n\in\mathbb Z$. Thus, 

Proposition: $\mathcal M_a$ is Leibnizian.

In order to rule out definable elements, we will need

Claim: For all irrational $a,b$, the structures $\mathcal M_a$ and $\mathcal M_b$ are elementarily equivalent.


Corollary: $\mathcal M_a$ has no definable elements.

Proof: Assume for contradiction that $u$ is definable in $\mathcal M_a$ by a formula $\phi(x)$. Then in $\mathcal M_{a'}$, $\phi$ defines an element $u'$. Since we have seen above that for any $k,n$, there is a formula that defines $\bigl(a+n2^{-k},a+(n+1)2^{-k}\bigr)$ in $\mathcal M_a$, and $\bigl(a'+n2^{-k},a'+(n+1)2^{-k}\bigr)$ in $\mathcal M_{a'}$, we must have $u'-u=a'-a$. However, this is impossible if we choose $a'$ so that $a'-a$ is irrational. QED
It remains to prove the claim. Observe:


*

*$\mathcal M_a$ is isomorphic to $\mathcal M_b$ via a shift if $b-a$ is rational.

*$\mathcal M_a$ is definable in the structure $\langle\mathbb Q+a\mathbb Q,<,+,\mathbb Q,1,a\rangle$.
The effect of 1 on 2 is that we can choose the zero element of the group to be arbitrarily close to $a$, thus by compactness, we can find a structure $\langle G,+,<,H,1,a\rangle$ such that
(a) $\langle G,+,<\rangle$ is a totally ordered divisible abelian group $G$, and $H$ is its proper divisible dense subgroup;
(b) $1\in H$, $a\in G\smallsetminus H$, $0<a<1$, and $a$ is infinitesimally small with respect to $1$;
(c) $\langle H,<,M,(a,a+1)\cap H\rangle$ is an elementary extension of $\mathcal M_a$.
It is well known that the theory described in (a) is complete and has quantifier elimination, hence also (a)+(b) gives a complete theory. But then (c) implies that the theory of $\mathcal M_a$ is independent of $a$.
