Remix.run Logo
A new bridge links the math of infinity to computer science(quantamagazine.org)
82 points by digital55 3 hours ago | 12 comments
shevy-java 21 minutes ago | parent | next [-]

Finally - we can calculate infinity.

Been a long way towards it. \o/

anthk 5 minutes ago | parent | prev | next [-]

It's cons'es all the way down.

k_bx an hour ago | parent | prev [-]

> 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 22 minutes ago | parent | next [-]

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

rdlw an hour ago | parent | prev | next [-]

Is there a collection of type theory axioms anywhere near as influential as ZF or ZFC?

k_bx an hour ago | parent [-]

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.

umanwizard an hour ago | parent | prev | next [-]

"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 an hour ago | parent [-]

"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 an hour ago | parent [-]

Math related to CS is typically formalized starting with set theory, just like other branches of math.

A_D_E_P_T 3 minutes ago | parent [-]

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.

nathias an hour ago | parent | prev [-]

the empirical modern mathematics are build on set theory, type and category theory are just other possible foundations

A_D_E_P_T 34 minutes ago | parent [-]

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.