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
In all these cases, equality implies substitutability only in some contexts.
- 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
- Of two
one may be relevant and the other irrelevant.
This is file p/eq0.html on Claus-Peter Wirth's web site.
Last modified 2004/10/17/17.40.