Is there a problem with Leibnizian-Russellian identity of indiscernibles in ZF?

[Frode Bjørdal]

In the following I use @ for the membership relation and ~> (<~>) for
implication (bi-implication). =: is the definition sign. [ and ] are used
to express extensional equality and two statements for property equality
(Eigenshaftsgleichheit) in definitions below.

While working in ZF without identity Ernst-Jochen Thiele in footnote 3,
page 175 of Ein Axiomatisches System der Mengenlehre, Zeitschrift für
Mathematische Logik und Grundlagenforschung der Mathematik, Bd. 1, S.
173-195, 1955, writes as the following:

“Durch Gegenbeispiele kann man zeigen, daß es nicht wie in der Typentheorie
genügt, die Eigenschaftsgleichheit wie folgt zu definieren: x]]y=:(z)(x at z
~>y at z).”

Translated into English: “One can show with counter examples that it is not
sufficient to define property equality as follows, like in Type theory:
x]]y=:(z)(x at z~>y at z).”

Thiele on the same page suggest the following alternative definition for
property equality:

x[]y=:(z)(x at z<~>y at z)

Define coextensionality as follows:

x][y=:(z)(z at x<~>z at x)


Thiele defines identity as follows on the same page 175: x=y=:x][y & x[]y

I don't understand Thiele's claim in the quoted footnote, as it to me seems
that we in a straightforward manner may prove x]]y~>y]]x if we have the
]]-pairing axiom so that we obtain the following ]]-singleton principle:

(x)(Ez)(y)(y at z<~>x]]z)

Furthermore, it seems to me that we may straightforwardly prove x[]y~>x][y,
and consequently x]]y~>x=y.

Am I right?
.......................................................
Professor Dr. Frode Alfson Bjørdal
Universitetet i Oslo Universidade Federal do Rio Grande do Norte
quicumque vult hinc potest accedere ad paginam virtualem meam
<http://www.hf.uio.no/ifikk/personer/vit/fbjordal/index.html>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200811/1ba15074/attachment-0001.html>