@inbook{82206f5b744c4e7baf7c977ce92826d7,
title = "From Mathesis Universalis to Provability, Computability, and Constructivity",
abstract = "This paper advocates for a revival of Leibniz{\textquoteright} mathesis universalis as proof theory together with his claim for theoria cum praxi under the conditions of modern foundational research of mathematics and computer science. After considering the development from Leibniz{\textquoteright} mathesis universalis to Turing computability (Chap. 1 ), current foundational research programs are analyzed. They connect proof theory with computational applications - proof mining with program extraction (Chap. 2 ), reverse mathematics with constructivity (Chap. 3 ) and intuitionistic type theory with proof assistants (Chap. 4 ). The foundational program of univalent mathematics is inspired by the idea of a proof-checking software to guarantee correctness, trust and security in mathematics (Chap. 5 ). In the age of digitalization, correctness, security and trust in algorithms turn out to be general problems of computer technology with deep societal impact. They should be tackled by mathesis universalis as proof theory (Chap. 6 ).",
keywords = "Constructivity, Intuitionistic type theory, Machine learning, Mathesis universalis, Program assistant, Program extraction, Proof mining, Reverse mathematics, Theoria cum praxis, Univalent foundations program",
author = "Klaus Mainzer",
note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.",
year = "2019",
doi = "10.1007/978-3-030-20447-1_12",
language = "English",
series = "Synthese Library",
publisher = "Springer Science and Business Media B.V.",
pages = "203--234",
booktitle = "Synthese Library",
}