Thank you for the links!
As stated in Tom Leinster's paper that you link to, both ZFC and Lawvere set theory are first-order theories:
"In logical terminology, both axiomatizations [i.e., ZFC and Lawvere set theory] are simply first-order theories."
This means that with both theories, we cannot categorically define important concepts such as the natural numbers, due to the compactness theorem and its consequence, the upward Löwenheim-Skolem theorem that hold in first-order logic:
https://en.wikipedia.org/wiki/Categorical_theory
https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_...
Also, the downward Löwenheim-Skolem theorem leads to Skolem's paradox, because ZFC proves (as we expect from a set theory) Cantor's theorem, and at the same time we know that if ZFC is consistent, then it has a countable model:
https://en.wikipedia.org/wiki/Skolem%27s_paradox
So, even the rather basic notion of countability is relative.
As long as you stay within first-order predicate logic, a theory of sets will run into such issues.
From what I see, such issues are often "resolved" when working with ZFC by stating explicitly that a very specific (i.e., the "intended") model is meant, with the caveat that, from a logical perspective, we do not even know whether the theory is consistent and hence whether such a model in fact exists.
Thus, even though ostensibly working "in" ZFC, a meta-logical statement about the intended models seems often necessary that cannot be formulated in first-order logic because with first-order predicate logic, we cannot control the cardinality of infinite models.
Do other considered set theories offer any improvements over ZFC in these specific respects?
As stated in Tom Leinster's paper that you link to, both ZFC and Lawvere set theory are first-order theories:
"In logical terminology, both axiomatizations [i.e., ZFC and Lawvere set theory] are simply first-order theories."
This means that with both theories, we cannot categorically define important concepts such as the natural numbers, due to the compactness theorem and its consequence, the upward Löwenheim-Skolem theorem that hold in first-order logic:
https://en.wikipedia.org/wiki/Categorical_theory
https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_...
Also, the downward Löwenheim-Skolem theorem leads to Skolem's paradox, because ZFC proves (as we expect from a set theory) Cantor's theorem, and at the same time we know that if ZFC is consistent, then it has a countable model:
https://en.wikipedia.org/wiki/Skolem%27s_paradox
So, even the rather basic notion of countability is relative.
As long as you stay within first-order predicate logic, a theory of sets will run into such issues.
From what I see, such issues are often "resolved" when working with ZFC by stating explicitly that a very specific (i.e., the "intended") model is meant, with the caveat that, from a logical perspective, we do not even know whether the theory is consistent and hence whether such a model in fact exists.
Thus, even though ostensibly working "in" ZFC, a meta-logical statement about the intended models seems often necessary that cannot be formulated in first-order logic because with first-order predicate logic, we cannot control the cardinality of infinite models.
Do other considered set theories offer any improvements over ZFC in these specific respects?