are there any current or foreseeable practical applications of those results?

the math of infinity isn't very relevant to the finite programs that humans use. Even today's astronomically large computing systems have size approximately equal to 3 compared to infinity.

> but cannot prove more theorems

usually you're more interested in better ergonomics: can you do X with less work?

it's like picking a programming language - depending on what you're attempting, some will be more helpful.

and ZFC is a lot more low level than what day-to-day mathematics usually bothers with. So most mathematians actually work in an informally understood higher-order wrapper, hoping that what they write sufficiently explains the actual "machine code"

the idea then behind adopting alternative foundations is that these come with "batteries included" and map more directly to the domain language.

Isabelle/HOL is still types. The underlying type theory of Isabelle/HOL is not theory of dependent types, but theory of simple types. Isabelle/ZF would be a better example as it encodes Zermelo–Fraenkel set theory.

It’s not really. It leads to paradoxes. There are alternative formulations which avoid these.

I think at this stage, most mathematicians recognize that formal proof verification is a real and interesting thing. We have extremely prominent mathematicians like Scholze & Tao making a point of using these tools.

But in many cases, it's extra effort for not much reward. The patterns which most mathemematicians are interested in are (generally) independent of the particular foundations used to realize them. Whether one invests the effort into formal verification depends on how hard the argument is and how crucial the theorem.

Took me an embarrassingly long time to realize you're talking about a music event not a math lecture

If you wanted to dive in, here is a Jazz version of one of their singles. The real version is 2 guitars, 1 bass, 1 drums, and someone screaming into the microphone -- its real rad.

https://www.youtube.com/watch?v=D4-erceTpc8

∞/1 + 1/∞

One infinitesimal step for the numerical, one giant step for mathkind.

Come on, now you know better than that. It was infinity that counted to Chuck Norris

I agree with our assessment of Quanta. I used to enjoy reading their articles, but the clickbait title formula has put me off. Also their status as a mouthpiece of the Simons foundation grantees.

I feel like I’m being a bit curmudgeonly, but I don’t read them much any more.

What? You can find tons of textbook examples when dealing with the uncountable sets from non-deterministic finite automata. Those frequently deal with power sets (like when you have an infinite alphabet) which are quintessentially uncountable

Asymptotics is a good example of CS using infinity practically.

Also, a small aside: there’s a finite amount of matter in the visible universe. We could have infinite matter in an infinite universe.

> There is no infinity at the end of a number line. There is a process that says how to extend that number line ever further.

Sure, but ordinal numbers exist and are useful. It's impossible to prove Goodstein's theorem without them.

https://en.wikipedia.org/wiki/Ordinal_number

https://en.wikipedia.org/wiki/Goodstein%27s_theorem

The statement and proof of the theorem are quite accessible and eye-opening. I think the number line with ordinals is way cooler than the one without them.

Whether you think infinity exists or not is up to you, but transfinite mathematics is very useful, it's used to prove theorems like Goodstein's sequence in a surprisingly elegant way. This sequence doesn't really have anything to do with infinity as first glance.

Actually, all numbers are functions in Peano arithmetic. :)

For example, S(0) is 1, S(S(0)) is 2, S(S(S(0))) is 3, and so on.

There is no end of a number line. There are lines, and line segments. Only line segments are finite.

> There is no infinity'th prime number. There is a process by which you can show that a bigger primer number must always exist.

You misunderstand the concept of infinity. Cantor's diagonal argument proves that such a bigger number must always exist. "Infinity'th" is not a place in a number line; Infinity is a set that may be countable or uncountable, depending on what kind of infinity you're working with.

There are infinities with higher cardinality than others. Infinity relates to set theory, and if you try to simply imagine it as a "position" in a line of real numbers, you'll understandably have an inconsistent mental model.

I highly recommend checking out Cantor's diagonal argument. Mathematicians didn't invent infinity as a curiosity; it solves real problems and implies real constraints. https://en.wikipedia.org/wiki/Cantor's_diagonal_argument

It turns out rather ok without actual infinity, by limiting oneself to potential infinity. Think a Turing Machine where every time it reaches the end of its tape, an operator ("tape ape") will come and put in another reel.

7, if the Extremely Strong Goldbach Conjecture holds. [1]

[1] https://xkcd.com/1310/

I don't think this is a good description of mathematicians using infinite objects. It typically doesn't involving something being given the label "infinity". That's used in like, taking limits and such, but there it is just a notation.

When mathematicians are working with infinite objects, it is not by plugging in "infinity" somewhere a number should go, in order to imagine that the rule that would construct an object if that were a number, constructs an object. No. Rather, (in a ZF-like foundations) the axiom of infinity assumes that there is a set whose elements are exactly the finite ordinals. (Or, assumes something equivalent to that.) From this, various sets are constructed such that the set is e.g. in bijection with a proper subset of itself (there are a handful of different definitions of a set being "infinite", which under the axiom of choice, are equivalent, but without AoC there are a few different senses of a set being "infinite", which is why I say "e.g.").

In various contexts in mathematics, there are properties relevant to that specific context which correspond to this notion, and which are therefore also given the name "infinite". For example, in the context of von Neumann algebras, a projection is called a "finite projection" if there is no strict subprojection that is Morray-von Neumann equivalent to it. Or, in the context of ordered fields, an element may be called "infinite" if it is greater than every natural number.

Usually, the thing that is said is that some object is "infinite", with "infinite" an adjective, not saying that some object "is infinity" with "infinity" a noun. One exception I can think of is in the context of the Surreal Numbers, in which the Gap between finite Surreal Numbers and (positive) infinite Surreal Numbers, is given the name "infinity". But usually objects are not given the name "infinity", except as like, a label for an index, but this is just a label.

I suppose that in the Riemann sphere, and other one-point compactifications, one calls the added point "the point at infinity". But, this kind of construction isn't more "make believe" than other things; one can do the same "add in a point at infinity" for finite fields, as in, one can take the projective line for a finite field, which adds a point that is doing the same thing as the "point at infinity" in the complex projective line (i.e. the Riemann sphere).

A triangle exists in physics.

A ZFC variant without infinity is basically just PA. (Because you can encode finite sets as natural numbers.) Which in practice is plenty enough to do a whole lot of interesting mathematics. OTOH by the same token, the axiom of infinity is genuinely of interest even in pure finitary terms, because it may provide much simpler proofs of at least some statements that can then be asserted to also be valid in a finitary context due to known conservation results.

In a way, the axiom of infinity seems to behave much like other axioms that assert the existence of even larger mathematical "universes": it's worth being aware of what parts of a mathematical development are inherently dependent on it as an assumption, which is ultimately a question of so-called reverse mathematics.

There are a couple philosophies in that vein, like finitism or constructivism. Not exactly mainstream but they’ve proven more than you’d expect

https://en.wikipedia.org/wiki/Finitism

https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_...

There’s tons of variants of ZFC without the “infinity”. Constructivism has a long and deep history in mathematics and it’s probably going to become dominant in the future.

Why is it that when I have a stack of business cards, each with a picture of a different finger on my left hand, then when I arrange them in a grid, there’s only one way to do it, but when I instead have each have a picture of either a different finger from either of my left or right hand, there is now two different arrangements of the cards in a grid?

I claim the reason is that 5 is prime, while 10 is composite (10 = 5 times 2).

Therefore, 5 and 10, and 2, exist.

Wouldn't it follow that those "things" we're pointing to aren't really "things" because they're all leaking and fuzzy? Begging the question, what ends up on a list of things that do exist?

Me neither. David Deutsch had some interesting thoughts on why finitists are wrong in TBOI but I never fully understood it.

Math is a tool for structured reasoning. We often want to reason about things that physically exist. Why should we use a tool that assumes the existence of something that literally cannot physically exist? That introduces the danger that of admitting all sorts of unphysical possibilities into our theories.

I think Baez's paper, Struggles with the Continuum, shows a lot of past difficulties we've had that resulted from this:

https://arxiv.org/abs/1609.01421

To echo the sibling comment, that answer is specifically referring to the type theory behind Lean (which I’ve heard is pretty weird in a lot of ways, albeit usually in service of usability). Many type theories are weaker than ZFC, or even ZF, at least if I correctly skimmed https://proofassistants.stackexchange.com/a/1210/7.

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.

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.

"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

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.

There is a world of difference between the obvious and the trivial. The post you are replying to only implied it was obvious, the retort is unnecessary.

Why? Both are basically about how to handle information with a priori indefinitely many cases, types, instances, species

Is it?

The notion of algorithms and computer science were invented to discuss the behavior of infinite sequences: examining if there’s descriptions of real numbers. This was extended by connecting complicated infinite structures like the hyperreals with decisions theory problems.

That descriptions of other infinite sets also corresponds to some kind of algorithm seems like a natural progression.

That it happens to be network theory algorithms rather than (eg) decision theory algorithms is worth noting — but hardly surprising. Particularly because the sets examined arose from graph problems, ie, a network.

The Löwenheim-Skolem theorem implies that a countable model of set theory has to exist. "Cardinality" as implied by Cantor's diagonal argument (which happens to be a straightforward special case of Lawvere's fixed point theorem) is thus not an absolute property: it's relative to a particular model. It's internally true that there is no bijection as defined within the model between the naturals and the reals, as shown by Cantor's argument; but externally there are models where all sets can nonetheless be seen as countable.

I just gave the reason - The notion of comparison and 1-to-1 mapping has an underlying assumption about the subjects being quantifiable and identifiable. This assumption doesn't apply to something inherently neither quantifiable nor is a cut in the continuum, similar to a number. What argument are you offering against this?

You can't enumerate the real numbers, but you can grab them all in one go - just draw a line!

The more I learn about this stuff, the more I come to understand how the quantitative difference between cardinalities is a red herring (e.g. CH independent from ZFC). It's the qualitative difference between these two sets that matter. The real numbers are richer, denser, smoother, etc. than the natural numbers, and those are the qualities we care about.

That doesn't make one set "larger" than the other. You need to define "larger". And you need to make that definition as weird as needed to justify that comparison.

.. because that is where you are allowed to challenge some biblical stories of the math without the fear of expulsion from the elite clubs.

Most of math history is stellar, studded with great works of geniuses, but some results were sanctified and prohibited for questioning due to various forces that were active during the times.

Application of regular logic such as comparison, mapping, listing, diagonals, uniqueness - all are the rules that were bred in the realms of finiteness and physical world. You can't use these things to prove some theories about things are not finite.