Lecture series on Logic and Foundations of Mathematics (1)
Lecture Title: Provability Logic and Modalised Fixed Points
Speaker: Prof. Albert Visser (University of Utrecht, Netherlands)
Date and Time: September 29, 2020, 19:00-21:00 Beijing time (UTC 11:00-13:00)
Organizer: School of Philosophy, Wuhan University
Platform: Zoom (ID: 839 0676 9057, Passcode: 925222)
Host: Prof. Yong Cheng (Wuhan University)
Abstract：
My talk is an introduction to classical provability logic with an emphasis on the fixed point calculation. Our treatment is slightly different from the usual one. We start with the logic K4 + fixed points. We show that this logic has “fixed point elimination”. For this aim we use a form of the multiple fixed points theorem. The result of eliminating the fixed point operator is Löb's Logic GL. We will also discuss arithmetical interpretations of GL.
About the speaker:
Prof. Albert Visser was assistant professor at Stanford University and Utrecht University and Professor of Logic, the Philosophy of Mathematics and Epistemology at Utrecht University. He is now emeritus professor at Utrecht University from 2016. His research centers on arithmetical theories, interpretability, constructivism, foundations of mathematics and topics in the philosophy of language. Albert Visser is a member of the Royal Netherlands Academy of Arts and Sciences. He is member of the editorial board of the Notre Dame Journal of Formal Logic. He served in various committees of the Association of Symbolic Logic.
Lecture series on Logic and Foundations of Mathematics (2)
Lecture Title: Proof Theory: From Arithmetic to Set Theory
Speaker: Prof. Michael Rathjen (University of Leeds, UK)
Date and Time: October 13, 2020, 4pm-6pm Beijing time (9am-11am UK time)
Platform: Zoom (ID: 671 9141 8191, Password：174598)
Organizer: School of Philosophy, Wuhan University
Interlocutor: Sam Sanders (TU Darmstadt, Germany)
Host: Prof. Yong Cheng (Wuhan University)
Abstract:
A central theme running through all the main areas of Mathematical Logic is the classification of sets, functions or theories, by means of transfinite hierarchies whose ordinal levels measure their ‘rank’ or ‘complexity’ in some sense appropriate to the underlying context. In Proof Theory this is manifest in the assignment of ‘proof theoretic ordinals’ to theories, gauging their ‘consistency strength’ and ‘computational power’. This area of mathematical logic has is roots in Hilbert's “Beweistheorie”, the aim of which was to lay to rest all worries about the foundations of mathematics once and for all by securing mathematics via an absolute proof of consistency. In the main, modern proof theory came into existence in the 1930s, springing forth from Gentzen's work, especially his consistency proofs of arithmetic. The intent of the talk is to introduce the main notions and results of proof theory and to explain the rationale of ordinal-theoretic proof theory, advancing from arithmetic to set theory.
About the speaker:
Prof. Michael Rathjen is one of the leading experts in modern proof theory. His most outstanding achievements belong to ordinal analysis, the most complicated and technically advanced area of the field, where exciting interplay with set theory, recursion theory and model theory comes into place. He also has made significant contributions to constructive set theory, explicit mathematics and Martin-Loef's type theory. M. Rathjen was an editor for the Journal of Symbolic Logic.
Lecture series on Logic and Foundations of Mathematics (3)
Lecture Title: Cut elimination and provably recursive functions
Speaker: Prof. Andreas Weiermann (School of Mathematics, Ghent University, Belgium)
Date and Time: 27th October 2020, 7pm-9pm Beijing time (1pm-3pm Belgium time)
Platform: Zoom (ID: 624 0604 7711, Password: 291067)
Organizer: School of Philosophy, Wuhan University
Interlocutor: Dr. Fei Liang (Shandong University)
Host: Prof. Yong Cheng (Wuhan University)
Abstract:
We start with sketching the Gentzen cut elimination theorem for predicate logic. We then introduce an infinitary system for Peano arithmetic which allows for cut elimination. By refining the classical cut elimination proof we obtain a neat characterization of the provably recursive functions of Peano arithmetic in terms of ordinal recursive functions.
About the speaker:
Prof. Andreas Weiermann is a Senior full professor in the school of mathematics at Ghent University in Belgium. He has made many contributions in varied fields of logic. His research interest covers proof theory, subrecursive hierarchies, term rewriting, well partial orderings, analytic combinatorics of the transfinite, phase transitions for Goedel incompleteness. He is editor of the Springer series “Trends in Logic”. Except for logic, he likes painting. He truly believes that art and mathematics fit nicely together and that creativity is one unifying element.
Lecture series on Logic and Foundations of Mathematics (4)
Lecture Title: Iterated consistency, reflection and foundations of mathematics.
Speaker: Prof. Joost J. Joosten (University of Barcelona, Spain)
Date and Time: 3th November 2020, 5pm-7pm Beijing time (10am-12am Spain time)
Platform: Zoom (ID: 623 7497 5671, Password: 240846)
Organizer: School of Philosophy, Wuhan University
Interlocutor: Prof. Albert Visser (Utrecht University)
Host: Yong Cheng (Wuhan University)
Abstrat:
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.
Lecture series on Logic and Foundations of Mathematics (5)
Lecture Title: Some theorems are more equal than others: a slow introduction to Reverse Mathematics
Speaker: Dr. Sam Sanders (Technical University of Darmstadt, Germany)
Date and Time: 17 November 2020, 7pm-9pm Beijing time (11am-1pm UTC)
Platform: Zoom (ID: 629 4146 6259)
Organizer: School of Philosophy, Wuhan University
Interlocutor: Prof. Yue Yang (National University of Singapore, Singapore)
Host: Prof. Yong Cheng (Wuhan University)
Abstract:
From high school mathematics to research level literature, we can easily find statements like“Theorem A is stronger than Theorem B” and “These two formulas are equivalent”. The field Reverse Mathematics provides a framework for making such statements precise, based on mathematical logic. I will provide a gentle introduction to this field and discuss some new directions based on my own research.
About the speaker:
Sam Sanders’ research is part of mathematical logic, computability and proof theory in particular. He investigates the role of the uncountable in these disciplines as follows: (1) studying mathematics in logic means chosing (often countable) representations/codes for classes of objects. Where does this coding practise break down for the uncountable? (2) What is the right scale for classifying objects? Is the Hilbert-Bernays inspired “Goedel hierarchy” based on comprehension the right one? (3) What are the foundational implications of logic? For instance, can they provide evidence for e.g. Platonism?
