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_modules embodying 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.