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

• @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