I thought about creating quantum recursive sets, where set definitions that depend on the set itself are defined as the limit of a sequence if it exists, which would naturally give the same result as normal set notation, but for set definition sequences which do not converge you end up with a 'quantum set' which is the sum of two or more sets. It works, but I cant find a single case where it gives any interesting or useful result. There are some problems which lead to multiple possible sets, but in general there turns out to be 2 'extreme' situations, in the case of OPs set you get A) the superposition of the empty set and the set of all elements in the universe you are working in S = {}&U, and B) the superposition of all subsets of the universe S = &P(U), where I use & as the superposition operator.
Why can't we define a set this way?
You can in New Foundations.
ZF set theory (and HoTT etc.) don't let you take the absolute complement of a set/type. Probably one of their more glaring deficiencies.
How the fuck do I into HoTT? Do I really need to be familiar with alg top and cat theory before?
You should know some category theory and general MLTT, and at least the idea of the fundamental group(oid) (which is pretty intuitive). General MLTT is most important though.
"absolute complements" never actually come up in actual mathematical practice. in fact, quantification over "all sets" is itself a huge meme
I was told the introduction to type theory was pretty good though, they made it seem like I could just use it and not have to read specifically about MLTT. By the way, is there any good paper that highlights the differences of type theory and "normal logic"? It's not clear to me what their fundamental differences are, for example, what's the difference between intuitionistic logic (where the notion of truth is proof theoretic) and type theory?
>the introduction to type theory
You mean in the HoTT book? I would combine it with Martin-Loef's original paper which is extremely clear (although it uses a few weird definitions/concepts).
>It's not clear to me what their fundamental differences are, for example, what's the difference between intuitionistic logic (where the notion of truth is proof theoretic) and type theory?
Type theory *is* intuitionistic. It's a refinement of natural deduction to include terms as well as types. Read ML's paper and this will all be clear.
>>"absolute complements" never actually come up in actual mathematical practice
Yeah but they come up in real life. You can say Gandhi is not a spoon without specifying any common set that they belong to, because they are both things that exist. This is really a problem of not having a universal set more than anything.
Just to be sure, you're referring to the paper from 1972 "An Intuitionistic Theory of Types"?
Intuititionist type theory (1986)