# How much of calculus can we formalize without infinity?

How much of calculus can we formalize in ZF-AoI? Can we formulate the basics of derivatives, integrals and their nice properties or do we lose some of those?

Also does choice make sense if we exclude the Axiom of Infinity? I heard somewhere that finite choice is implied by ZF but would a weaker version of choice (countable choice) be necessary?

• How do you formulate real numbers without naturals? – mniip Feb 15 '17 at 1:29
• This is related, I think. – user228113 Feb 15 '17 at 1:33
• @mniip you don't need the axiom of infinity to define the naturals. I believe you can do it with just the axiom of extensionality and axiom of regularity. And the rationals can be defined without infinity as well. Not having the axiom of infinity is different from insisting that everything is finite (for whatever that actually means without infinity). – lordoftheshadows Feb 15 '17 at 1:38
• @G.Sassatelli thanks. I think that is what I was looking for. Although I'm having a bit of trouble parsing it. – lordoftheshadows Feb 15 '17 at 1:42
• Mathematica can do calculus even though it is run on a finite state machine. The proof that the Mathematica algorithm yields the correct outcome, even if the input is a calculus problem, can always be reduced to a discrete math problem. – Count Iblis Feb 15 '17 at 1:50

## 1 Answer

You lose surprisingly little. ZF with the axiom of infinity replaced by its negation turns out to be the set of hereditarily finite sets and you can still do calculus perfectly well.

On choice, if you simply remove the axiom, there is no hope of proving anything more than you could without it. But if you add the negation, then Ackermann's bijection provides a choice function. That said, I don't know whether it can be proven to be a well-defined choice function from within that axiom system. I suspect not.

Of more historic and philosophical interest is removing the law of the excluded middle. This gives you Constructivism. It turns out that you can still construct the real numbers, do calculus, and so on. However you get odd consequences such as numbers not always being comparable and all well-defined functions having to be continuous.

• I've run across constructivism but no matter how I try I just don't get it. I can prove things in it but I have absolutely no intuition for it. What would be the negation of choice? Would it be the negation of choice in the infinite case? Doesn't finite choice follow from ZF? – lordoftheshadows Feb 15 '17 at 2:13
• @lordoftheshadows Finite choice follows from ZF. But if you remove the axiom of infinity then the integers are not a set for the same reason that the ordinals can't be a set in ZF. And therefore a "function" from them isn't really a function. – btilly Feb 15 '17 at 17:04
• @lordoftheshadows As for constructivism, you can think of it like this. The only things that exist are ones that you can construct. And the only things that are true are ones that you have proofs for. So, for example, instead of talking about Cauchy sequences of rationals, you might talk about a computer program that takes an integer $n$ and produces a rational $r_n$ such that if $n < m$ then $|n-m| < \frac{1}{n}$. If you can't write down the computer program and prove that it fits the definition, it doesn't represent a real number. – btilly Feb 15 '17 at 17:12
• In this framework, talking about the axiom of choice is meaningless. Heck, it may be an open question whether 2 programs represent the same real number! (For example we can construct a sequence which converges to $0$ if the Riemann hypothesis is true, or $(-0.5)^n$ if it is not with $n$ being the first nontrivial zero with real part not $0.5$. Perfectly well-defined constructive real, but from our present knowledge it is not less than, equal to, or greater than 0.) – btilly Feb 15 '17 at 17:17