Theorem·T48
Quantifier axioms are valid
Every instance of every quantifier axiom schema is satisfied by every structure under every assignment.
For a language
, L-structure
, assignment
, and
a quantifier axiom:
In words
Every formula that is a quantifier axiom is satisfied by every structure under every assignment - each schema's side condition is exactly what its validity proof needs.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1A8: , with . Suppose (else the implies clause of D091 holds vacuously); need . By the forall clause, for every ; taking gives . By the substitution lemma (applicable since ): , and the right side holds, so the left side does too.
- 2A9: , with . Suppose and, for the consequent, suppose further (else the relevant implies clause of D091 holds vacuously); need . Fix . By the forall clause applied to the first supposition: . Since , T44 gives , and the right side holds by the second supposition, so . By the implies clause: . As was arbitrary, the forall clause gives .
∎
Remarks
The quantifier third of soundness's case analysis over logical axioms; the other two are propositional axioms and equality axioms. This is precisely where dropping either side condition would break the argument: without
in A8, the substitution lemma would not apply; without
in A9, T44 would not apply, and the counterexample in D099's notes shows the schema genuinely fails without it.