Your remarks bring me close to the border of my limited knowledge of model theory so I must be careful with my response. I believe the answer to your question:

Your remarks bring me close to the border of my limited knowledge of model theory so I must be careful with my response. I believe the answer to your question: > Do other considered set theories offer any improvements over ZFC in these specific respects? is "no", and that you essentially answer this yourself with the following paraphrasing of Löwenheim–Skolem: > As long as you stay within first-order predicate logic, a theory of sets will run into such issues. So if we opt Lawvere set theory I think we just do the same thing as if we had opted for ZCF, i.e., just assume we have a model (perhaps provided by some higher order logical system). However in my opinion, we do have a theory with a much more intuitive set of axioms.