Axiomatic WikiWWikiDDefinitionsEquality logical axiom schemas
Definition·D102
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
there exist
and, for the second schema,
,
, and
with
and
, such that, writing formulas and terms with the notation,
is one of:
In words
A formula is an equality axiom exactly when, for some term and, for the second shape, another term, a variable, and a formula free for it in both terms, it is one of: some term equals itself, or the terms being equal implies that substituting the first for the variable in the formula implies substituting the second for it 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.