#	Pagina
attuale pagina	/open-h2020/projects/202055/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - SLMK (The Scope and Limits of Mathematical Knowledge)

Teaser

Summary

Digital computers are based on a mathematical idea (Turing machines) originally developed to resolve a question in the foundations of mathematics: whether all mathematical problems could be solved by repeated application of a set of rules. The negative answer to this question led to a debate about whether the human mind was more powerful than a computer, and what the implications were for the scope of mathematical knowledge. In order to achieve progress in this debate, we must develop a more precise account of what an idealised mathematician can know in principle by means of rigorous mathematical proof.

In the SLMK project, the idealisations embedded in the notions of formal proof (proof within an axiomatic system with a fixed language and fixed rules of inference, from a fixed set of basic principles) and informal proof (proof as carried out in mathematical practice, using any linguistic and inferential means the mathematician deems necessary) were investigated using an interdisciplinary methodology, applying formal tools from computability theory, proof theory, and model theory, and analysing case studies from contemporary and historical mathematics.

The project objectives were as follows: (i) to investigate the relationship between formal and informal arithmetical reasoning in order to identify a formal system that captures informal reasoning formally, allowing the investigation of the scope of mathematical knowledge; (ii) to achieve substantial progress on the debate on the mechanisation of the mind; and (iii) to use formal tools to obtain a naturalistic account of informal mathematical reasoning and the mechanisms of justification in mathematical practice.

The result of the project is a novel and comprehensive view of mathematical methodology and the mechanisms of justification in mathematical practice that is historically and mathematically informed, and compatible with a broadly empiricist view of science and scientific justification.

Work performed

The first part of the project investigated the notions of formal and informal proof, and how they are connected to our acceptance of mathematical statements, with a particular focus on arithmetical reasoning. Our everyday use of arithmetic seems to imply that we implicitly believe that arithmetical reasoning will not lead to any contradictions and that every conclusion we obtain by rigorous arithmetical reasoning is true. These properties can be expressed formally in the language of arithmetic through â€˜reflection principlesâ€™. Such principles, however, do not follow from the axioms of arithmetic, highlighting an asymmetry with our informal reasoning. This project developed an epistemic account of the justification of reflection principles, which dispenses with any appeal to a formal truth theory.

The second part of the project was devoted to the development of a rigorous account of the notion of â€˜human-effective computabilityâ€™: computability by an idealised mathematician that incorporates the non-deterministic character of mathematical reasoning. It was argued that the epistemic version of Churchâ€™s Thesis holds for this notion, and the hypotheses advanced were tested in models that embed natural idealisations. This laid the grounds for fruitful applications to GÃ¶delâ€™s Disjunction. This work package led to a promising new line of research on the use of computability-theoretic hierarchies to measure the complexity of mathematical objects and mathematical reasoning. Preliminary results from this research formed the basis of a plenary lecture at the Logic Colloquium 2018.

The third part of the project developed an original version of mathematical naturalism which accounts for parts of mathematics that are far removed from applications in scientific practice and is compatible with an empiricist approach to mathematics. The result of this novel view is a naturalist framework that fits with mathematical practice and is ontologically parsimonious. The project then applied formal tools from reverse mathematics to the analysis of the informational content of mathematical proofs, with the aim of explaining cases in which, after a purely existential result is obtained, mathematicians expend considerable efforts to obtain more â€˜informativeâ€™ proofs. The major innovation of this approach consisted in applying the distinction between â€˜de reâ€™ and â€˜de dictoâ€™ predication of properties to the analysis of existential statements in mathematics, to obtain notion of the informational content of a proof that applies to both classical and constructive mathematics.

Invited talks disseminating the research conducted within the project were given at numerous universities and world-leading centres for philosophical and mathematical logic, including the universities of Glasgow, Konstanz, Manchester, Oxford, Lorraine, Salzburg, St. Andrews, TÃ¼bingen, and Udine within the EU, as well as Boise State, UC Berkeley, UC Irvine, and the University of Utah. The results of the project are also being disseminated in the form of articles in peer reviewed journals, chapters in collected volumes, and edited volumes.

Final results

Each of the work packages carried out in this project advanced the state of the art in the field. The work on human-effective computability led to substantial advances in the analysis of the idealisations that our formal models of informal mathematical reasoning should embed, and supported that analysis with technical results demonstrating the robustness of the notion of the human-effective computability and its relevance for the question of absolute undecidability of mathematical propositions. The work on the justification of new arithmetical principles via the relation between formal and informal provability led to a new, epistemic route to those principles. The work on the mechanisms of justification in mathematical practice led to a a new conception of mathematical proof with diverse aspects, that can be analysed using formal methods, and fits in a broadly empiricist view. The projectâ€™s results therefore push the boundaries of philosophical investigations of mathematical practice and the foundations of mathematics.

The project also contributed positively to the mutual cooperation between researchers in mathematics, education, theoretical computer science, and philosophy, highlighting the need for and the benefits of interdisciplinary studies. The combination of powerful formal tools with a novel approach to the understanding of the limitations of mathematical reasoning is expected to revive interest in traditional foundational questions in mathematics and theoretical computer science that have their roots in the pioneering work of modern giants such as Leibniz, who invented the first calculating machine in the 17th century, and Turing, who developed the notion of Turing machine that lies at the heart of our contemporary understanding of computation. The project thereby reinforces the image of philosophical enquiry as continuous with the natural and formal sciences that is at the core of the European cultural and scientific identity. The impact of this research is clear in the large and growing number of invitations to present it in both philosophical contexts and at large interdisciplinary events where the audiences include mathematicians, computer scientists, linguists, and researchers in mathematical education, as well as in a number of invitations to publish new work building on the research carried out in the project.