Set Theory with Types
Key topics
Regulars are buzzing about a novel approach to set theory that incorporates type theory, as outlined in a recent blog post. The discussion revolves around the potential benefits and challenges of combining these two mathematical frameworks, with commenters riffing on the implications for formal verification and proof assistants. Although the conversation is sparse, the few respondents seem to be enthusiastically exploring the possibilities of typed set theory, highlighting its potential to simplify certain mathematical constructs. As researchers continue to push the boundaries of formal mathematics, this thread feels particularly relevant right now, sparking interesting conversations about the future of mathematical foundations.
Snapshot generated from the HN discussion
Discussion Activity
Light discussionFirst comment
2d
Peak period
3
54-60h
Avg / period
3
Key moments
- 01Story posted
Nov 22, 2025 at 2:22 AM EST
about 1 month ago
Step 01 - 02First comment
Nov 24, 2025 at 12:02 PM EST
2d after posting
Step 02 - 03Peak activity
3 comments in 54-60h
Hottest window of the conversation
Step 03 - 04Latest activity
Nov 24, 2025 at 12:41 PM EST
about 1 month ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
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.
This actually comes in handy: While 1 ∈ 2 is nonsensical, `TRUE ∨ (1 ∈ 2)` is TRUE, and `FALSE ∧ (1 ∈ 2)` is false, and this is useful because then you can write:
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: and separately prove that y = x.7 more comments available on Hacker News