Theorem·T49
Equality axioms are valid
Every instance of every equality axiom schema is satisfied by every structure under every assignment.
For a language
, L-structure
, assignment
, and
an equality axiom:
In words
Every formula that is an equality axiom is satisfied by every structure under every assignment - reflexivity from the ambient logic's own reflexivity, and substitutivity from the substitution lemma applied twice.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1A10: . By the eq clause of D091, iff , which holds by reflexivity of identity applied to the element .
- 2A11: , with and . Suppose and, for the consequent, suppose further (else the relevant implies clause of D091 holds vacuously); need . By the eq clause, the first supposition gives . By the substitution lemma (applicable since ), the second supposition gives . Since , the assignments and are the same function (D087, Extensionality: they agree with off and send to the same element), so . By the substitution lemma again (applicable since ): , and the right side holds, so the left side does too.
∎
Remarks
The equality third of soundness's case analysis over logical axioms; the other two are propositional and quantifier axioms. With all three in hand, every logical axiom is valid - the base cases of the soundness induction over a proof's length are done; only the two inference rules remain.