We’ve done an enormous amount of work to make mainstream mathematics work the way it currently works. We have sets which are infinite, but individual elements are not. In other words, you have an infinite set of numbers, but no number is itself infinite. Only after centuries of effort did we make this work rigorously.
I think it’s worth remembering this, when we think about alternative foundations for mathematics. What if we discard the axiom of infinity? What if we discard the axiom of choice? Axiom of regularity? Each of these decisions leads us to a path which may be as fruitful as current mainstream mathematics, but which relatively unexplored. Or you could stick with existing formulations, and rework how you do calculus.
To pick on the calculus example—mainstream calculus defines continuity using limits, which are defined by formulas quantified over infinite sets. What happens if, instead of using infinite sets, you use sets that contain infinite numbers? Voilà, you have nonstandard analysis… the “dx” and “dy” can now be actual infinitesimal numbers. Is this easier for students to understand? Or is it confusing? Does it formalize existing intuition about infinitesimals, and let you do things like treat dy/dx as an actual division?
Same is true in the opposite direction. What if you have no infinite sets, no infinite numbers? How do you do calculus? What theorems still work, which don’t?
The theorems that don’t work—do we miss them when they are gone?
We actually know a fair bit about what happens if you discard the axiom of choice; mostly because Banach-Tarski made it so controversial.
As for calculus, it doesn't require the existence of infinities or infinitesimals. Set theory needs to care about infinities and the sizes thereof because they are creatures of the axioms they adopt. But in calculus "infinity" just means "it gets as big as you want" and "infintesimal" just means "it gets as small as you want". Everything's argued on top of limits that are done in the real number system where there aren't any infinities or infinitesimals.
The thing that calculus really cares about is continuity: i.e. the idea that if you nudge the input to a function a little bit, the output changes by a little bit. If you try to do calculus on functions that don't work this way, then calculus doesn't work, either.
> We actually know a fair bit about what happens if you discard the axiom of choice; mostly because Banach-Tarski made it so controversial.
Do you have any more information about this? Is there an overview somewhere? The major work I know in this area is Reverse Mathematics, but I otherwise thought it was relatively unexplored. Emphasis on “relatively”.
My impression here is that Banach-Tarski reveals “flaws” not just in ZFC but in ZF, and that while we may want to reevaluate the axiom of choice, we should be looking at the rest of ZF as well.
> As for calculus, it doesn't require the existence of infinities or infinitesimals.
The question was never “can you do calculus?” but “HOW do you do calculus?” Maybe I should clarify what I originally said and elaborate. Forgive me for imprecise wording here, and forgive me for being too verbose, I’m trying to get across a specific point and I’ll be stomping across some flower gardens to get there.
The current, mainstream form of calculus is based on real analysis and measure theory, which in turn, makes heavy use of infinite sets, excluded middle, and the axiom of choice. When I say that calculus is “based on” real analysis, what I really mean is that calculus was invented, and then later, people invented real analysis to provide a rigorous framework for doing calculus with real numbers.
I might ask, “What are the most important theorems in calculus?” The second theorem which comes to mind is the Bolzano-Weierstrass theorem, which involves infinite sequences and is the foundation for many other core results in calculus. Real numbers are themselves typically defined in terms of infinity—either as Dedekind cuts (infinite sets) or Cauchy sequences (infinite sequences). You don’t have to do calculus on real numbers, but real numbers are surely a very convenient tool for the kind of calculus we want to do, and some of the most important properties of real numbers have backed us into a corner w.r.t. how real numbers are constructed—namely, constructions satisfying “complete ordered Archimedean field”.
If you decide that you still want to do calculus but you don’t want to do real analysis, the most popular alternative is nonstandard analysis, which has actual infinitesimal numbers. The main advantage of nonstandard analysis is that it provides a rigorous framework for manipulating infinitesimals, which may perhaps be more intuitive that working with differential forms. With nonstandard analysis, you can eliminate limits from a lot of your definitions, because you can use actual infinitesimal numbers instead. At that point, you’re working with non-Archimedean fields.
So, to summarize, two likely candidates for the foundations of calculus are:
- Real analysis, with heavy use of infinite sets,
- Nonstandard analysis, with infinitesimal numbers.
I ask, HOW do you do calculus without either? What does the field of calculus look like without either? When you are doing calculus in a strict finitist world, what definition do you come up with for “real number”?
I never dove all the way into this, but I always found one detail unsatisfying: the natural numbers as defined by Peano arithmetic, and more generally the kind of sets described in the OP, are sets all the way down. Each element is itself a set consisting, recursively, of sets. The system has no types!
But Cauchy sequences, and limit sequences, aren’t sets all the way down, nor are they things that grew out of untyped lambda calculus. They are sequences, not sets. And their elements are real numbers, not sets.
Sure, a real number may well be describable as itself being a Dedekind cut over the rational numbers, which are themselves describable using Peano arithmetic. But you can do calculus using the axioms of the real numbers and treat the real numbers as their own type of object. The result seems much cleaner to me - a real number is equivalent to a Dedekind cut, but this does not mean that a real number is a Dedekind cut. A set of reals is not sets all the way down. An object of type Integer in most programming languages is not implicitly convertible to Set. Putting types into a model of mathematics seems to add a very welcome firewall between algebraic structures (like the reals) and the underlying formalism that was used to justify their existence and properties.
In this context, of course infinite sets exist. The set of distinct real numbers in a sequence of reals converging to given irrational number is (countably) infinite. This infinity is firewalled off from the axiom of infinity, and it is infinite all by itself, which is amazing because I can take a limit or calculate a derivative without thinking about ZF at all!
(The problems in the world are not all solved like this. Calculus certainly involves measures, and the Banach-Tarski paradox works on sets of reals, etc. But I don’t have to worry about Banach-Tarski when integrating a function.)
I get what you are trying to say here. If we were talking only about calculus, it would be a reasonable thing to say. In this context, we are talking about calculus in connection with its set theory foundations, and so this statement, in context, is simply incorrect.
Imagine I dropped a tomato on the floor and called you in to help me clean up a “chemical spill”. You’d say that’s not a chemical spill, that’s a tomato. On any other day of the year you would be correct, but today we are in chemistry class, talking about how ordinary matter is made of chemicals. Today you are wrong, because we are in chemistry class, talking about what tomatoes are made of.
> Putting types into a model of mathematics seems to add a very welcome firewall between algebraic structures (like the reals) and the underlying formalism that was used to justify their existence and properties.
The firewall only works if the underlying structure is sound. People have, historically, spent enormous amounts of time working with mathematical objects that turned out to be trivial, turned out not to exist at all, or had contradictions. For that reason, real mathematicians spend some time fussing about proving that the real numbers exist using set theory, before they turn around and work with exactly that firewall that you’re discussing. In upper-level undergrad courses, you’ll be expected to do this. (At least, I was asked to do this in undergrad.)
Again, today, the topic of discussion is the axiom of infinity. If I ask, “how would we do calculus without infinite sets,” we need to revisit the set-theoretic construction of real numbers and calculus before we can put that firewall back into place.
> But I don’t have to worry about Banach-Tarski when integrating a function.
Unfortunately, the Banach-Tarski paradox is exactly the kind of paradox you must worry about when integrating functions. In a loose sense, what the paradox shows is that you cannot cut up a function you want to integrate, rearrange the pieces, and then integrate the result.
For a long time, mathematicians had all sorts of incorrect beliefs about calculus. For example, “a continuos function defined on an open interval is differentiable at some point on the interval”. These incorrect beliefs didn’t disappear overnight. We created a rigorous foundation for calculus on a carefully-crafted list of set theory axioms (ZFC) and slowly rooted out the incorrect beliefs with proofs and counterexamples.
It’s worth asking whether ZFC is the foundation we want for calculus. Maybe it’s time to adjust the foundations. Maybe you think—what if I had a version of calculus that didn’t have non-measurable sets? Working backwards from that idea, what axioms would I need in order to still get work done?
As long as the mathematics you do within your chosen set of axioms is internally consistent you are doing “real” mathematics.
And different choices of axioms and logics will give you different flavours of mathematics. That may or may not be beautiful or elegant or useful according to your specific tastes and needs.
It just happens to be the case that the Axiom of Infinity has been a popular choice among mathematicians. While computer scientists working within type theory and proof theory usually prefer to use mathematics based on a different axiomatic foundations than what a typical career mathematician would choose to be successful in getting jobs/grants etc.
However it is all “real” mathematics. Just different branches off the same tree.
I'm generally aligned with constructivism and intuitionism, but I don't quite get finitism. To me it seems that even without this axiom, it's clear that there are infinite objects in the sense of an unbounded set.
Practically speaking, what results obtained with the Axiom of Infinity cannot be achieved without it?
Thank you, that seems really interesting, and it touches tantalizingly onto some ideas I've wondered if anyone has formalized.
There's the old joke that
1. Not all numbers are interesting
2. If not all numbers are interesting, then there's a smallest number that's not interesting
3. But that's interesting in itself! Ha! Contradiction!
But it seems to me all you need to resolve that contradiction is to be a bit tough and say that no, it being the smallest boring number isn't interesting. Who cares.
What I would like to know is if there is a formalization of "we don't care about that". Obviously we use the idea sometimes (Karnaugh maps come to mind).
Well, you can't create the infinite set of all natural numbers without the Axiom of Infinity. You can still reason about natural numbers themselves without the Axiom of Infinity (and if you are inclined to speak in such terms, the natural numbers will still comprise a "class", just a proper class rather than a set, when the Axiom of Infinity is negated).
ZF(C) with the Axiom of Infinity replaced by its negation is essentially equivalent to Peano Arithmetic, and you can do an awful lot of math just fine in Peano Arithmetic.
You can't create the set of natural numbers even with the axiom of infinity either, at least not in any first order logic. No first order logic is sufficient to strictly define the set of all natural numbers.
You can technically construct natural numbers in second order logic, at least syntactically, but then the semantics of natural numbers in second order logic does not end up corresponding to what is actually meant by natural numbers.
> You can't create the set of natural numbers even with the axiom of infinity either, at least not in any first order logic. No first order logic is sufficient to strictly define the set of all natural numbers.
Eh that's a fundamentally different problem though, although that is part of the reason why finitism and ultra-finitism are attractive.
You can define a set that is the natural numbers for all intents and purposes from the viewpoint of your theory. If you were willing accept that something like PA is enough to do large parts of real analysis (and also believed in the usefulness of real analysis), then philosophically you should be totally fine with using theories that have models with nonstandard natural numbers, since "you can't observe any of the consequences from your theory" is the same bar in both cases (in the case of finitistic approaches to analysis it's even trickier because often you can only deal with encodings of objects rather than objects themselves and must rely on your metatheory to do the association of the encoding to the object).
I don't agree it's a different problem, as OP pointed out, ZF with the axiom of infinity replaced by its negation is equal to first order Peano Arithmetic, sometimes referred to as the theory of hereditarily finite sets.
Said theory is also sufficient for all intents and purposes of doing real analysis.
> I don't agree it's a different problem, as OP pointed out, ZF with the axiom of infinity replaced by its negation is equal to first order Peano Arithmetic, sometimes referred to as the theory of hereditarily finite sets.
Being unable to talk about the set of natural numbers except through encodings (which is how you do infinitary math without infinity) is different than having a symbol for the set of natural numbers which may or may not have additional properties which cannot be discerned within the theory itself (e.g. Lowenheim-Skolem).
> Said theory is also sufficient for all intents and purposes of doing real analysis.
Large chunks of real analysis can indeed be carried out, but significant amounts cannot. Many theorems in analysis concerning perfect sets are not provable in that theory (usually stated as ACA0).
> Notice here, we are just treating the natural numbers as a class, not necessarily a set. In fact we can prove from ZF minus infinity that any of the (translations of the) axioms of PA, including all the induction axioms, hold in this class.
I need more elucidation on that. Why can't you use the natural numbers? You can construct them even within the constraints of ZF. Is it just that you can't use it the same way as a set in all cases? It seems like you could define a new class, call them seits, that include both the set as axiomatically defined as well as these sorts of unbounded objects, and then prove that you can define similar operations as exist for sets on seits, and then go on and live your life.
When you say you can't "use" anything infinite, what's an example of a theorem that cannot be proven without the Axiom of Infinity?
Because the rest of the axioms of ZF aren't sufficient to construct them.
> what's an example of a theorem that cannot be proven without the Axiom of Infinity?
That there exists a set equal to the natural numbers up to isomorphism, that there exist well-defined operations "+", "-", "*", "/" with usual semantics, that there exist the usual sets of rational, real, complex numbers.
You can construct any natural number without the axiom of infinity, but you cannot construct the set of natural numbers itself.
> It seems like you could define a new class, call them seits, that include both the set as axiomatically defined as well as these sorts of unbounded objects, and then prove that you can define similar operations as exist for sets on seits, and then go on and live your life.
Imagine you’re at a vegan restaurant. Your food arrives, you pull a fistful of ground beef out of your pocket and stick it on top. You’re “still eating vegan food”, you’ve just added beef to it.
Finitism is a lot like a dietary restriction. It’s asking “What can you do WITHOUT these axioms?” The question is whether you still have a balanced diet afterwards, whether you’re satisfied, whether you prefer a vegan or omnivorous diet, etc. If you add infinities to your finite sets but call them classes instead you’re just cheating on your diet. (Or you’re talking about models of finitism.)
I suspect that there are a ton of results that can’t be proven without the axiom of infinity, but I don’t keep track of them.
Not a mathematician, but can't you parameterize e.g. the natural numbers by its largest element, then write whatever you want to do with the set and put lim n->inf around it? That way, you keep the objects finite, but you still allow them to become arbitrarily large.
Define lim without infinite sets. Define how you quantify over all values of n without infinite sets. The parameterization you describe would be a function mapping an infinite set of sets of natural numbers to their maximum elements, that function itself being (or containing) an infinite set of ordered pairs.
You might be able to pull it off without creating something equivalent to the axiom of infinity — I wouldn’t know if it’s possible. But the naïve implementation of your ideas involves the construction of infinite sets.
I think you can do this rigorously outside the theory, talking about it, but not inside.
One construction of the natural numbers that I've seen is
1. There exists an element 0 that is a natural number
2. For every natural number there is a "sucessor" that is also a natural number. (i.e. if n is a natural number then n+1 is a natural number)
This construction means there can't be an upper bound N because then step 2 couldn't be applied to N.
Maybe there are other constructions that could workaround this? I'm guessing not because you'd still struggle to define the usual rules of addition for all numbers in a bounded set
> This construction means there can't be an upper bound N because then step 2 couldn't be applied to N.
Bendegem discusses this problem at length in his paper [1]. As programming-heavy site, I assume we're all aware that computers have finite resources. The universe too has finite resources so no matter how big a computer you build, it too will be finite. Therefore the infinity that is so pervasive in math is unphysical in a very real sense. So what would math look like and how would theorems change if this finiteness were formalized? That's what various flavours of finitism aim to achieve.
So to get back to your question as to the nature of the naturals, it seems evident that yes, at some point, you literally can fail construct the natural number N+1 if you are given N, because you will run out of particles in the universe. What implications this will have for various theorems will be interesting for sure, but it isn't clear yet because finitism isn't given much funding.
Edit: however, it's clear that some very unintuitive results follow from the infinities embedded in mathematics, and that a finitist approach resolves some of them. For instance, the argument that "0.9999... = 1" is true in classical mathematics while this equality is arguably not true under strict finitism because "0.999..." does not exist, because infinite objects do not exist, and so it will never equal 1.
Calling “0.999… = 1” very unintuitive is a very strange thing to say, because that makes perfect sense to most children. I’d like to see a result that truly is unintuitive, like what we get with the axiom of choice.
I remember being a kid and having this discussion in elementary school. Kids have enough intuition to know that operations with fractions should get the same result as with decimal numbers. Or that 1-0.999… = 0.000…. Or that different lengths have a length in between them. All are legitimate and compelling arguments.
I think lots of students get lost with different orders of infinity (countable, uncountable, etc.), so I think there is definitely a point beyond which you can't push the intuition behind infinite objects.
> Practically speaking, what results obtained with the Axiom of Infinity cannot be achieved without it?
There's a surprising amount you can achieve without the Axiom of Infinity, but the way you have to "talk" about things gets very awkward very quickly.
First off, what you end up with at the end of the day if you take the negation of the Axiom of Infinity but keep the rest of ZF (this is also known as the theory of hereditarily finite sets, i.e. finite sets whose members must also be finite sets all the way down) are the (first-order) Peano Axioms. To explain an intuition for why in a very hand-wavy sense, if you only have finite sets, you can encode any finite set as a single natural number and vice versa .As witness of this in programming, note that that an array ultimately is a single binary number consisting of 0s and 1s and likewise a single natural number ultimately is just a single binary number consisting of 0s and 1s. To also very hand-wavingly describe why the Peano Axioms are in fact excluding the notion of infinity, note that the Peano Axioms have no way to talk about the natural numbers as a single entity, only a way of talking about each individual number.
So to answer your question directly, any theorem about the natural numbers that cannot be proved with the Peano Axioms cannot be proved without the Axiom of Infinity in ZF. For example, the Paris-Harrington Theorem cannot be proved without the Axiom of Infinity in ZF. These are potentially philosophically interesting examples since they are theorems about finite numbers that cannot be proved without the Axiom of Infinity (although the ultrafinitist would object to the careless use of "for all natural numbers" that shows up in these statements).
On the flip side, a surprising amount of theorems ostensibly about infinite structures can be proved purely with Peano Arithmetic alone. Let's talk about the real numbers for example. The general trick is that while you obviously cannot talk directly about a "real number," you can talk about all the finite structures which approximate a real number and their finite consequences. So instead of saying statements of the form "there exists a real number r such that X" you end up saying "for all natural numbers n, there exists another natural number m_n with property A such that each number satisfies X'" where n forms the indices of a series of approximations m_n whose property A ensures that they are correctly approximating r and X' is the property X translated to be a property on each individual approximation.
Now I personally find this a very awkward way to talk about the real numbers. In particular the theory itself cannot recognize that it's trying to approximate something, as the theory has no concept of that "something." Only you as an external observer can look at the theory and "realize" that a given theorem is "really" talking about the real numbers. Within the theory it just looks like you're proving really weird things about really weird sequences.
But with this in hand you can prove some parts of analysis, but not others. E.g. the validity of using the ratio test from calculus cannot be proven even within this framework.
You can't prove the validity of the ratio test for all sequences of real numbers, because you can't talk about all sequences of real numbers. But you could at least prove the validity of the ratio test for any computably enumerable sequence of computable real numbers, or such things. You could carry out the full argument of the ratio test, except for the tiny part at the beginning where it says "Let us quantify over the set of all sequences of reals...".
> But you could at least prove the validity of the ratio test for any computably enumerable sequence of computable real numbers, or such things. You could carry out the full argument of the ratio test, except for the tiny part at the beginning where it says "Let us quantify over the set of all sequences of reals...".
I don't actually think so. I'd have to retrace the arguments again, but I believe the ratio test is beyond ACA0 which puts it beyond PA and therefore impossible to prove in a much more fundamental way than just the inability to quantify over the reals. (also, as I'm sure you know, but for the benefit of other readers, you can "morally" quantify over the reals in the same manner I described for "moral" existential quantification of a real, but even with that trick, I don't believe you can prove the transformed version of the ratio test).
How could the ratio test possibly be beyond ACA0? The ratio test is just a straightforward special case of the comparison test.
For convenience, let us suppose we are dealing with series of positive terms (since the ratio test is about magnitudes and absolute convergence anyway). Given a series S with limiting value L for ratio of terms to previous terms, and considering a geometric series G for which the same ratio is any value strictly between L and 1, then when L < 1, we have that S is eventually upper-bounded by G and G is convergent, while for L > 1, we have that S is eventually lower-bounded by G and G is divergent.
I have no idea why I wrote ACA0. I was totally wrong (ACA0 is enough for Dedekind-completeness...).
But the ratio test is actually subtly difficult.
> But you could at least prove the validity of the ratio test for any computably enumerable sequence of computable real numbers, or such things.
This still actually isn't quite true, the emphasis on "computable" being essential here. In particular the ratio test is (unless I've yet again made a catastrophic mistake) not provable in RCA0. The tricky problem with your proof sketch is the word "eventually." In general you can't find the N that validates your usage of the word "eventually" in a computable fashion.
This is fundamentally different than superficially similar tests such as the alternating series test because those don't lean on "eventually" in the same way.
So the ratio test is actually still uniquely difficult for (computable) finitism.
RCA_0 is a much stronger restriction than just negating the Axiom of Infinity, though. Your original post claimed the ratio test could not be proven in Peano Arithmetic, which was what I objected to. Peano Arithmetic is basically equivalent in strength to ACA_0.
I think it’s worth remembering this, when we think about alternative foundations for mathematics. What if we discard the axiom of infinity? What if we discard the axiom of choice? Axiom of regularity? Each of these decisions leads us to a path which may be as fruitful as current mainstream mathematics, but which relatively unexplored. Or you could stick with existing formulations, and rework how you do calculus.
To pick on the calculus example—mainstream calculus defines continuity using limits, which are defined by formulas quantified over infinite sets. What happens if, instead of using infinite sets, you use sets that contain infinite numbers? Voilà, you have nonstandard analysis… the “dx” and “dy” can now be actual infinitesimal numbers. Is this easier for students to understand? Or is it confusing? Does it formalize existing intuition about infinitesimals, and let you do things like treat dy/dx as an actual division?
Same is true in the opposite direction. What if you have no infinite sets, no infinite numbers? How do you do calculus? What theorems still work, which don’t?
The theorems that don’t work—do we miss them when they are gone?