ABSTRACT
In the past 20 years, tools from proof theory, certain so-called proof transformations, have been used systematically
to extract explicit effective data from prima facie noneffective arguments used frequently in mathematical reasoning.
Such noneffective steps prevent one from directly following the flow of data processed in a proof and require a reinterpretation
of the argument using higher order tools to restore the flow of information. We discuss what kind of quantitative information
one can extract under which circumstances from proofs of existential statements which proceed by contradiction.
We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functions B, L,
where L is a learning procedure for explicit witnessing which succeeds after at most B(a)-many mind changes,
where "a" is the set of parameters of the statement in question. In many cases one can obtain even fully effective data (
with no need for a mind change at all) from highly nonconstructive arguments.
SPEAKER'S BIOGRAPHY
Ulrich Kohlenbach (https://www2.mathematik.tu-darmstadt.de/~kohlenbach/)
is professor of mathematics at the Technische Universität Darmstadt, Germany. He is one of the world's leading scholars in mathematical logic
and its applications. He received his Ph.D. from the University of Frankfurt (J.W.Goethe-Universität) in 1990 under the supervision
of Horst Luckhardt and passed his habilitation ('venia legendi') in mathematics five years later. During the academic year 1996-1997
he has been a visiting assistant professor at the University of Michigan.
In 1997 he joined the computer science department of Aarhus University where he became tenured associate professor in 2000
and worked until 2004. Since 2004 Kohlenbach has been a full professor at the Technische Universität Darmstadt.
His research interests lie in the field of logic (in particular proof theory, computability theory, and constructive reasoning)
with applications to mathematics and computer science, computational content of proofs, proof interpretations and their use in mathematics. Kohlenbach achieved relevant results in each of these research areas. These results appeared in national and international journals and books.
In 2011, Kohlenbach received the prestigious Kurt Gödel Research Prize from the Kurt Gödel Society. He was President of the German Association
for Mathematical Logic and Basic Research in the Exact Sciences (DVMLG) from 2008 to 2012 and President of the Association
for Symbolic Logic from 2016 to 2018.
|