Lecture series on Logic and Foundations of Mathematics (10)
Lecture Title: Proof Theory: From the Foundations of Mathematics to Applications in Core Mathematics
Speaker: Prof. Ulrich Kohlenbach (Technical University of Darmstadt, Germany)
Date and Time: 2021-03-09, 16:00-18:00 Beijing time (UTC 8:00-10:00)
Platform: Zoom (ID: 67685850217, Password: 20210309)
Organizers:
School of Philosophy, Wuhan University
Tianyuan Mathematical Center in Central China
School of Mathematics and Statistics, Wuhan University
Interlocutors:
Dr. Thomas Powell (University of Bath, UK)
Dr. Sam Sanders (Ruhr-Universität Bochum, Germany)
Prof. Hong-Kun Xu (Hangzhou Dianzi University, China)
Host: Prof. Yong Cheng (Wuhan University, China)
Abstract:
During the last two decades a systematic program of `proof mining' emerged as a new applied form of proof theory and has successfully been applied to a number of areas of core mathematics. This program has its roots in Georg Kreisel's pioneering ideas of `unwinding of proofs' going back to the 1950's who asked for a `shift of emphasis' in proof theory away from issues of mere consistency of mathematical theories (`Hilbert's program') to the question `What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?'We are primarily concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of infinitary noneffective principles. The main logical tools for this are so-called interpretation. Logical meta-theorems based on such interpretations have been applied with particular success in the context of nonlinear analysis including fixed point theory, ergodic theory, continuous optimization, game theory and abstract Cauchy problems. The combinatorial content can manifest itself both in explicit effective bounds as well as uniformity results.
In this talk we will outline the general background of this logic-based approach and its origin in research on the foundations of mathematics and indicate some recent applications in the context of nonlinear analysis.
About the speaker:
Ulrich Kohlenbach is a German mathematician and professor of mathematical logic at the Technische Universität Darmstadt. His research interests lie in proof theory. He is a leading expert in the field of proof mining. Kohlenbach was President of the German Association for Mathematical Logic and the Foundations of Exact Sciences (DVMLG) from 2008 to 2012, and President of the Association for Symbolic Logic from 2016 to 2018. He was the Dean of Department of Mathematics at the Technische Universität Darmstadt. In 2011 he received the prestigious Kurt Gödel Research Prize Fellowship of the Kurt Gödel Society. He was an invited speaker at the 2018 International Congress of Mathematicians (Section: Logic and Foundations). He has published more than 90 research papers in mathematics and logic, and a book titled "Applied Proof Theory: Proof Interpretations and their Use in Mathematics" in the series of "Springer Monographs in Mathematics" in 2008. He is an advisory editor of Journal of Mathematical Logic, and a coordinating editor of Annals of Pure and Applied Logic.
Lecture series on Logic and Foundations of Mathematics (11)
Lecture Title: Well ordering principles and a uniform Kruskal theorem
Speaker: Dr. Anton Freund （TU Darmstadt, Germany）
Date and Time: 2021-03-23, 16:00-18:00 Beijing Time （UTC 8:00-10:00）
Platform: Zoom (ID: 678 2616 2829, Password: 899127)
Organizer:
School of Philosophy, Wuhan University
Interlocutors:
Dr. Sam Sanders (Ruhr-Universität Bochum, Germany)
Dr. Juan P. Aguilera (Ghent University, Belgium)
Host: Prof. Yue Yang (National University of Singapore, Singapore)
Abstract:
Well ordering principles are statements of the form ``F(X) is a well order for any well order X", where F is a transformation of linear orders (usually computable). They connect several areas of mathematical logic, notably ordinal analysis, computability theory and reverse mathematics. In this talk, I introduce the area and present recent work with Michael Rathjen and Andreas Weiermann (arXiv:2001.06380): We have investigated the astonishing meta-mathematical properties of a uniform Kruskal theorem, which extends the original theorem from trees to general recursive data types.
About the speaker:
Anton Freund is a postdoctoral researcher in the Logic Group at theTechnical University of Darmstadt (assistant of Ulrich Kohlenbach). He obtained his PhD from the University of Leeds in 2018 (supervised by Michael Rathjen). In his research, he aims to connect proof theory (ordinal analysis, dilators, computational content), set theory (admissible sets, reflection principles) and combinatorics (well quasi orders, mathematical independence).
Lecture series on Logic and Foundations of Mathematics (12)
Lecture Title: Interactive theorem proving and the Lean theorem prover
Speaker: Prof. Jeremy Avigad (Department of Philosophy and Department of Mathematical Sciences, Carnegie Mellon University, USA)
Date and Time: 2021-04-07, 9:30-11:30 Beijing Time （UTC 1:30-3:30）
Platform: Zoom (ID: 666 7012 4180, Password: 831333)
Organizer:
School of Philosophy, Wuhan University
Interlocutors:
Qinxiang Cao (Shanghai Jiao Tong University, China)
Bohua Zhan (Institute of Software, Chinese Academy of Sciences, China)
Yangjing Wang (Peking University, China)
Host: Prof. Yong Cheng (Wuhan University, China)
Abstract:
Since the early twentieth century, it has been understood that mathematical statements can be expressed in formal languages, and mathematical proofs can be represented in formal deductive systems with precise rules and semantics, at least in principle. Remarkably, the development of computational proof assistants over the last few decades has made it possible to do this in practice. The technology is firmly based on the methods and concepts of modern logic, and in many ways the practice represents the contemporary embodiment of the foundational tradition.
In this informal talk, I will provide a brief overview of interactive theorem proving and the body of logic that supports it. I will then discuss a particular theorem prover, Lean, its formal library, mathlib, which are attracting a growing community of mathematical users. The Lean community web pages provide a good starting point for more information: https://leanprover-community.github.io/.
About the speaker:
Jeremy Avigad is a Professor of Philosophy and Mathematical Sciences at Carnegie Mellon University. He received a B.A. in Mathematics from Harvard in 1989, and a Ph.D. in Mathematics from the University of California at Berkeley in 1995 under the supervision of Jack Silver. He has contributed to mathematical logic and foundations, proof theory, formal verification, interactive theorem proving, and the philosophy and history of mathematics.
Lecture series on Logic and foundations of mathematics (13)
Lecture Title: The journey from Peano Arithmetic to proof complexity
Speaker: Prof. Pavel Pudlák (Mathematical Institute of the Czech Academy of Sciences, Czech)
Date and Time: 2021-05-18, 16:00-18:00 Beijing Time (UTC 8:00-10:00)
Platform: Zoom (ID: 693 0929 0011, Password: 276109)
Organizer:
School of Philosophy, Wuhan University
Interlocutors:
Prof. Yue Yang (National University of Singapore)
Dr. Fedor Pakhomov (Ghent University, Belgium)
Host: Prof. Albert Visser (Utrecht University, Netherlands)
Abstract:
Proof complexity is a fast growing field connected to logic, computational complexity, and combinatrorial optimization. In order to fully understand the concepts and their importance, one should go to the roots of this field and follow its history. It started with investigations of the Hilbert school at the beginning of the 20th century, whose aim was to prove consistency and completeness of basic theories used in the foundations of mathematics. After the groundbreaking result of Godel in the 1930s, the incompleteness of Peano Arithmetic and any theory extending it, the focus turned to the study of fragments of Peano Arithmetic. With the advent of computational complexity theory in the 1970s, connections between weak fragments and complexity classes were discovered. Soon after that provability of certain sentences in weak fragments was connected with the existence of polynomial length propositional proofs of sequences of tautologies expressing these sentences in propositional logic. Another boost for the emerging field of proof complexity came from the realization that several heuristic used in combinatorial optimization could be viewed as propositional proof systems.
In this lecture we will briefly review the history and introduce basic concepts of proof complexity. After that we will demonstrate on a concrete example how one can prove an independence result using propositional proof complexity.
About the speaker:
Pavel Pudlák is a full professor in the Department of Mathematical Logic and Theoretical Computer Science at Mathematical Institute of the Czech Academy of Sciences. He is an expert in proof theory, especially on meta-mathematics of arithmetic and proof complexity, and has made many contributions in these fields. He is the author of the book “Logical Foundations of Mathematics and Computational Complexity, a gentle introduction” published by Springer in 2013. Pavel Pudlák is also the author (with P. Hájek) of the book “Metamathematics of first order arithmetic” published by Springer-Verlag/ASL Perspectives in 1993.
Lecture series on Logic and Foundations of Mathematics (14)
Title: Flexible Turing Machines
Speaker: Prof. Ali Enayat (Professor of Logic, University of Gothenburg, Sweden)
Time: 2021-06-15, 9:00-11:00 Beijing Time (UTC 1:00-3:00)
Platform: Zoom (ID: 698 4517 0856)
Organizer:
School of Philosophy, Wuhan University
School of Mathematics and Statistics, Wuhan University
Interlocutors:
Dr. Tin Lok Wong (School of Mathematics, National University of Singapore,Singapore)
Dr. Zachiri McKenzie (School of Philosophy, Zhejiang University, China)
Host: Prof. Yue Yang (School of Mathematics, National University of Singapore,Singapore)
Abstract:
Suppose T is a consistent r.e. (recursively enumerable) extension of Q (Robinson Arithmetic). A Turing Machine (hereafter TM) with program e is said to be T-flexible if for any prescribed natural number m, the theory T plus “on input 0, the output of the TM with program e is precisely the singleton {m}” is consistent. T-flexible TMs were first constructed by Kripke (1961). Note that here e is a concrete (standard) program. In 2011 Woodin introduced a new type of T-flexible TM for consistent r.e. extensions of PA (Peano arithmetic) such that: (1) T proves “on input 0, the output of the TM with program e is finite”, and (2) for every countable model M of T, and any M-finite set s extending the M-output of the TM with program e (when the input is 0), there is an end extension N of M satisfying T plus “on input 0, the output of the TM with program e is precisely s”. In this talk, I will (a) compare and contrast the aforementioned constructions of Kripke and Woodin, and (b) present a refinement of Woodin's theorem obtained in collaboration with Rasmus Blanck.
About the speaker:
Prof. Ali Enayat is a mathematical logician, with a strong interest in the metamathematics of foundational axiomatic systems such as Zermelo-Fraenkel set theory (ZF) and Peano arithmetic (PA). His current research is focused on the model theory of arithmetic, the model theory of set theory, and axiomatic theories of truth. He is academically affiliated with the University of Gothenburg (Sweden) as Emeritus Professor of Logic; his research is supported by the Polish National Science Centre, in connection with the project Epistemic and Semantic Commitments of Foundational Theories. Currently he serves as an editor of the Bulletin of Iranian Mathematical Society (BIMS), published by Springer; and the Bulletin of Symbolic Logic (BSL), published by Cambridge Univ. Press. Further information about his work can be found on his homepage:https://www.gu.se/en/about/find-staff/alienayat
Lecture series on Logic and Foundations of Mathematics (15)
Title: Cyclic Henkin Logic: Is there Life beyond Löb’s Third Condition?
Speaker: Prof. Albert Visser (School of Philosophy, Utrecht University, Netherlands)
Time: 2021-06-22, 16:00-18:00 Beijing time (UTC 8:00-10:00)
Platform: Zoom (ID: 651 4976 9146)
Organizer:
School of Philosophy, Wuhan University
Host:
Dr. David Fernández Duque (School of Mathematics, Ghent University, Belgium)
Interlocutors:
Dr. Junhua Yu (Department of Philosophy, Tsinghua University, China)
Prof. Joost J. Joosten (Department of Philosophy, University of Barcelona, Spain)
Abstract:
The third Löb Condition L3, to wit *provable* implies *provably provable*, is the most problematic of Löb's three conditions. There are theories and representations of the axiom set such that either we do not know how to verify L3 or we can actually show that it fails. Still, in many circumstances where L3 is lacking, both Gödel’s Second Incompleteness Theorem and the de Jongh-Sambin-Bernardi Theorem on the uniqueness of fixed points still hold.
In this talk, we study Cyclic Henkin Logic. In this logic we do have Löb’s Rule but we do not have L3. We cannot define modalised fixed points in the purely modal language, since the de Jongh-Sambin Theorem on explicit fixed points fails. There are several ways of adding fixed points to the language: as constants, using a variable-binding fixed point operator and by adopting a cyclic syntax. Cyclic Henkin Logic embodies the choice for a cyclic syntax. This choice is arguably the most beautiful one. The talk is an introduction to CHL. We will explain the syntax and prove some basic facts.If time allows, we will how CHL can be viewed as a fragment of the mu-Calculus.
About the speaker:
Prof. Albert Visser is a member of the Royal Netherlands Academy of Arts and Sciences. He was assistant professor at Stanford University and Utrecht University and Professor of Logic, the Philosophy of Mathematics and Epistemology at Utrecht University. Albert Visser is now professor emeritus at Utrecht University. His research centers on arithmetical theories, interpretability, constructivism, foundations of mathematics and topics in the philosophy of language. He served in various committees of the Association of Symbolic Logic.
You can watch the lecture videos via the official bilibili channel of School of Philosophy at Wuhan University:
https://space.bilibili.com/592450385/channel/detail?cid=158781
