Philosophy (Lecture): Topics in Mathematical Logic 2024 (1)/(2), one of the courses offered at the Hokkaido Summer Institute 2024 by the School/Graduate School of Humanities and Human Sciences, was taught over five days from September 2 to 6. Professor Katsuhiko Sano from the Laboratory of Philosophy and Ethics, and Senior Lecturer Tadeusz LITAK from the University of Erlangen–Nuremberg in Germany collaborated to deliver the course in person.
In this course, students learned how to use the theorem-proving support system Coq to prove theorems in first- and higher-order classical and intuitionistic logic while building on their basic knowledge and a certain level of proficiency in logic, under the guidance of Senior Lecturer Litak, an expert in the use of theorem-proving support systems, and Professor Sano of Hokkaido University.
In logic and mathematics, it is not uncommon for handwritten proofs on paper to contain gaps or errors, or for the verification of proofs to be extremely challenging due to an excessive number of case distinctions. A theorem-proving support system is software designed to assist in proving mathematical theorems. It is used to ensure the correctness of mathematical proofs, even those involving numerous case distinctions, and to guarantee the safety of software. The theorem-proving support system Coq, which was primarily used in this course, has also been utilized to verify the correctness of the proof of the four-color theorem, which states that “any map can be colored with four colors so that no adjacent regions share the same color.” This proof involved complex case distinctions.
The first lecture began with self-introductions by both instructors and students, who shared their respective topics of study, interests, and areas of focus. The majority of the participants were graduate students in doctoral or master’s programs specializing in logic.
The lectures began with an introduction of Coq and theorem-proving support systems, covering topics such as Curry-Howard correspondence and comparisons between logic and type theory. The course progressed through a combination of lectures and exercises led by Senior Lecturer Litak. Professor Sano also participated in the exercises with the students, reviewing their work (code) together with Senior Lecturer Litak.
Senior Lecturer Litak, who has extensive experience living in Japan, delivered humorous lectures that occasionally included some Japanese expressions. The students spent five days in a privileged environment where they could receive thorough instruction in a small-group setting. They gradually learned about Curry-Howard correspondence, dependent type theory, viewing proofs as programming, and the appropriate use of theorem-proving support systems.
According to Senior Lecturer Litak, mastering the content covered in this course in one leap is extremely challenging, and it is important to take the time to gradually internalize what has been learned.
