Identity, Indiscernibility and Individuation Criteria

This post is stimulated by some discussions with my research student Johannes Korbmacher about identity criteria (e.g., Horsten 2010, "Impredicative Identity Criteria"). I am interested here in how such identity criteria might be connected with other work on indiscernibility.

If $P$ is a unary predicate, then write,

$x{\sim }_{P}y$
for
$Px\leftrightarrow Py$

If $R$ is a binary predicate, then write,

$x{\sim }_{R,1}y$
for
$\mathrm{\forall }z(Rzx\leftrightarrow Rzy)$

and

$x{\sim }_{R,2}y$
for
$\mathrm{\forall }z(Rxz\leftrightarrow Ryz)$

Roughly, $x{\sim }_{P}y$ means that $x$ and $y$ are indiscernible by $P$; and $x{\sim }_{R,1}y$ means that $x$ and $y$ are indiscernible by $R$ on the first argument position; and $x{\sim }_{R,2}y$ means that $x$ and $y$ are indiscernible by $R$ on the second argument position.
It's easy to see how to generalize this to any primitive $k$-ary relation symbol.

The resulting formulas,

$x{\sim }_{R,i}y$,

are Hilbert-Bernays clauses.

The strongest (first-order) notion of indiscernibility expressible in a language $\mathcal{L}$ is given by the conjunction of all the Hilbert-Bernays clauses over the primitive predicate symbols. I.e., write:

$x{\sim }_{\mathcal{L}}y$
for
$\bigwedge \{x{\sim }_{R,i}y\mid R$ is an $n$-ary relation symbol in $\mathcal{L}$ and $1\le i\le n\}$.

Some accessible technical results about such formulas are given in

Ketland 2006, "Structuralism and The Identity of Indiscernibles";
Ketland 2011, "Identity and Indiscernibility".

My favourite results are:

1. If $=$ is definable in $\mathcal{M}$, then it is defined by $x{\sim }_{\mathcal{L}}y$.
2. If $\mathcal{M}\models a{\sim }_{\mathcal{L}}b$, then ${\pi }_{ab}\in Aut(\mathcal{M})$

where ${\pi }_{ab}:M\to M$ is the transposition that swaps $a,b\in M$.

In the case of set theory, we have the signature $\sigma =\{\in ,=\}$. Then the Axiom of Extensionality can be expressed as follows:

$x{\sim }_{\in ,1}y\to x=y$.

If we prefix this with a relativization to sets, then we have,

$Set(x)\wedge Set(y)\to (x{\sim }_{\in ,1}y\to x=y)$.

This kind of thing is sometimes called an individuation principle (I think this terminology is due to Quine). So, we sometimes say that sets are individuated by their members. But notice that we simply use a Hilbert-Bernays indiscernibility clause for the membership predicate.
Leibniz's Principle of Identity of Indiscernibles has the same form,

$Obj(x)\wedge Obj(y)\to (x{\sim }_{\iota ,2}y\to x=y)$.

where $Obj(x)$ means "$x$ is an object", and we introduce $x\iota X$ to mean "$x$ instantiates $X$" and $x{\sim }_{\iota ,2}y$ means

$\mathrm{\forall }X(x\iota X\leftrightarrow y\iota X)$.

Similarly, for extensional properties, we have,

$Ext(X)\wedge Ext(Y)\to (X{\sim }_{\iota ,1}Y\to X=Y)$.

(This generalizes to extensional relations too, when the instantiation relation is taken to be polyadic.)
So, going by analogy, one naturally expects all such individuation criteria to be formulated using Hilbert-Bernays indiscernibility clauses. So, an individuation criterion would then have the form,

$K(x)\wedge K(y)\to [\bigwedge \{x{\sim }_{R,i}y\mid (R,i)\in I_K\}\to x=y$].

where $I_K$ specifies a set of pairs of primitive symbols and argument positions.
So, for sets, $I_K$ is $\{(\in ,1)\}$.

Of course, there might be a kind $K$ of entities for which there is no such individuation criterion unless one assumes that the primitive identity predicate $x=y$ already is in $I_K$. In other words, $=$ is not definable in such structures from the other primitive notions/relations. It is easy to show that there are structures $\mathcal{M}$ in which $=$ is not definable. Examples are given in Ketland 2006 and Button 2006, "Realistic Structuralism's Identity Crisis: A Hybrid Solution". I call such structures "non-Quinian".

Because of such examples (and for other reasons), it is preferable to treat identity as a primitive notion.