The people that make theorem provers, because they are type theorists and not set theorists doing ZFC derivatives, are very aware of your last point. Painfully aware, from years of people dismissing their work.
Read Andrej Bauer on them many foundations of math, for example. Clearly he is a believer in "no one true ontology".
> The people that make theorem provers [...] are very aware of your last point.
> Clearly he is a believer in "no one true ontology".
My point wasn't that you should aim for some kind of fictitious absence of ontological commitments, only that whatever language you use will have ontological commitments. Even the type judgement e:t has ontological implications, i.e., for the term e to be of type t presupposes that the world is such that this judgement is possible.
You can still operate under Fregean/Russellian presuppositions without sets. For example, consider the problem of bare particulars or the modeling of predicates on relations.
Indeed, and e:t in type theory is quite a strong ontological commitment, it implies that the mathematical universe is necessarily subdivided into static types. My abstraction logic [1] has no such commitments, it doesn't even presuppose any abstractions. Pretty much the only requirement is that there are at least two distinct mathematical objects.
Read Andrej Bauer on them many foundations of math, for example. Clearly he is a believer in "no one true ontology".