Written: July 2, 2017
I just finished reading (parts of) a fascinating, beautifully written, sermon, by Constructive Mathematician Andrej Bauer, preaching the merits of constructive mathematics, and showing how one can get almost everything dear to the classical mathematician without the pernicious law of excluded middle.
While I admire the eloquence of Bauer, I, being an ultra-finitist, could not relate to it. It read like Martin Luther's critique of Thomas Aquinas. Suppose that you are an atheist, or agnostic, or Jewish, or Buddhist, then they are both wrong, and their quibbles over minutiae are at best amusing.
The intuitionist-constructivist movement that started with the Cantor-Kronecker and Brouwer-Hilbert feuds, still holds the basic dogmas of infinitarian mathematics, and their "cure" sounds like talmudic pilpul and apologetics. There is a much simpler way. Keep everything discrete and finite, as outlined in my essay Real analysis is a degenerate case of Discrete analysis. Instead of the "reals", R, do analysis on Z/pZ where p is the "largest prime", and the mesh size is h=1/p. Since p is Soo large (and h is so small, and both unknowable) keep them symbolic.
One of the things in Bauer's article was a "corrected" proof of the Intermediate Value "Theorem". To me, the statement itself is false! Since the real "real" line is discrete, with "mileposts" that are distance h apart, it is very possible that a "continuous" function (in fact, in discrete calculus, all functions are continuous) never vanishes inside an interval even if its values have opposite signs at its endpoints. What is true is that there exists an "atomic interval", of length h, where the function takes opposite signs, and now the proof is an utter triviality.
Instead of differntiability, we have "Lipschitz condition": |f(a)-f(b)| ≤ K|a-b| for a symbolic K. Instead of the derivative, we have the finite-difference operator f'(x):=(f(x+h)-f(x))/h, instead of xn we have x(x+h)...(x+h(n-1)). We can still have Taylor series, and even complex analysis (and discrete complex-analytic functions), except that the size of the calculus textbooks would considerably shrink, and one would be able to go thorough the calculus sequence in a few weeks. At the end of the day, to get the classical theorems, just set h=0.
But what about all the "wonderful" edifice made by classical mathematics, that the costructivists try so hard to bend to their slightly-modified dogmas? Well, modern mathematics, as practiced today, looks the way it is due to the historical accident that it was developed before computers came along, and its high-priest, (mentioned favorably in Bauer's essay), Alexandre Grothendick, even thought that the computer is the devil (and vice versa). If we relegate all this (including measure theory, and the continuous stochastic Ito calculus, abstract Grothendick-style algebraic geometry, etc. etc.) to the province of historians and theologians, and start mathematics ab initio, and only talk about finite sets and discrete calculus, but keeping p (and h) symbolic, we will get a leaner and livelier mathematics. While doing a discrete analog of classical calculus is almost trivial, there are so many challenging problems in finite combinatorics, and finite number theory.
Anderj Bauer laments that it is hard to kick old habits, but, he himself has to kick the old habit of believing in infinite sets.