Lecture 5 (Logic) Inference with Quantifiers and an Axiomatic System

What does the rule of Universal Specification (US) allow?

1. A.Replacing ∀x P(x) with ∃x P(x) when the domain is non-empty
2. B.Concluding ∀x P(x) from a derivation of P(a) for some constant a
3. C.Inferring P(t) for any term t from ∀x P(x)
4. D.Removing the universal quantifier only when the domain is the natural numbers