Notion of Primitive Equality

Primitive Equality (_=_) can be understood as the equality in the model. More generally, one could take primitive equality as an arbitrary equivalence relation that satisfies Leibniz substitutability, but this is nothing but the equality in the factor or quotient structure. According to Tarski, primitive equality is a logical notion. Thus, roughly speaking, any signature should include an equality symbol for all types that is to be interpreted as equality in the model.

For more sophisticated approaches, equality cannot simply be taken as equality in the model. This is always the case when equality does not imply substitutability everywhere. For example:

In all these cases, equality implies substitutability only in some contexts.
This is file p/eq0.html on Claus-Peter Wirth's web site.
Last modified 2004/10/17/17.40.