Leibniz's law of the identity of indiscernibles can be stated in monadic second order logic: $$\forall x\forall y (x=y \leftarrow \forall P (Px \leftrightarrow Py))$$ This law is true for standard semantics. My first question is:
Is this law also true for Henkin semantics with comprehension axioms for first-order formulas?
Here I still assume equality to be part of the language, and the comprehension axioms to be $\forall P_1\ldots\forall P_m\forall x_1\ldots\forall x_n\exists P\forall x(Px\leftrightarrow\varphi(x,P_1,\ldots,P_m,x_1,\ldots,x_n))$ for each first-order formula $\varphi(x,P_1,\ldots,P_m,x_1,\ldots,x_n)$ with free variable $x$, free predicates $P_1,\ldots,P_m$ and free variables $x_1,\ldots,x_n$. A first-order formula is a formula that doesn't use quantification over predicates (or other higher order variables). Because the sentence $\forall x_1 \exists P \forall x(Px\leftrightarrow(x=x_1))$ is among these axioms, even a formal proof of Leibniz's law is probably doable.
The indiscernibility of identicals is trivially true: $$\forall x\forall y (x=y \rightarrow \forall P (Px \leftrightarrow Py))$$
This allows us to define an identity relation $E$ without explicit reference to equality: $$\forall x\forall y (Exy \leftrightarrow \forall P (Px \leftrightarrow Py))$$ If we now remove equality from the language, this relation $E$ will remain the identity in case of standard semantics, but will be reduced to an equivalence relation for Henkin semantics. For simplicity, let us also remove constants and functions from the language. Here's my next question:
Is the equivalence relation $E$ compatible with the rest of the language, i.e. $\forall x\forall y (Exy \rightarrow(\varphi(x,x) \rightarrow \varphi(x,y))$ for all formulas $\varphi(x,y)$ with free variables $x$ and $y$ (i.e. $\varphi$ can use all symbols from the language, and also quantify over monadic predicates)?
Here, the first order comprehension axioms shouldn't be allowed to use the symbol $E$, because the definition of $E$ uses quantification over monadic predicates.
And my last question:
Will $E$ partition any model (of a set of axioms) into equivalence classes without any discernible internal structure with respect to the relations available in the language and the monadic predicates available from the Henkin structure?