Homotopy Type Theory UMyn8W7b (Rev #29)

Comments about school mathematics

On real numbers

There are many different types of real numbers, which are suited for different subjects taught in school mathematics.

Linear algebra and some of scalar differential calculus does not need any type of real numbers at all. The rational numbers or any other Archimedean ordered field suffices. Linear algebra is about vector spaces which is defined for general fields.

Archimedean ordered fields suffice for scalar differential calculus, because according to a result by Otto Hoelder, any Archimedean ordered field embeds in the Dedekind real numbers, and therefore is a metric space. The epsilon-delta defintion of a limit of a function is thus well defined for any Archimedean ordered field, and one could define continuous functions, differentiable functions, smooth functions, power series, and analytic functions, as well as ordinary differential equations.

For vector differential calculus and extensions such as geometric differential calculus and tensor differential calculus, one only needs the real constructible numbers or any Euclidean Archimedean ordered field, so that the square root function and the Euclidean metric on the vector space is well defined. For the same reason as for scalar differential calculus, one could define partial derivatives, directional derivatives, the geometric derivative, the div, the curl, systems of ordinary differential equations, and partial differential equations.

For pre-algebra, numerical analysis, the theory of equations, and trigonometry, the Cauchy real numbers suffice. The Cauchy real numbers suffice for pre-algebra and numerical analysis because according to a result by Auke Booij, every Cauchy real number is a Dedekind real number with a locator, and every Dedekind real number with a locator is a Cauchy real number and has an infinite decimal representation. Thus, every Cauchy real number has a locator. Conversely, one could prove that every infinite decimal representation of a real number has a corresponding Cauchy sequence. The Cauchy real numbers suffice for the theory of equations because according to a result by Wim Ruitenberg, the Cauchy real numbers are a real closed field and its algebraic closure is the Cauchy complex numbers. However, this is only true for the Cauchy real numbers. In trigonometry, the transcendental functions such as $\exp$, $\sin$, and $\cos$ are defined as limits of a certain Cauchy sequence or series, and Auke Booij showed that the limit of a sequence of Cauchy real numbers has a locator and is thus a Cauchy real number.

For geometry one needs the Dedekind real numbers because the Dedekind real numbers are the only type of real numbers that are Dedekind complete and connected, or where the shape of the type of real numbers is contractible. The connected components of every other type of real numbers defined above could be shown to be homotopy contractible, and thus the shape of the type is equivalent to the type itself.

A replacement for the quadratic formula

Very few people use the quadratic formula for real quadratic functions in applications of mathematics. (The quadratic formula also doesn’t hold for most types of real numbers in constructive mathematics.) Instead, they use numerical solvers in a computer or on a calculator, and it would be better for students to understand the numerical analysis algorithms behind the numerical solvers:

Given a real quadratic function $f:\mathbb{R} \to \mathbb{R}$, $f(x) \coloneqq a x^2 + b x + c$ for real numbers $a:\mathbb{R}$, $b:\mathbb{R}$, $c:\mathbb{R}$, where $\vert a \vert \gt 0$, suppose we want to find an approximate zero of $f$. The real quadratic function has discriminant $\Delta = b^2 - 4 a c$ and has 2 zeroes if $\Delta \gt 0$, 1 zero of multiplicity 2 at $2 a x_i + b = 0$ if $\Delta = 0$, or no zeroes of $\Delta \lt 0$. (In constructive mathematics, there are real quadratic functions where it isn’t possible to determine the number of zeroes the real quadratic function has.) Assume that $\Delta \gt 0$. Select a real number $x_0:\mathbb{R}$ as the initial guess, where $2 a x_0 + b \gt 0$ or $2 a x_0 + b \lt 0$, and the next guess would be defined as

The algorithm isn’t valid when $2 a x_0 + b = 0$ because of division by zero. When $2 a x_0 + b \gt 0$, the algorithm converges towards the zero at $x \gt -\frac{b}{2a}$, and when $2 a x_0 + b \lt 0$, the algorithm converges towards the zero $x \lt -\frac{b}{2a}$, where $-\frac{b}{2a}$ is where the extremum (minimum/maximum) of the parabola occurs.

This is known as Newton’s method for real quadratic functions, and could be introduced in any secondary school algebra course. The proof would have to wait until a calculus course, but the proof of the fundamental theorem of algebra requires some form of real or complex analysis and the fundamental theorem of algebra is still taught in secondary school algebra.