arXiv · 2009.03185
Short Axiomatization of Stratified Comprehension
Abstract
Several finite axiomatizations of stratified comprehension are known. This paper gives five set existence principles which, in the presence of Extensionality, yield the fourteen set-construction principles used in the finite basis recorded by Holmes. In addition, a direct unordered proof is given showing that the same five principles, together with extensionality only for nonempty sets, already imply every stratified comprehension instance, without passing through the Holmes ordered-pair machinery. The displayed reductions for unordered products, Cartesian products, and ordered relative products have been corrected. The original Holmes-basis reduction and the new direct weak-extensionality development have been checked by the Lean 4 kernel; the complete Lean source is supplied with this version.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Zuhair A. Al-Johar. 2026-09-22. Short Axiomatization of Stratified Comprehension. https://arxiv.org/abs/2009.03185
Cite the original work for its findings. Save a collection to share your selection of sources.