[ux266478]

Of course. Though it's also important to note: whether or not an object exists is dependent on the logic being utilized itself, which is to say nothing of how even if the object holds some structural equivalent in the given logic of attention, it might not have all provable structure shared between the two, and that's before we get into how the chosen axioms on top of the logical system also mutate all of this.

It's not that classical logic is useless, it's just that it's not particularly appropriate to choose as the basis for a system built on algorithms. This goes both ways. Set theory was taken as the foundation of arithmetic, et al. because type theory was simply too unwieldy for human beings scrawling algebras on blackboards.

[gf000]

I am absolutely not even close to being an expert on the topic, but type theory wasn't all that well understood even relatively recently - Voevodsky coined the Univalence axiom in 2009 or so, while sets have been used for centuries.

So not sure it would be "unwieldy", it's a remarkably simple addition and it may avoid some of the pain points with sets? But again, not even a mathematician.

[zozbot234]

Set theory was chosen because it was a compatively simple proof of concept. You don't really refer to the foundation when scrawling algebra on a blackboard the way you would with a proof assistant, and this actually causes all sorts of issues down the line (it's a key motivation for things like HoTT).