Lecture Title: Iterated consistency, reflection and foundations of mathematics.
Speaker: Prof.Joost J. Joosten (University of Barcelona, Spain)
Date and Time: 3rd November 2020, 5pm-7pm Beijing time (10am-12am Spain time)
Commentator: Prof. Albert Visser (Utrecht University)
Organizer: School of Philosophy, Wuhan University
Host: Yong Cheng (Wuhan University)
By Gödel’s second incompleteness theorem we know that any consistent axiomatisable theory interpreting enough arithmetic cannot prove its own consistency. Turing realised that this induces a sequence of ever stronger theories if we start with a sound base theory T and if we fix a natural ordinal representation: at stage zero, we consider this base theory T; at successor stages we take the theory at the previous stage together with the consistency assertion of this theory; at limit stages we simply take the union of all theories before. These progressions of theories are called Turing progressions. In this talk we will see how Turing progressions can be used to gauge the strength of mathematical theories: Start out with some trustworthy base theory T and perform a Turing progression over T until the stage where you “hit” the target theory. We will see early results by Schmerl. Next we deal with Beklemishev’s paradigm using polymodal provability logics to perform this program. At the end of the talk we will mention some current progress.
About the speaker:
Joost J. Joosten is a professor in the department of philosophy at University of Barcelona in Spain. He works in two main research lines. The first line of research is related to foundations of mathematics and ordinal analysis. In this line of research polymodal provability logics are used to denote ordinals, fragments of mathematical theories and Turing progressions among others. This bridging function of these polymodal provability logics allows that they can be the main tool for performing ordinal analysis of mathematical theories. The other line of research concerns applied proof theory where, using proof assistants and intuitionistic/constructive logic, proven error-free software is produced. Being provably error-free is a must for critical and legal enforcement software. Apart from studying and applying the main techniques for achieving provably error-free software this line of research also studies the impact and integration of the techniques in the legal landscape in particular and in society in general.
Zoom ID：623 7497 5671