Description: Specialization. A universally quantified wff implies the wff without a
quantifier. Axiom scheme B5 of Tarski p. 67 (under his system S2,
defined in the last paragraph on p. 77). Also appears as Axiom scheme C5'
in Megill p. 448 (p. 16 of the preprint). This corresponds to the axiom
(T) of modal logic.

For the axiom of specialization presented in many logic textbooks, see
theorem stdpc4 .

This theorem shows that our obsolete axiom ax-c5 can be derived from the
others. The proof uses ideas from the proof of Lemma 21 of Monk2
p. 114.

It appears that this scheme cannot be derived directly from Tarski's
axioms without auxiliary axiom scheme ax-12 . It is thought the best we
can do using only Tarski's axioms is spw . Also see spvw where x
and ph are disjoint, using fewer axioms. (Contributed by NM, 21-May-2008)(Proof shortened by Scott Fenton, 24-Jan-2011)(Proof
shortened by Wolf Lammen, 13-Jan-2018)