If two sets contain the same elements, they are equal.
\(\forall x \forall y[\forall z(z\in x \leftrightarrow z\in y)\rightarrow x=y]\)
This is an axiom, not a definition, because equality was defined as part of first-order logic.
Note that this is not bidirectional. \(x=y\) does not imply that \(x\) and \(y\) contain the same elements. This is appropriate as \(\dfrac{1}{2}= \dfrac{2}{4}\) for example, even though they are written differently as sets.
The reflexive property is:
\(\forall x(x=x)\)
We can replace the instance of \(y\) with \(x\):
\(\forall x [\forall z(z\in x \leftrightarrow z\in x)\rightarrow x=x]\)
We can show that the following is true:
\(\forall z(z\in x \leftrightarrow z\in x)\)
Therefore:
\(\forall x [T \rightarrow x=x]\)
\(x=x\)
The symmetry property is:
\(\forall x \forall y[(x=y)\leftrightarrow (y=x)]\)
We know that the following are true:
\(\forall x \forall y[\forall z(z\in x \leftrightarrow z\in y)\rightarrow x=y]\)
\(\forall x \forall y[\forall z(z\in x \leftrightarrow z\in y)\rightarrow y=x]\)
So:
\(\forall x \forall y[\forall z(z\in x \leftrightarrow z\in y)\rightarrow (x=y\land y=x)]\)
The transitive property is:
\(\forall x \forall y \forall z[(x=y \land y=z) \rightarrow x=z]\)
The substitutive property for functions is:
\(\forall x \forall y[(x=y)\rightarrow (f(x)=f(y))]\)
The substitutive property for formulae is:
\(\forall x \forall y[((x=y)\land P(x))\rightarrow P(y)]\)
Doesn’t this require iterating over predicates? Is this possible in first order logic??
We can now show the empty set is unique.
If an element did not exist, the set containing it would be equal to a set which did not contain that element.
We have already ready defined the relationship equality, between terms.
\(a=b\).
Sometimes we may wish to talk about a collection of terms which are all equal to each other. This is an equivalence class.
Though we have not yet defined them, integers are example of this. For example \(-1\) can be written as \(0-1\), \(1-2\) and so on.
\(\forall y \forall x x=y\rightarrow x\in z\)
For all sets, we can call the class of all sets equal to the set an equivalence class.
This does not necessarily exist.