Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
This is probably a question for Mike, but anybody could answer it.
Have you ever come across an axiom scheme of (say material) set theory, which I’m tentatively calling subset separation (or perhaps better, but longer, power-class-bounded separation), stating the axiom of separation for all formulas in which all quantifiers are guarded by some power class, so of the form ∀x⊆t,… or ∃x⊆t,…, or guarded by a set (as usual).
Subset separation follows from full separation; it also follows from bounded separation and power sets. Arguably, it is the impredicative core common to the axioms of full separation and power sets.
In Mathias’ paper “The strength of Mac Lane set theory”, section 6, he calls formulas of that sort Δ𝒫0, so that your axiom scheme would be called “Δ𝒫0-separation”. He also uses “restricted” for quantifiers guarded by a set and “limited” for quantifiers guarded by the power class of a set, so that perhaps your axiom could also be called “limited separation” (as opposed to “restricted separation” meaning Δ0-separation).
He references the following papers, which I have not read:
Thanks!
1 to 3 of 3