> 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.
> 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.