For over a century mathematicians have wrongfully divorced themselves from the fundamental developments in mathematical logic which took place at the turn of the 20th century. These subjects were better received in computer science (and philosophy). Mathematicians have always used computers as a tool since computers were first developed, even if mainly in specialized or applied branches. But they had in general no philosophical, logical and computational understanding of key developments and results in mathematical logic and the foundations of mathematics, specially what formal systems, computability and formalization signify for mathematics. A harmful myth or half-truth was widely adopted: Gödel allegedly "destroyed" Hilbert's program and mathematics is somehow not formalizable or computable. In reality every mathematical theory in order to claim epistemic certitude or value must pass the test of formalizability in some system T. As a consequence if a sentence in T has a proof whose size is human manageable, then a computer can find it. Just as if a conjecture has a counter-example of human-manageable size, then a computer can in principle find it. The particular method of search (brute force, heuristics, machine learning, etc.) is not important. For a long time it was simply a question of computers not having the memory or processing power required to perform such searches or apply the required optimization and training algorithms.
A notable development occurred when mathematicians finally became interested in formalizing theorems and checking proofs using proof assistant software. Voevodsky was a Fields Medalist taking an active and serious interest in proof assistants and their theoretical foundations. With the advent of the 21st century computer hardware became thousands of times faster and memory capable. The circumstance of so-called AI mathematical breakthroughs - regardless of the essential human input involved - can never count as anything but truisms from a philosophical point of view. If there is a human-manageable sized counter-example or proof then a computer can find it - this is a truism, part of the nature of mathematics.
The essence of mathematics, its beauty, lies in the the art of organizing a body of knowledge into definitions, examples and counter-examples, lemmas, theorems, applications and interconnections between different areas. In giving meaning, elegance, clarity and efficiency to the proofs and conceptual structures involved, something which can depend heavily on the formal system or software adopted.
And what about the verification that an alleged formalization of a proof does in fact prove what it is supposed to?
But specially the study of how one formal system reflects, interprets or can yield meta-theoretical knowledge about another - and how one area interprets and applies to another. Thus we can distinguish between two searches. One which explores a formal system T directly, another which explores how other formal systems can interpret and yield knowledge regarding a given problem in T. And we need results regarding the length of proofs, in particular limiting results showing that for a wide class of relevant systems T there are "small" provable sentences whose smallest proofs exceed the capacity of all modern hardware.
The great philosophical and mathematical contemporary relevance of "ultrafinitism" (for instance Esenin-Volpin) and "ultraconstructivism" is evident! See the books Predicative Arithmetic by Edward Nelson and Bounded Arithmetic by Samuel Buss. The fusion and mutual clarification between mathematics and programing languages cannot be but a good thing. And this has tremendous philosophical significance, specially, with regards to the philosophy of Plotinus. Genuine ultrafinitism deconstructs false metaphysics, imposes very demanding epistemic standards and ontological parsimoniousness precisely in order to pave the way for true metaphysics and transcendental knowledge.
And furthermore ultrafinitism has huge social and political consequences relating to the radical reconsideration of the value, merit, prestige and economic support accorded to mathematical activity and productivity. Thus we need a new pantheon of the truly great mathematicians, computer scientists and logicians (like Bolzano, Peirce, Frege, Russell, Church, Skolem, Gödel, Brouwer, Heyting, Hilbert, Turing, Herbrand, Jaśkowski , Gentzen*, Schütte, Kleene, Girard, Lawvere, Per Martin-Löf, Edward Nelson,...), Genuine mathematics - which transcends the division between science and the humanities - should at the same time:
i) Contribute to the progress of science, medicine and engineering
ii) Contribute to human development (creativity, problem-solving, recreation) and the fundamental unity between mathematics, programing, logic and games. Also manifesting the inseparability between true intelligence and morality: Esenin-Volpin was a human rights activist and Edward Nelson grew up in a nonconformist milieu.
iii) Furnish a basis for philosophical knowledge and spiritual-ethical development
*While the immediate structural foundations for Gentzen's calculi are usually attributed to Paul Hertz, Hertz in turn appears to have merely copied the same theory already extensively developed by Bolzano and which in turn can be traced to Stoic Logic (the cut rule being one of the themata). Gentzen is included in this list essentially for his proof-theoretic ordinal version of the incompleteness theorem and other major proof-theoretic results.
The numerical algorithms used in applied science and engineering are always feasible in the sense that for a feasible input they yield a feasible output in a feasible amount of time. This suggests that there should be some way of "reducing" standard minimal reverse mathematics axiomatizations of analysis used by Simpson to the kind of system used by Nelson. That is, we consider for instance even the restricted forms of induction as convenient fictions, the only real induction being $I\Delta_0$, induction over formulas with bounded quantifiers.
Doing mathematics and its research strategies have close affinities to games such as Chess and Go and so it is not surprising if models used to find proofs employ similar training methods.
No comments:
Post a Comment