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?

  • 2
    $\begingroup$ How do you formulate real numbers without naturals? $\endgroup$
    – mniip
    Feb 15, 2017 at 1:29
  • $\begingroup$ This is related, I think. $\endgroup$
    – user228113
    Feb 15, 2017 at 1:33
  • $\begingroup$ @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). $\endgroup$
    – Zaros
    Feb 15, 2017 at 1:38
  • $\begingroup$ @G.Sassatelli thanks. I think that is what I was looking for. Although I'm having a bit of trouble parsing it. $\endgroup$
    – Zaros
    Feb 15, 2017 at 1:42
  • $\begingroup$ 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. $\endgroup$ Feb 15, 2017 at 1:50

1 Answer 1


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.

See If all sets were finite, how could the real numbers be defined? for more. See also https://en.wikipedia.org/wiki/Hereditarily_finite_set.

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.

  • $\begingroup$ 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? $\endgroup$
    – Zaros
    Feb 15, 2017 at 2:13
  • $\begingroup$ @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. $\endgroup$
    – btilly
    Feb 15, 2017 at 17:04
  • $\begingroup$ @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. $\endgroup$
    – btilly
    Feb 15, 2017 at 17:12
  • $\begingroup$ 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.) $\endgroup$
    – btilly
    Feb 15, 2017 at 17:17

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .