I am one of the (rare on the Internet now) people that is a fan of "everything is a set".
Of course I don't believe that set theory is the One True Foundation and everything else is a lie, the fact that one can give a foundation with just one type of object, just one binary relation and relatively few simple axioms (or axiom schemas) is quite relaxing and I would say a bit unappreciated.
And also unlike other fellow students I never encountered any problem with more seemingly complicated constructions like tensor products or free groups since one can easily see how they are coded in set theory if one is familiar with it as a foundation.
As one of those that do not like the “sets at the bottom” approach I just want to highlight why. For me, mathematics built on sets have leaky abstractions. Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices. For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly. Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized. Finally, I do not mind sets, they are great, and a very useful tool, I just do not like they as the foundation. I firmly believe we should teach type theoretic or categorical foundations in mathematics and be less dependent on sets.
I'm more into only state change/differentiation exists.
Which of course means state is real.
Which mean langauge, syntax and semantics can be traced all the way down to fundementals.
Which means human meaning making is making the meaning of the universe, like an accidental organ of the universe.
And far from human meaning making being subjective its tied directly to physical existence and is objective.
And a cesium clock is all you need to derive everything fundemental.
That's what I play around with at least.
The idea that if stars are a process that emits photons and change energy gradients, humans are a process that emits complex meaning and change causal leverage gradients.
I don't understand arguments like "nobody can agree on what set theory is". This is not how mathematics work.
In mathematics labels are _not_ important, definitions are.
One simple example that everybody can relate to: do natural numbers include 0 or not? Who cares? Some definitions include it, some do not. There's even a convention of using N for N with 0, and N+ for excluding it, but even the convention is just a convention, not a definition. You could call them "funky numbers, the set of whole positive numbers including 0", and you're fine. Funky, natural, those are just names, labels, as long as you define them, it doesn't matter.
Same applies to set theory, there's many, many set theories, and they differ between properties, and this has never caused problems, because in mathematical discussion or literature...you provide or point to a definition. So you'll never discuss about "set theory" without providing one or pointing to one.
This is very, very different from how normal people waste their time.
E.g. arguing whether AI "thinks" or not, but never defining what thinking means, thus you can't even conclude whether you think or not, because it's never been defined.
The distinction between material set theories (like ZF and other set-theoretical foundations you might have heard about) and structural set theories (like ETCS, SEAR and most likely the "typed set theories" mentioned in OP) is rather fundamental. To the point that calling both of them "set theory" feels quite misleading.
Maybe because there are many different set theories. The one taught in school is not a correct one but grokable for most students. Then you got the Zermeno Frenkel set theory, and you got the Homotopy Type Theory one which can yield or emulate the same results. So in a sense the opening statement is correct. There is no consensus on a single "this is THE one and true correct set theory"
I think that the aesthetic dislike of "everything is a set" is misplaced, because it misses a crucial point that people unfamiliar with formal untyped set theories often miss: Not every proposition in a logic needs to be (or, indeed, can be) provable. The specific encoding of, say, the integers need not be an axiom. It's enough to state that an encoding of the integers as sets exists, but the propositions `1 ∈ 2` or `1 ∩ 2 ≠ ∅` can remain unprovable. Whether they're true or false remains unknown and uninteresting (or, put another way, "nonsensical").
The advantage is, then, that we can use a simple first order logic, where all objects in the logic are of the same type. This makes certain things easier and more pleasant. That the proposition `1 ∈ 2` can be written (i.e. that it is not a syntax error, though it's value is unknowable) should not bother us, just as that the English proposition "the sky is Thursday" is not a grammatical error and yet is nonsensical, doesn't bother us. It is no more or less bothersome than being able to write the proposition `1/x = 13`, with its result remaining equally "undefined" (i.e. unknowable and uninteresting) if x is 0. If `1/x = 13` isn't a syntax error, there's no reason `1 ∈ 2` must be a syntax error, either.
That a proposition is nonsensical (for all assignments of variables or for some specific ones, as in x = 0 in 1/x) need not be encoded in the grammar of the logic at all, and defining nonsense as "unknowable and uninteresting" is both convenient and elegant. I think that some logicians overlook this because they're attracted to intuitionist theories, where the notion of provability is more reified, whereas in classical theories every proposition is either true or false. They're bothered perhaps less by the ability to write 1 ∈ 2 and more by the idea that 1 ∈ 2 has a truth value. But while the notion of provability itself is not reified in classical logics, unprovable propositions are natural and common. 1 ∈ 2 has a meaning only in a very abstract sense; the theory can make that statement valid yet practically nonsensical by not offering axioms that can prove or disprove it. Things can be "undefined" in a precise way: the axioms do not allow you to come to any definition.
1 ∈ 2 is operating at a _different layer of abstraction_ than peano arithmetic is. It's like doing bitwise operations on integers in a computer program. You can do it, but at that point you aren't really working with integers as _integers_.
bananaflag|3 months ago
Of course I don't believe that set theory is the One True Foundation and everything else is a lie, the fact that one can give a foundation with just one type of object, just one binary relation and relatively few simple axioms (or axiom schemas) is quite relaxing and I would say a bit unappreciated.
And also unlike other fellow students I never encountered any problem with more seemingly complicated constructions like tensor products or free groups since one can easily see how they are coded in set theory if one is familiar with it as a foundation.
Atiscant|3 months ago
fellowniusmonk|3 months ago
Which of course means state is real.
Which mean langauge, syntax and semantics can be traced all the way down to fundementals.
Which means human meaning making is making the meaning of the universe, like an accidental organ of the universe.
And far from human meaning making being subjective its tied directly to physical existence and is objective.
And a cesium clock is all you need to derive everything fundemental.
That's what I play around with at least.
The idea that if stars are a process that emits photons and change energy gradients, humans are a process that emits complex meaning and change causal leverage gradients.
louthy|3 months ago
YouAreWRONGtoo|3 months ago
[deleted]
epolanski|3 months ago
In mathematics labels are _not_ important, definitions are.
One simple example that everybody can relate to: do natural numbers include 0 or not? Who cares? Some definitions include it, some do not. There's even a convention of using N for N with 0, and N+ for excluding it, but even the convention is just a convention, not a definition. You could call them "funky numbers, the set of whole positive numbers including 0", and you're fine. Funky, natural, those are just names, labels, as long as you define them, it doesn't matter.
Same applies to set theory, there's many, many set theories, and they differ between properties, and this has never caused problems, because in mathematical discussion or literature...you provide or point to a definition. So you'll never discuss about "set theory" without providing one or pointing to one.
This is very, very different from how normal people waste their time.
E.g. arguing whether AI "thinks" or not, but never defining what thinking means, thus you can't even conclude whether you think or not, because it's never been defined.
zozbot234|3 months ago
rootnod3|3 months ago
cmrx64|3 months ago
pron|3 months ago
The advantage is, then, that we can use a simple first order logic, where all objects in the logic are of the same type. This makes certain things easier and more pleasant. That the proposition `1 ∈ 2` can be written (i.e. that it is not a syntax error, though it's value is unknowable) should not bother us, just as that the English proposition "the sky is Thursday" is not a grammatical error and yet is nonsensical, doesn't bother us. It is no more or less bothersome than being able to write the proposition `1/x = 13`, with its result remaining equally "undefined" (i.e. unknowable and uninteresting) if x is 0. If `1/x = 13` isn't a syntax error, there's no reason `1 ∈ 2` must be a syntax error, either.
That a proposition is nonsensical (for all assignments of variables or for some specific ones, as in x = 0 in 1/x) need not be encoded in the grammar of the logic at all, and defining nonsense as "unknowable and uninteresting" is both convenient and elegant. I think that some logicians overlook this because they're attracted to intuitionist theories, where the notion of provability is more reified, whereas in classical theories every proposition is either true or false. They're bothered perhaps less by the ability to write 1 ∈ 2 and more by the idea that 1 ∈ 2 has a truth value. But while the notion of provability itself is not reified in classical logics, unprovable propositions are natural and common. 1 ∈ 2 has a meaning only in a very abstract sense; the theory can make that statement valid yet practically nonsensical by not offering axioms that can prove or disprove it. Things can be "undefined" in a precise way: the axioms do not allow you to come to any definition.
Indeed, this is exactly how the formal set theory in TLA+ is defined: https://pron.github.io/posts/tlaplus_part2
empath75|3 months ago
David-Henrry|3 months ago
[deleted]
nekomorphism|3 months ago
[deleted]