## Mathematical Aphorisms. Part 6.

It seems underemphasized that the parsimony of ZFC in the way of ‘types’ (having only one sort called sets) has the following practical and notational virtue: you can get by with a single type of the quantifier $\exists$, and a single type of the quantifier $\forall$; multi-sorted formalisms need multiple sorts for each of $\exists$ and $\forall$, respectively. Why? Because otherwise the semantics do not work. (You can find a suitable example for yourself.)