Theorem sp

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)

	Ref	Expression
Assertion	sp	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		alex	⊢ ( ∀ 𝑥 𝜑 ↔ ¬ ∃ 𝑥 ¬ 𝜑 )
2		19.8a	⊢ ( ¬ 𝜑 → ∃ 𝑥 ¬ 𝜑 )
3	2	con1i	⊢ ( ¬ ∃ 𝑥 ¬ 𝜑 → 𝜑 )
4	1 3	sylbi	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )