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

[Patrik Eklund]

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/20230305/5319151f/attachment-0001.html>