[HN Gopher] Set theory with types
___________________________________________________________________
Set theory with types
Author : baruchel
Score : 111 points
Date : 2025-11-22 07:22 UTC (2 days ago)
(HTM) web link (lawrencecpaulson.github.io)
(TXT) w3m dump (lawrencecpaulson.github.io)
| epolanski wrote:
| 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.
| cmrx64 wrote:
| what... argument? anyway, pretty sure larry is quite fluent
| with how mathematics is done.
| epolanski wrote:
| Doesn't show in the premise.
| TimorousBestie wrote:
| That first sentence has very little to do with the content
| of the essay; you're being pedantic. You understand very
| well what was meant.
| epolanski wrote:
| You're probably right, that was a bit pointless of a
| comment.
| rootnod3 wrote:
| 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"
| zozbot234 wrote:
| 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.
| bananaflag wrote:
| 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.
| Atiscant wrote:
| 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.
| librexpr wrote:
| > Say I want natural numbers, I need to choose a concrete
| implementation in set theory e.g. Von Neumann, but there are
| multiple choices.
|
| You don't need to choose a concrete implementation. If you
| don't want to choose a construction, you can just say
| something like "let (N, 0, +, *) be a structure satisfying
| the peano axioms" and work from there.
|
| > 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.
|
| Why is that problematic? The constructions are isomorphic
| under the sentences that actually matter. This kind of
| statement is usually called a "junk theorem", and they are a
| thing in type theory too, see for example this quote from a
| faq by Kevin Buzzard about why Lean defines division by zero
| to be zero:
|
| > The idiomatic way to do it is to allow garbage inputs like
| negative numbers into your square root function, and return
| garbage outputs. It is in the theorems where one puts the
| non-negativity hypotheses.
|
| https://xenaproject.wordpress.com/2020/07/05/division-by-
| zer...
|
| > Secondly, it is hard to formalize, and I think mathematics
| desperately needs to be formalized.
|
| Is that actually true? At the very least writing out the
| axioms and derivation rules is easier for set theory, since
| it's simpler than type theory. And there has been plenty of
| computer-verified mathematics done in Metamath/set.mm and
| Isabelle/ZF, even though less has been done than in type
| theory. Currently the automated tools are better for type
| theory, but it seems likely to me that that has more to do
| with how much effort has been put into type theory than any
| major inherent advantages of it.
|
| ---
|
| More generally, types in type theory are also constructed!
| The real numbers in Lean don't come from the platonic realm
| of forms, they are constructed as equivalence classes of
| cauchy sequences. And the construction involves a lot of
| type-theoretic machinery which I'd usually rather ignore when
| working with reals, much like I'd usually rather ignore the
| set-theoretic construction of the real numbers. And the great
| thing is that I can ignore them, in either foundation!
|
| So I just don't really buy these common criticisms of set
| theory, which to me seem like double standards.
| Atiscant wrote:
| Sure you can work around it most of the time, but some
| times you cant. The whole point is that isomorphic is _not_
| equality in set theory, and sometimes proofs does not
| transfer along isomorphism because they refer to
| implementations. I agree that it is much preferable to work
| with abstract structure, but that not always what happens
| in practice. The natural number example is contrived but
| easy to see. My point of view is also that I do not like
| the Lean approach. It would actually like no junk theorems
| to exist in my theory. I am much more partial to the
| univalent approach and in particular univalent
| implementation that compute e.g. cubical. Regarding how
| easy it is to formalize, you are right. Lots of good work
| happens with set theory based type theory. My point was
| also that set theoretic foundations themselves are very
| hard to formalize, e.g ZFC + logic is very difficult to
| work from. A pure type theoretical foundations is much
| easier to get of the ground from. To prove that plus
| commutes directly from ZFC is a nightmare.
| zero-sharp wrote:
| >Say I want natural numbers, I need to choose a concrete
| implementation in set theory
|
| In what situation do you ever actually need a set theoretic
| foundation of the natural numbers to get work done?
| louthy wrote:
| Have you considered the next step from sets into Category
| Theory?
| bananaflag wrote:
| Yes, I am very familiar with category theory. Not sure I
| would consider it the "next step from sets". Sure, there are
| alternative foundations based on category theory, but that is
| not its only or its main use.
| fellowniusmonk wrote:
| 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.
| pron wrote:
| 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.
|
| Indeed, this is exactly how the formal set theory in TLA+ is
| defined: https://pron.github.io/posts/tlaplus_part2
| empath75 wrote:
| 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_.
| pron wrote:
| If 1 [?] 2 is neither provable nor refutable, then you're not
| working with anything. The proposition literally has no
| meaning. It's not a syntax error, but you can't use its value
| for anything. Its value is undefined.
|
| This actually comes in handy: While 1 [?] 2 is undefined, `(2
| > 1) [?] (1 [?] 2)` is true, and `(1 > 2) [?] (1 [?] 2)` is
| false, and this is useful because it means you can write:
| x = 0 [?] 1/x [?] 0
|
| which is a provable theorem despite the fact that the clause
| `1/x` is difficult to typecheck. This comes in even more
| handy once you apply substitutions. E.g. it is very useful to
| write: y = 0 [?] 1/x [?] 0
|
| and separately prove that y = x.
|
| To make this convenient, typed theories will often define 1/0
| = 0 or somesuch (but they don't complain about that). In
| untyped set theory, 1 [?] 2 and 1/0 can remain valid yet
| undefined.
|
| Of course a ZF set theory operates with different objects
| than Peano arithmetic - it's a different theory. But Peano
| arithmetic nevertheless applies to any encoding of the
| integers, even the ones where 1 [?] 2 is undefined.
___________________________________________________________________
(page generated 2025-11-24 23:02 UTC)