What axioms of equality do you have? One can prove from them that equality is an equivalence relation.
Hi everyone, first time poster here.
I'm trying to figure out how to show that the interpretation of equality in a model of equality is an equivalence relation.
As in, if I have a structure that satisfies the axioms of equality, how do i show that this structure also satisfies the axioms of equivalence relations?
I've got 2 axioms of equality:
1. for every x, x=x
2. for every x and for every y, (x=y --> (fi(x,x) --> fi(x,y))) where fi(x,x) is an atomic formula with x substituted for some of the x in fi
I'm confused about how to formally say that if a structure satisfies these axioms then they hold true under an interpretation of equality in that structure.
You are saying you don't know how to say "if A, then B." But your A and B are the same thing by definition. A structure satisfies a formula iff a formula is satisfied by that structure.
A definition of when a first-order formula is true in a structure can be found in Wikipedia. This definition assumes that you have a logic "with equality," which means that equality is interpreted as identity: if the interpretation of and in M is literally the same element of the domain of M. In this case, the interpretation of equality (i.e., identity) is an equivalence relation by definition. Since your problem asks to prove that the interpretation of equality is an equivalence relation, you probably have a logic "without equality," where = is just a predicate symbol like any other and it can be interpreted by an arbitrary relation as long as equality axioms are true.
Suppose you have a model of the equality axioms where = is interpreted by a relation R. Then R is reflexive because of the first axiom. Further, x = y -> x = x -> y = x is an instance of axiom 2 where is x = x. Indeed, y = x is obtained by replacing the first occurrence of x in with y. Therefore, R is symmetric. Finally, x = y -> z = x -> z = y is also an instance of axiom 2 where is z = x. Indeed, z = y is obtained from z = x by replacing x in with y. Switching the two assumptions, we get the transitivity property.