A new bridge links the math of infinity to computer science
Foundations: Set Theory vs. Type Theory
- Several comments contest the article’s claim that all modern math is built on set theory, pointing to type theory and category theory as alternative foundations.
- Defenders of ZFC emphasize its historical role and minimal, elegant axioms, while conceding it’s not how working mathematicians or computer scientists actually think day-to-day.
- Critics note ZFC is awkward for CS: in ZFC “everything is a set” (numbers as sets, functions as sets of pairs), whereas programming practice treats types as distinct and enforces boundaries; type theory better mirrors this.
- Others push back that in TCS research, type theory is still a niche area, and in practice many results are still framed set-theoretically, even if proof assistants use type theory under the hood.
Strength and Scope of Type Theories
- One subthread discusses the relative strength of type theories vs ZFC, noting some (e.g., underlying certain proof assistants) can be stronger than ZFC+extras, while many others are weaker.
- There’s disagreement over how influential type theory really is compared to set theory, though formalized math in Lean/Coq is cited as increasingly important.
Infinity, Finitism, and Constructivism
- Long debate on whether infinity “exists” or is just a process/limiting notion; several participants espouse finitist or ultrafinitist sympathies.
- Others argue:
- Infinity (and ordinals, transfinite methods) are deeply useful mathematically (e.g., Goodstein’s theorem, analysis, measure theory).
- Math doesn’t require physical existence of its objects; numbers and infinity are conceptual tools.
- Cantor’s diagonal argument and different sizes of infinity are challenged by some as misapplied finite intuitions; others strongly defend standard set-theoretic treatment and point to its internal consistency and consequences.
- Constructive vs classical views arise around diagonal arguments and the axiom of choice; some insist the “pathology” is about which axioms you accept, not about logic breaking.
Computer Science and the Infinite
- Several commenters object to the article’s framing that CS is mainly “finite,” pointing to: asymptotics, non-halting programs, automata over infinite alphabets, real-number encodings, and program analysis.
- Others stress CS rarely touches uncountable structures in practice; measure-theoretic infinities look far from everyday computing, though they underlie some theoretical work.
Surprisingness of the New Bridge
- Some feel it’s unsurprising that descriptive set theory and distributed algorithms align, given longstanding correspondences between logic and computation (Curry–Howard, etc.).
- Others (including people with PL/theory background) find it genuinely surprising: measure theory and descriptive set theory were long seen as needing non-constructive, “non-computational” tools, so a clean algorithmic correspondence is technically deep, not obvious.
Applications and Relevance
- Readers ask about practical uses (e.g., distributed systems, mesh networking).
- Responses propose possible implications for hardness/impossibility results in distributed algorithms and complexity.
- Skeptics argue that infinities are far removed from finite programs and real systems, at least near-term.
Critique of the Article / Quanta Style
- Multiple comments criticize the article’s opening line and its portrayal of CS as ignoring logic.
- Some see Quanta trending toward pop-sci, personality-driven narratives with clickbait titles and oversimplified technical claims, though others still value the outreach.
- One commenter suspects heavy LLM editing due to repetitive stylistic tics.
Meta, Humor, and Side Threads
- Numerous jokes about “calculating infinity,” Chuck Norris, Haskell definitions of infinite values, and
node_modulesembodying infinity on disk. - Side discussions touch on discrete/“gappy” number systems, p-adics, the ontology of numbers vs physical reality, and what “existence” means for mathematical objects.