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:

Two bisimular states may be unequal in the model.
Two syntactical weight terms may be equal in the model, but different in a wellfounded ordering.
Two functions may be intensionally different but extensionally equal.
Of two Evans-equal terms, one may be relevant and the other irrelevant.

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.