I would like to teach students about the pertinence of the Axiom of Infinity. Are there any high school-level theorems of arithmetic, algebra, or calculus, whose proof depends on the Axiom of Infinity? If there are no such examples, what would be the simplest theorem which demands the Axiom of Infinity?
It seems we can still generate endless numbers without the Axiom of Infinity, but this axiom lets us treat infinite sets as a whole -- is this true?
On
The "Hydra game" also known as Goodstein's theorem can be easily explained to highschoolers, and is not provable in Peano arithmetic. Kirby and Paris proved that the result is dependent on infinitary assumptions.
The axiom of infinity, in ZFC set theory, says that there is an infinite set. Once you have one infinite set, because you can take the powerset of any set, you can form larger and larger infinite sets, in terms of cardinality. On the other hand, none of the other axioms of set theory is able to create an infinite set out of finite sets. So the axiom of infinity is important as a fundamental basis in set theory, just as an axiom that there are infinitely many different points is important in Euclidean geometry. Otherwise, we could have a world in which all sets are finite, or a geometry in which there are only finitely many points. Those kinds of models are interesting but are not the main subject of their fields.
One challenge in the question is that you are presumably looking for statements that can be expressed solely in terms of finite objects such as natural numbers, but which cannot be proved without the use of some kind of infinitary axioms.
Moving on - for simplicity, suppose we take my interpretation of the question to mean that we want true statements that are expressed in the language of first-order Peano arithmetic (PA). These can have many quantifiers, but are expressed solely in terms of natural numbers. The challenge with such statements is that they can't imply the axiom of infinity, even if they are not provable from PA or not provable from ZFC without the axiom of infinity. This is because such theorems are true in the standard model of PA, with no "sets" and certainly no infinite sets.
Most of the theorems that you will find that are expressible in PA, but not provable with the axiom of infinity, are either consistency statements or combinatorial statements. These can often be inaccessible even to non-logicians with much more than a high school background. But there are some examples that can be explained.
One interesting example is the TREE sequence, which was recently on the Numberphile Youtube channel (good for high schoolers) here. There are several blog posts about this sequence, such as this one.
The proof that this sequence is well defined - that TREE($k$) is a natural number for each natural number $k$ - is a corollary of Kruskal's theorem, which is not phrased as a finitary statement. The fact that TREE(3) exists is very hard to prove in Peano arithmetic - Friedman states that any proof in PA that TREE(3) exists must have at least $2^{1000}$ symbols (FOM post). So the only way we are able to prove that TREE(3) exists, with a proof short enough that we can actually read it, is to use infinitary methods, such as ZFC set theory with the axiom of infinity.