In axiomatic set theory, the axiom schema of predicative separation, or of restricted, or Δ0 separation, is a schema of axioms which is a restriction of the usual axiom schema of separation in Zermelo–Fraenkel set theory.
The axiom asserts only the existence of a subset of a set if that subset can be defined without reference to the entire universe of sets.
The formal statement of this is the same as full separation schema, but with a restriction on the formulas that may be used: For any formula φ, provided that φ contains only bounded quantifiers and, as usual, that the variable y is not free in it.
So all quantifiers in φ, if any, must appear in the forms for some sub-formula ψ and, of course, the definition of
The axiom appears in the systems of constructive set theory CST and CZF, as well as in the system of Kripke–Platek set theory.