Monadic second order logic without constants, functions and equality

Question

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?

Answer 1

Is this law also true for Henkin semantics with first order comprehension axioms?

Let's try to prove that it is true. The idea is that $\forall x_1 \exists P \forall x(Px\leftrightarrow(x=x_1))$ should entail the conclusion $\forall x\forall y (x=y \leftarrow \forall P (Px \leftrightarrow Py))$. Here is the sketch for the formal derivation:

\begin{eqnarray} \cup_\varphi\{\forall x_1\exists P\forall x(Px\leftrightarrow\varphi(x,x_1)) \}& \vdash & \forall x_1 \exists P \forall x(Px\leftrightarrow(x=x_1)) \\ \forall x_1 \exists P \forall x(Px\leftrightarrow(x=x_1)) & \vdash & \forall y \exists Q \forall z(Qz\leftrightarrow(z=y)) \\ \forall y \exists Q \forall z(Qz\leftrightarrow(z=y)) & \vdash & \forall x\forall y(\forall P(Px\leftrightarrow Py)\rightarrow(x=y\leftrightarrow y=y)) \\ \forall x\forall y(\forall P(Px\leftrightarrow Py)\rightarrow(x=y\leftrightarrow y=y)) & \vdash & \forall x\forall y(\forall P(Px\leftrightarrow Py)\rightarrow x=y) \end{eqnarray}

---

The next question asked about the situation when equality is removed from the language, in the context of monadic second order logic:

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)?

There is the implicit question whether the given axiom scheme models compatibilty, and the explicit question whether $E$ is actually compatible. Ignoring the implicit question, it will be compatible, because the definition of $E$ ensures compatibility with second order monadic predicates, and the comprehension axioms for first-order formulas will imply compatibility with the first order predicates, similar to how "compatibility with equality" was derived above.

---

The last question seems to be just a more hand waving version of the previous 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?

The answer is yes, as far as this is just a rewording of the previous question. However, in a certain sense, the intention of the construction was to get rid of superfluous structure encoded by equality. This has not been achieved, because the second order monadic predicates can still encode the same amount of superfluous structure as could be encoded by equality. Basically, the whole system is still equivalent to first order logic with equality.

The correct way to get rid of the superfluous structure would have been a weaker version of the axiom of extensionality. (Instead of $\forall x\forall y[\forall z(x\in z \leftrightarrow y\in z)\rightarrow x=y]$ it would be $\forall x\forall y[(\forall z(x\in z \leftrightarrow y\in z)\land\forall z(z\in x \leftrightarrow z\in y))\rightarrow x=y]$. The axiom of extensionality obviously also gets rid of the superfluous structure, but also has other consequences.) This is different from the second order identity of indiscernibles, exactly because it doesn't refers to quantification over second order predicates.

Answer 2

Is this law also true for Henkin semantics with comprehension axioms?

No, even if the language contains the identity predicate with its standard interpretation.

In the case where identity isn't in the language, the principle of identity of indiscernables (as stated, quantifying only over monadic properties) fails in the Henkin semantics. Why? Because we might have distinct individuals that can't be discriminated by any property in the class of monadic properties which are available in the second-order domain in the Henkin interpretation. (Just take an impoversihed second-order domain.)

So what happens if we add identity to the language (given the comprehension principle is in play)? What new properties have to be in the domain of the monadic second order quantifiers in an Henkin interpretation? For a start, properties like being self-identical; and (if we have a name for $a$) properties like being-identical-to-$a$. But take a Henkin interpretation where there are unnamed individuals in the domain (just chose a big enough domain), two distinct such individuals $x$ and $y$ could be indiscernible either by the available "ordinary" monadic properties in the domain, or by properties like being self-identical [both $x$ and $y$ have the property] or being being-identical-to-some-named-individua [neither $x$ nor $y$ have the property].

[At least, that's the basic idea. We could do an induction on the logical complexity of open wffs $\varphi$ built using identity to fancy up the argument.]

Of course, if we use a relational principle of the identity of indiscernables (at a first shot, $\forall x\forall y (\forall R\forall z(Rxz \equiv Ryz) \to x = y)$ and have the identity relation in the language and a suitable comprehension principle, then the principle is trivially true.