Short Axiomatization of Stratified Comprehension
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.