118 points by digital55 5 hours ago | 7 comments
shevy-java 2 hours ago
Finally - we can calculate infinity.

Been a long way towards it. \o/

gorgoiler 1 hour ago
If you’re in the Bay Area next month then The Dillinger Escape Plan are bringing the Calculating Infinity circus to town(s):

https://www.theregencyballroom.com/events/detail/?event_id=1...

This is enormously off topic but if one person sees this and ends up not missing the show then it was worth mentioning. I think there’s a reasonable crossover between math, discrete math, hacking, and mathcore :)

anon291 43 minutes ago
Fairly trivial, in haskell:

let x = x in x

Completely encapsulates a countable infinity.

firecall 1 hour ago
>Finally - we can calculate infinity.

And Beyond!

keyle 51 minutes ago
This has indeed taken forever /s
donw 22 minutes ago
That’s nothing, ‘node_modules’ has been linking the math of infinity to my filesystem for years.
dboreham 26 minutes ago
Confused why the article author believes this is a surprise. The foundations of mathematics and computer science are basically the same subject (imho) and dualities between representations in both fields have been known for decades.
alexnewman 36 minutes ago
I studied math for a long time. I’m convinced math would be better without infinity. It doesn’t exist. I also think we don’t need numbers too big . But we can leave those
dullcrisp 7 minutes ago
I think we can stop at 8.
dumstick 19 minutes ago
Is this a joke or are you deeply interested in some ZFC variant that im unaware of? We absolutely need infinity to make a ton of everyday tools work, its like saying we dont need negative numbers because those dont exist either.
anthk 2 hours ago
It's cons'es all the way down.
anon291 44 minutes ago
> computer science with the finite

um... no... computer science is very concerned with the infinite. I'm surprised quanta published this. I always think highly of their reporting.

k_bx 3 hours ago
> All of modern mathematics is built on the foundation of set theory, the study of how to organize abstract collections of objects

What the hell. What about Type Theory?

philipfweiss 2 hours ago
Type theory is actually a stronger axiomatic system than ZFC, and is equiconsistent with ZFC+ a stronger condition.

See this mathoverflow response here https://mathoverflow.net/a/437200/477593

zozbot234 1 hour ago
Regardless of the name, descriptive set theory does not seem to have all that much to do with "set theory" in a foundational sense; it can be recast in terms of types and spaces with comparative ease, and this can be quite advantageous. The article is a bit confusing in many ways; among other things, it seems quite obviously wrong to suggest that recasting a concept that seems to be conventionally related to mathematical "infinities" in more tangible computational terms is something deeply original to this particular work; if anything, it happens literally all the time when trying to understand existing math in type-theoretic or constructive terms.
rdlw 3 hours ago
Is there a collection of type theory axioms anywhere near as influential as ZF or ZFC?
k_bx 3 hours ago
Sure, but is discarding Type Theory and Category Theory really fair with a phrase like "All of modern mathematics"? Especially in terms of a connection with computer science.
anon291 41 minutes ago
Arguably, type theory is more influential, as it seems to me all the attempts to actually formalize the hand-wavy woo mathematicians tend to engage in are in lean, coq, or the like. We've pretty much given up on set theory except to prove things to ourselves. However, these methods are notoriously unreliable.
3 hours ago
umanwizard 3 hours ago
"the study of how to organize abstract collections of objects" is not really a great explanation of set theory. But it is true that the usual way (surely not the only way) to formalize mathematics is starting with set-theoretic axioms and then defining everything in terms of sets.
k_bx 3 hours ago
"Usual", "most common by far" etc. are all great phrases, but not "all of mathematics", esp when we talk about math related to computer science
umanwizard 3 hours ago
Math related to CS is typically formalized starting with set theory, just like other branches of math.
A_D_E_P_T 2 hours ago
What's important to note is that this is just a matter of convention. An historical accident. It is by no means a law of nature that math need be formalized with ZFC or any other set theory derivative, and there are usually other options.

As a matter of fact, ZFC fits CS quite poorly.

In ZFC, everything is a set. The number 2 is a set. A function is a set of ordered pairs. An ordered pair is a set of sets.

In ZFC: It is a valid mathematical question to ask, "Is the number 3 an element of the number 5?" (In the standard definition of ordinals, the answer is yes).

In CS: This is a "type error." A programmer necessarily thinks of an integer as distinct from a string or a list. Asking if an integer is "inside" another integer is nonsense in the context of writing software.

For a computer scientist, Type Theory is a much more natural foundation than Set Theory. Type Theory enforces boundaries between different kinds of objects, just like a compiler does.

But, in any case, that ZFC is "typical" is an accident of history, and whether or not it's appropriate at all is debatable.

jltsiren 1 hour ago
In CS, types are usually a higher level of abstraction built on top of more fundamental layers. If you choose to break the abstraction, you can definitely use an integer as a string, a list, or a function. The outcome is unlikely to be useful, unless your construct was designed with such hacks in mind.

When I did a PhD in theoretical computer science, type theory felt like one niche topic among many. It was certainly of interest to some subfield, but most people didn't find it particularly relevant to the kind of TCS they were doing.

umanwizard 1 hour ago
Sure, but it fits the rest of mathematics "poorly" for exactly the same reasons. No working mathematician is thinking about 3 as an element of 5.

The reason ZFC is used isn't because it's a particularly pedagogical way of describing any branch of math (whether CS or otherwise), but because the axioms are elegantly minimal and parsimonious.

nathias 3 hours ago
the empirical modern mathematics are build on set theory, type and category theory are just other possible foundations
A_D_E_P_T 2 hours ago
Most modern mathematicians are not set theorists. There are certain specialists in metamathematics and the foundations of mathematics who hold that set theory is the proper foundation -- thus that most mathematical structures are rooted in set theory, and can be expressed as extensions of set theory -- but this is by no means a unanimous view! It's quite new, and quite heavily contested.