Theory of Definition & Kurt Gödel's Proof of God - Lecture 13 (Logic)

What does the criterion of eliminability require of a definition?

1. A.The defined symbol must occur in at least one axiom of the system
2. B.Any formula using the new symbol must be logically equivalent to one without it
3. C.The defined symbol must be expressible using only a single primitive
4. D.Each definition must reduce the total number of symbols in the system