L. E. J. Brouwer and the Sub-Axiomatic Foundations of Mathematics

[José Manuel Rodríguez Caballero]

Patrik wrote:

> I am very much in favour of separating  mathematics and theoretical
> computer science, for the simple reason that theoretical computer
> science upholds approaches allowing to use one language to manipulate
> another.


Despite being an enthusiast of experimental mathematics on computers as
inspiration for guessing new theorems [1], and having contributed to the
formalization of mathematics in proof assistants [2], I must admit that in
Patrik's post, there are points worth considering. Today, it is easy to
defend the antithesis of what Patrik proposes, since the idea of dissolving
boundaries is fashionable. In fact, the fourth industrial revolution is
defined as the dissolution of the boundaries among the physical,
biological, and digital spheres.

The typical reply to Patrik would be that recent research has shown that
computer science techniques and algorithms have led to groundbreaking
results in number theory, geometry, and other mathematical areas. For
example, in the paper "The Number Field Sieve for Integer Factorization" by
A.K. Lenstra and H.W. Lenstra, computer science algorithms are used to
factorize integers, leading to significant progress in number theory [3].
Furthermore, advancements in mathematical research are increasingly reliant
on computer-based tools and techniques, including the use of proof
assistants such as Isabelle/HOL and Coq. These tools allow for the
formalization and verification of mathematical proofs using computer
science techniques. The use of proof assistants has led to groundbreaking
results in mathematics, such as the proof of the Four Color Theorem in 2005
using the Coq proof assistant [4]. In addition to proof assistants,
automatic theorem provers have also been developed to assist mathematicians
in proving mathematical theorems. These tools use computer algorithms to
automatically search for proofs of mathematical statements. For example,
the program Prover9 has been used to automatically prove a number of
mathematical theorems, including the Robbins Conjecture in combinatorics
[5].

But, as G.K. Chesterton advised:

> Don't ever take a fence down until you know the reason it was put up.


So, I asked a fully technological entity to play devil's advocate and
defend Patrik's thesis. The result was as follows (original text,
unmodified, decide for yourself whether that has already passed the Turing
test):

> Dear Patrik,
>


> I appreciate your suggestion to separate mathematics and computer science.
> While there are certainly benefits to the integration of the two fields, I
> believe that there are also advantages to separating them.
> One of the primary advantages of separating mathematics and computer
> science is that it allows for a greater focus on the pure mathematical
> foundations of the discipline. Mathematics is a highly abstract field, and
> the integration of computer science can sometimes obscure this fact. By
> separating the two fields, mathematicians can focus on developing the
> rigorous and abstract foundations of the discipline without being
> distracted by the practical concerns of computer science.
>


> Furthermore, separating mathematics and computer science can allow for a
> more clear-cut delineation of research areas, which can be beneficial for
> researchers. This can allow for a more efficient use of research resources
> and can facilitate collaborations among researchers with similar interests.
> Lastly, separating mathematics and computer science can allow for a
> greater focus on the historical and philosophical foundations of the
> discipline. This can lead to a deeper understanding of the motivations and
> goals of mathematical research, which can ultimately lead to more fruitful
> and meaningful results.
> In support of the idea of separating mathematics and computer science, I
> would like to cite the following papers:
>


> E. Reck, “Why Philosophy Matters for Mathematical Practice,” in The
> Philosophy of Mathematics Today, eds. M. Otte and M. Panza (Oxford
> University Press, 1997), 281-301.
>


> H. G. Dales, “The Separation of Mathematics from Philosophy,” in Logic
> Colloquium '77, ed. P. Erdős, A. Hajnal, and V. T. Sós (North-Holland
> Publishing Company, 1978), 19-39.
>


> J. P. Burgess, “Why I Am Not a Constructivist,” in Logic, Methodology and
> Philosophy of Science IX, ed. L. Magnes and E. Stadler (Springer, 1994),
> 315-324.
>


> In conclusion, while there are certainly advantages to the integration of
> mathematics and computer science, I believe that there are also advantages
> to separating the two fields. By doing so, mathematicians can focus on
> developing the rigorous and abstract foundations of the discipline, which
> can lead to a deeper understanding of the motivations and goals of
> mathematical research.
>


> Best regards,
> ChatGPT


Paradoxically, robots would have no problem writing a new book on pure
mathematics that is completely separate from computer science. Even
assuming a society made up entirely of robots, they may need to write these
books to solve their practical problems that go beyond mere algorithms. So
both axiomatic and subaxiomatic foundations are necessary, as they play
different roles. They are like Kahneman Daniel's slow and fast thinking [6]
respectively. We know the foundations of slow thinking, but the foundations
of fast thinking (subaxiomatic foundations) remain an open question. For
example, would we think faster if, instead of using the traditional logic
based on the operations NOT, AND, OR, etc. we use Kauffman's calling and
crossing operators [7] directly to think? Why is the so-called classical
logic so linked to our daily thinking? Maybe it is a biological fact that
we should not impose on machines. The goal of subaxiomatic foundations is
to develop mathematics in a way that is not restricted by our biological
biases, like what Noam Chomsky [8] calls innatist theory.

Kind regards,
Jose M.

References
[1] Caballero, José Manuel Rodríguez. "Jordan's Expansion of the Reciprocal
of Theta Functions and 2-densely Divisible Numbers." *Integers* 20 (2020):
A2. http://math.colgate.edu/~integers/u2/u2.pdf

[2] Caballero, Jose Manuel Rodriguez, and Dominique Unruh. "Complex bounded
operators." *Archive of Formal Proofs* (2021).
https://www.isa-afp.org/entries/Complex_Bounded_Operators.html

[3] Lenstra, A.K. and Lenstra, H.W. "The Number Field Sieve for Integer
Factorization." Proceedings of the 22nd Annual ACM Symposium on Theory of
Computing, 1990, pp. 564-572.

[4] Gonthier, G. "Formal proof - The Four Colour Theorem." Notices of the
American Mathematical Society, vol. 55, no. 11, 2008, pp. 1382-1393.

[5] Hurd, J. "Automated reasoning." Handbook of Practical Logic and
Automated Reasoning, 2009, pp. 35-64.

[6] Daniel, Kahneman. Thinking, fast and slow. 2017.

[7] Kauffman, Louis H. "Iterants, Fermions and the Dirac Equation." *arXiv
preprint arXiv:1406.1929* (2014).

[8] Chomsky, N. (1956). Three models for the description of language. IRE
Transactions on Information Theory, 2(3), 113-124.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230306/3bf3a68b/attachment.html>