# 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? Feb 15, 2017 at 1:29
• This is related, I think.
– user228113
Feb 15, 2017 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). Feb 15, 2017 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. Feb 15, 2017 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. Feb 15, 2017 at 1:50

• @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. Feb 15, 2017 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.) Feb 15, 2017 at 17:17