| ▲ | Set theory with types(lawrencecpaulson.github.io) | ||||||||||||||||||||||||||||||||||||||||||||||
| 91 points by baruchel 2 days ago | 15 comments | |||||||||||||||||||||||||||||||||||||||||||||||
| ▲ | pron 3 minutes ago | parent | next [-] | ||||||||||||||||||||||||||||||||||||||||||||||
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 part of the axioms. 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 can remain unknown (unprovable) and uninteresting. 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. | |||||||||||||||||||||||||||||||||||||||||||||||
| ▲ | bananaflag 2 days ago | parent | prev | next [-] | ||||||||||||||||||||||||||||||||||||||||||||||
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. | |||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||
| ▲ | epolanski 2 days ago | parent | prev [-] | ||||||||||||||||||||||||||||||||||||||||||||||
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. | |||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||