Definition·D102
Equality logical axiom schemas
Every term equals itself, and substituting equal terms for a free variable cannot change whether a formula holds.
For a language
, a formula
is an equality axiom
is one of:
In words
A formula is an equality axiom exactly when it has one of two shapes: a term equals itself, or two equal terms, both free for a variable in a formula, imply that substituting either for that variable holds exactly when the other does.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 · A09 (computed from the citation graph, not asserted).
Remarks
The second schema is Leibniz's law in axiom form: equal terms are interchangeable in every context that does not capture their variables (guarded, as in D101, by substitutability for both
and
). Soundness will confirm both schemas are valid in every structure: reflexivity is immediate from equal values are equal, and the second follows once substitution is shown to change a formula's truth value only through the substituted term's own value. Together with D100 and D101, these complete the logical axioms.