The basic principles of entailment for identity are among the most familiar of logical principles; but, because equations do not have sentential components, they will play a role in derivations that is quite different from other logical forms we study.
6.3.1. Logical properties of identity
For our purposes, identity amounts to sameness in all respects, a sameness that implies interchangeability as input for any predicate or functor.
6.3.2. A law for aliases
Many of the valid conclusions from a group of equations can be captured by rules telling when terms count as co-aliases
—i.e., aliases for the same thing.
6.3.3. Derivations for identity
The key rules for identity are rules for closing gaps, but all rules can be extended to reflect the interchangeability of co-aliases.