Leonid A. Levin
Usual math sets have special types: countable, compact, open, occasionally Borel, rarely projective, etc. Each such set is described by a single Set Theory formula with parameters unrelated to other formulas. Exotic expressions involving sets related to formulas of unlimited quantifiers height appear mostly in esoteric or foundational studies. Recognizing internal to math (formula-specified) and external (based on parameters in those formulas) aspects of math objects greatly simplifies foundations. I postulate external sets (not internally specified, constituting the domain of variables) to be hereditarily countable and independent of formula-defined classes, i.e. with finite algorithmic information about them. This allows to eliminate all non-integer quantifiers in Set Theory sentences. All with seemingly no need to change almost anything in mathematical papers, only to reinterpret some formalities.