Suppose that $L$ is a second-order language, where we do not assume $=$ is a primitive. Let $T$ be an $L$-theory containing Comprehension for all arities (we just need unary and binary below).

Clearly, these conditions (a) and (b) are the formal syntactic properties of $=$. That is, reflexivity and substitutivity.Definition: An $L$-formula $x \approx y$ is aLeibniz formulain $T$ just in case both the following hold:

(a) $T \vdash \forall x(x \approx x)$for any $L$-formula $\phi(z)$.

(b) $T \vdash \forall x \forall y(x \approx y \rightarrow (\phi(z/x) \rightarrow \phi(z/y))$,

Lemma 1: Let $x \approx y$ be a Leibniz formula in $T$. Then:

(i) $T \vdash \forall x \forall y(x \approx y \leftrightarrow \forall X(Xx \rightarrow Xy))$

(ii) $T \vdash \forall x \forall y(x \approx y \leftrightarrow \forall R(\forall z Rzz \rightarrow Rxy))$

**Proof**

Part (i) By comprehension, $\forall y \exists X \forall x(Xx \leftrightarrow x \approx y)$. Let $a$ be such that $\exists X \forall x(Xx \leftrightarrow x = a)$. Let $A$ be such that $\forall x(Ax \leftrightarrow x \approx a)$. Thus, $Aa \leftrightarrow a \approx a$. Since $a \approx a$, we have $Aa$. Let $b$ be such that $\neg(a \approx b)$. By symmetry of $\approx$, $\neg(b \approx a)$. So, $\neg Ab $. So, $Aa \wedge \neg Ab$. Hence, $\neg (a \approx b) \rightarrow (Aa \wedge \neg Ab)$. So, $\neg(a \approx b) \rightarrow \exists X(Xa \wedge \neg Xb)$. Since $a$ and $b$ are arbitrary, $\forall x \forall y(\neg(x \approx y) \rightarrow \exists X(Xx \wedge \neg Xy)$. By contraposition, $\forall x \forall y(\forall X(Xx \rightarrow Xy) \rightarrow x \approx y)$, as required. (Notice that this requires simply that $\approx$ be reflexive and symmetric.)

For the converse, suppose $a \approx b$ and $Xa$. By substitutivity, $Xb$. So, $Xa \rightarrow Xb$. So, $\forall X(Xa \rightarrow Xb)$. So, $a \approx b \rightarrow \forall X(Xa \rightarrow Xb)$. So, $\forall x \forall y(x \approx y \rightarrow \forall X(Xx \rightarrow Xy)$, as required. (This requires substitutivity.) QED.

Part (ii). First, we have $\forall z (z \approx z)$. Suppose that $\forall R (\forall z Rzz \rightarrow Rab)$. By comprehension, $\exists R \forall x \forall y(Rxy \leftrightarrow x \approx y)$. So, $\forall z (z \approx z) \rightarrow a \approx b$. So, $a \approx b$. So, $\forall R (\forall z Rzz \rightarrow Rxy) \rightarrow a \approx b$. So, $\forall x \forall y(\forall R (\forall z Rzz \rightarrow Rxy) \rightarrow x \approx y)$, as required. (Notice that this requires merely that $\approx$ be reflexive.)

For the converse, suppose $a \approx b$ and $\forall z Rzz$. So, $Raa$. By substitutivity, $Rab$. So, $\forall z Rzz \rightarrow Rab$. So, $\forall R(\forall z Rzz \rightarrow Rab)$. So, $a \approx b \rightarrow \forall R(\forall z Rzz \rightarrow Rab)$. So, $\forall x \forall y(x \approx y \rightarrow \forall R(\forall z Rzz \rightarrow Rxy)$, as required. (This requires substitutivity.) QED.

There is a sense in which the notion of being a Leibniz formula is unique. For:

Lemma 2: Let $x \approx y$ and $x \equiv y$ be Leibniz formulas in $T$. Then:

$T \vdash \forall x \forall y(x \approx y \leftrightarrow x \equiv y)$

**Proof**. By symmetry, it is no loss of generality to prove just one direction. Suppose $x \approx y$. An instance of substititivity is $x \approx y \rightarrow (x \equiv x \rightarrow x \equiv y)$. (Take $\phi(z)$ to be $x \equiv z$. Then $\phi(z/x)$ is $x \equiv x$ and $\phi(z/y)$ is $x \equiv y$.) So, $x \equiv x \rightarrow x \equiv y$. But, we already have $x \equiv x$. So, $x \equiv y$, as required. QED.

Thus, any two Leibniz formulas (in $T$) are provably equivalent (in $T$).

Your blog is very informative, finally, I found exactly what I want. Paypal is an excellent service for online payments but lots of its users confront issues while they access Paypal. If you want to resolve your problems then must visit Paypal contact.

ReplyDeleteYour blog is very informative and interesting to read, finally, I found exactly what I searching for. There are lots of users of Macfee antivirus in the world because of its features and easy interface. If you want to explore more interesting facts about Mcafee antivirus or want to resolve your technical issues then must visit helpdesk Mcafee.

ReplyDeleteHi, Thank you for sharing such a good and valuable information,It is very important for me. Gmail is the worldwide used email service but sometimes user faces some problems in it. If you want to get some information about the Gmail then you can visit Gmail asiakaspalvelu.

ReplyDeleteUnbelievable blog! This blog provides a brief introduction which is very helpful for me. Instagram is the most usable platform in the world because of its latest features but the user some time confronts some issues on Instagram. For more information, you can visit Instagram-tili.

ReplyDeleteHi..I read out your blog and that is so informative for me. You must visit on another blog which is very helpful for us avast deinstallieren

ReplyDeleteHi your post is really appreciatable.I really thankful for this post. Here i would llike to share some information about facebook. As we know that facebook is a social trap where we connect with people in all over world. So if you are using facebook and face any technical issue that time so just visit our website. We can resolve the smallest problem on same time. For further information please visit on our website- facebook bellen belgie

ReplyDeleteHi thankyou for this great helpful information.this information is really useful at today's time.you had easily explained whole information in a short note. Now i would like to share some information about PayPal.So If you are a Paypal user and you are facing any problem regarding to PayPal. No need to worry just simply visit on our site- paypal klantenservice belgie

ReplyDeleteHi this post is very nice.finally i got all those information whatever i really wanted to know. Thankyou for sharing this usefull information. Here I want to share the information about Dell support. As we all have been digitalied and we do multiple works together so if you face any problem or need any assist about Dell klentenservice so pleae visit over this site:- dell ondersteuning bellen

ReplyDeleteReally Nice Post Admin, Very helpful looking for more posts, Now I have to share some information about How To Fix “Lenovo Troubleshooting Guide” problem. If you are going through this problem you can simply visit Lenovo ondersteuning

ReplyDelete