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

[martdowd at aol.com]

 Patrick Eklund wrote:

Is it time to finally separate mathematics from computer science, and I would be happy if computer science takes all results produced by Gödel, Turing and Church completely to the side of Computer Science, and mathematicians will be happy at least with Hilbert and maybe also Kleene. We will go back 100 years and restart from there. It's time to do so. We never did.
 
 The main new subject introduced by theoretical computer science, over and above how computation as formulated by Church-Turing-Post et al relates to the foundations of reasoning about the integers and formal systems therefore, is the complexity of computation.  This seems to provide a "working" dividing line between theoretical computer science and mathematics, although I think we have already seen some "crossover" research, such as the complexity of decidable theories.
Martin Dowd
 
-----Original Message-----
From: Patrik Eklund <peklund at cs.umu.se>
To: José Manuel Rodríguez Caballero <josephcmac at gmail.com>
Cc: Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Sat, Mar 4, 2023 11:09 pm
Subject: Re: L. E. J. Brouwer and the Sub-Axiomatic Foundations of Mathematics

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. This is where paradoxes and antinomies come from, basically adopting Richard and Liar in more or less subtle forms. Nothing wrong with that, in particular if it leads to innovative computations, but that's besides what mathematics and foundations of mathematics is- Indeed, I will be very fine with Computer Science taking care of the "mathematics of the brain" so that mathematics can continue to take care of the "mathematics of mathematics".The question of proof is indeed far from trivial and mathematics will never allow languages like Isabelle/HOL to be like a supersupervisor or "oberschwester" for best practice in mathematical proof mechanization.Is it time to finally separate mathematics from computer science, and I would be happy if computer science takes all results produced by Gödel, Turing and Church completely to the side of Computer Science, and mathematicians will be happy at least with Hilbert and maybe also Kleene. We will go back 100 years and restart from there. It's time to do so. We never did.What I'm saying is that we must be truly interested in solving antinomies. If computer science do not care to join, fine.Best,Patrik
On 2023-03-03 10:26, José Manuel Rodríguez Caballero wrote:
Dear FOM members,Traditionally, mathematics has developed from intuition, formalized in a set of axioms. The statements of a theory are proven or disproven by means of symbolic manipulations that are driven by algebraic, geometric, analytical, combinatorial, and other kinds of intuition. If I understood correctly, subaxiomatic foundations are the attempt to circumvent the intelligibility of mathematical practice and develop mathematics directly from the computational evolution of a complex system. From a technological point of view, subaxiomatic foundations are the presentation of mathematics that would be most compatible with the most powerful artificial intelligence algorithms, for example, deep learning. Following the analogy between symbolic machine learning for the conscious brain and statistical machine learning for the unconscious brain, we could say that subaxiomatic foundations are the mathematics of the subconscious part of the mind. That is, this type of mathematics tries to operate directly on the process that produces intuition rather than on its symbolic representation. Concerning this possibility, S. Wolfram wrote [1]: 
But if we actually want to make full use of the computational capabilities that our universe makes possible, then it's inevitable that the systems we're dealing with will be equivalent in their computational capabilities to our brains. And this means that—as computational irreducibility implies—we'll never be able to systematically "outthink" or "understand" those systems.


But then how can we use them? Well, pretty much like people have always used systems from the natural world. Yes, we don't know everything about how they work or what they might do. But at some level of abstraction we know enough to be able to see how to get purposes we care about achieved with them.
 In statistics, there are two goals: explainability and prediction. The best methods for one of these objectives are not the same as for the other. Traditional mathematics is like methods for the explanation of a data set, while subaxiomatic mathematics is like methods for prediction. It would be nice to have a translator from subaxiomatic mathematics to a human-readable mathematical system, such as Isabelle/HOL [2], but I am not sure that it would be possible. The question of the meaning of a mathematical proof is far from trivial. We can imagine proofs translated from this mathematical source code into Isabelle/HOL language and still feel unintelligible. There are many candidates as starting points of the subaxiomatic foundations. One of them are Kauffman's calling and crossing symbols [3]. Other candidates are combinators [4]. Here is a series of videos developing this idea, following a rather empirical approach [5] and here is a computational notebook on this subject [6]. According to L. E. J. Brouwer [7]: 
Completely separating mathematics from mathematical language and hence from the phenomena of language described by theoretical logic, recognizing that intuitionistic mathematics is an essentially languageless activity of the mind having its origin in the perception of a move of time. This perception of a move of time may be described as the falling apart of a life moment into two distinct things, one of which gives way to the other, but is retained by memory. If the twoity thus born is divested of all quality, it passes into the empty form of the common substratum of all twoities. And it is this common substratum, this empty form, which is the basic intuition of mathematics. 
 If we interpret the "substratum" mentioned by Brouwer as the evolution of a complex system and the lack of mathematical language as unintelligibility, I think we get the two main properties of the subaxiomatic foundations. Of course, there is a lot of work associated with the word "intuitionism" which Brouwer may reject as a betrayal of his original point of view. My question would be: To what extent does L. E. J. Brouwer's intuitionism resonates with the ideas of the subaxiomatic foundations? Kind regards,Jose M. References[1] Stephen Wolfram, Logic, Explainability and the Future of Understanding, Stephen Wolfram Writings, URL: https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ [2] Nipkow, Tobias, Markus Wenzel, and Lawrence C. Paulson, eds. Isabelle/HOL: a proof assistant for higher-order logic. Berlin, Heidelberg: Springer Berlin Heidelberg, 2002. [3] Kauffman, Louis H. "Iterants, Fermions and the Dirac Equation." arXiv preprint arXiv:1406.1929 (2014). https://arxiv.org/pdf/1406.1929.pdf [4] Schönfinkel, Moses. "Über die Bausteine der mathematischen Logik." Mathematische annalen 92.3-4 (1924): 305-316. [5] Metamathematics: Sub-Axiomatic Foundations: https://youtube.com/playlist?list=PLM_MgbAF1uYK4vSUEZtjnRVMfvcy-PshC [6] [WELP22] Sub-axiomatic foundations of group theory in SK combinators  https://community.wolfram.com/groups/-/m/t/2818259 [7] Brouwer, L.E.J., 1981, Brouwer's Cambridge lectures on intuitionism, D. van Dalen (ed.), Cambridge: Cambridge University Press, Cambridge.  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230306/f3ffbe3b/attachment-0001.html>