Consider Leibniz's principle of the indiscernibility of identity, stated in (1) in second order logic:

$$(1) \hspace{0.3cm} \forall x \thinspace \forall y \thinspace [\hspace{0.2cm}x \hspace{0.2cm}= \hspace{0.2cm}y \hspace{0.2cm} \rightarrow \hspace{0.2cm} \forall P\hspace{0.2cm}(Px \hspace{0.2cm} \leftrightarrow \hspace{0.2cm} Py)]$$

Many axiomatisations of FOL (First Order Logic) seem to contain principles of substitution that amount to a schematic form of this principle in which $(1)$ below holds, for any variables $x$ and $y$ and any formula $\Phi \thinspace(x)$, if $\Phi\thinspace(y)$ is obtained by replacing any number of free occurrences of $x$ in $\Phi$ with $y$, such that these remain free occurrences of $y$:

$$(2) \hspace{0.3cm} x \hspace{0.2cm} = \hspace{0.2cm} y \hspace{0.3cm} \rightarrow \hspace{0.3cm}[\thinspace \Phi \thinspace(x) \hspace{0.2cm} \leftrightarrow \hspace{0.2cm} \Phi\thinspace(y) \thinspace ] \hspace{0.2cm}$$

Now consider the converse of (1) in second order logic (The identity of indiscernibles):

$$(1') \hspace{0.3cm} \forall x \thinspace \forall y \thinspace [ \thinspace \forall P \hspace{0.3cm}(Px \hspace{0.3cm} \leftrightarrow \hspace{0.3cm} Py) \hspace{0.3cm} \rightarrow \hspace{0.3cm} x \hspace{0.3cm}= \hspace{0.3cm}y \thinspace ]$$ Can FOL be axiomatised taking the converse of (2) as an axiom?

$$(2') \hspace{0.3cm}[\thinspace \Phi \thinspace(x) \hspace{0.2cm} \leftrightarrow \hspace{0.2cm} \Phi\thinspace(y) \thinspace ] \hspace{0.2cm} \rightarrow \hspace{0.3cm} x \hspace{0.2cm} = \hspace{0.2cm} y\hspace{0.2cm}$$

More generally, how is $(2')$, for an arbitrary predicate $\Phi$, derivable in FOL?

Noah Schweber has pointed out that $(2')$ is false in FOL. But how about $(2'')$:

$$(2'') \hspace{0.3cm}\forall x \thinspace \forall y \hspace{0.3cm} [\thinspace[\thinspace \Phi \thinspace(x) \hspace{0.2cm} \leftrightarrow \hspace{0.2cm} \Phi\thinspace(y) \thinspace ] \hspace{0.2cm} \rightarrow \hspace{0.3cm} x \hspace{0.2cm} = \hspace{0.2cm} y\hspace{0.2cm}]$$

How is $(2'')$ derivable for arbitrary $\Phi$ in FOL? I suppose it would again be falsified in the empty structures Noah mentioned?

If not, can FOL be axiomatised taking the (2'') as an axiom? More generally, what is the status of the identity of indiscernibles in FOL?


1 Answer 1


Actually, (2') is false in first-order logic. Consider, for example, a two-element structure $\{a, b\}$ in the empty language. Then $a$ and $b$ satisfy all the same sentences, but $a\not=b$.

(Note that if we allow parameters in $\Phi$, then identity of indiscernibles holds for a silly reason: $a$ satisfies "$x=a$," but any $b\not=a$ will not.)

And, in fact, the patterns of indiscernibility within a structure can be extremely complicated, and are important in model theory; see also this previous question.

  • $\begingroup$ Thank you :). I have edited my question, for a puzzle remains... :) $\endgroup$
    – user378426
    Oct 15, 2016 at 16:58
  • $\begingroup$ Outside of the empty language is $(2')$ true? $\endgroup$
    – user378426
    Oct 15, 2016 at 17:19
  • $\begingroup$ @Lukelindenbaum No, there are examples in any language - e.g. given a structure $\mathcal{M}$ in an arbitrary language, we can form the "disjoint union" $\mathcal{M}\sqcup \mathcal{M}$ consisting of two copies of $\mathcal{M}$ side-by-side (strictly speaking, this only works if the language consists only of relation and constant symbols; with function symbols it's a bit messier). Now every element of $\mathcal{M}$ corresponds to a pair of indiscernibles, one in each copy of $\mathcal{M}$. (cont'd) $\endgroup$ Oct 15, 2016 at 17:30
  • $\begingroup$ And (2'') fails for exactly the same reason. There really isn't any way around it: identity of indiscernibles fails in first-order logic. $\endgroup$ Oct 15, 2016 at 17:31
  • $\begingroup$ But it the identity of indiscernibles IS provable in SOL on the full semantics, correct? I'm confused by whether it is provable in the Henkin semantics because Thomas Klimpel's answer here seems to contradict Peter Smith's answer (Thomas Klimpel presents a proof of the principle, whereas Peter Smith says such a proof is not possible): math.stackexchange.com/questions/353353/… $\endgroup$
    – user378426
    Oct 15, 2016 at 20:13

You must log in to answer this question.