> 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

> 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.