In Higher-order Settings
In a typed language where we can quantify over predicates, the axiom schema of specification becomes a simple axiom. This is much the same trick as was used in the NBG axioms of the previous section, where the predicate was replaced by a class that was then quantified over.
In second-order logic and higher-order logic with higher-order semantics, the axiom of specification is a logical validity and does not need to be explicitly included in a theory.
Read more about this topic: Axiom Schema Of Specification