WIAS Seminar: “Type Theory and Proof Theory” (March 16)
Speakers
XU, Chuangjie (Postdoctoral Researcher, Ludwig-Maximilians-Universität München)
YAMASAKI, Sakiko (Doctoral Student, Tokyo Metropolitan University)
Schedule
Presentation and Question-and-answer session (1) 13:20-14:20
Speaker: XU, Chuangjie
Title: The computer as referee in mathematics
Abstract: Proofs in modern mathematics now cover hundreds (and soon thousands) of pages, with additional computer calculations worth gigabytes of data. Given that no referee (or even team of referees) can reliably judge the correctness of such a proof, how should mathematics as a field proceed? I will discuss one way forward, namely the use of Martin-Loef’s constructive type theory and the associated proof assistants (like Agda and Coq) to formalise and verify the correctness of proofs, and to execute proofs as computer programs. During the talk I will use the Agda proof assistant for demonstration.
Presentation and Question-and-answer session (2) 14:30-15:30
Speaker: YAMASAKI, Sakiko
Title: An attempt at a new embedding of intuitionistic logic into linear logic－via multi-succedent G3-style sequent calculus for intuitionistic logic－
Abstract: In this presentation, I will examine the relationship between linear logic and G3-style sequent calculus for intuitionistic logic. It is well known that intuitionistic logic can be embedded into linear logic (Girard embedding). It is natural to do so, because intuitionistic logic can be embedded into modal logic S4 (Gödel embedding), and the behavior of exponentials for linear logic (! and ?) is similar to that of the modal operators for S4 (□ and ◇). Here, it is important for us (1) which system of intuitionistic logic is to be adopted, and (2) that the proof of the embedding is properly proof-theoretic one. For this purpose, we would like to employ the multi-succedent cut-free G3-style sequent calculus for intuitionistic logic: G3Int. I have already shown that we can establish the proof-theoretic proof for Gödel embedding via G3Int. Now, how about Girard embedding? In this presentation, I will propose a new translation. And I shall investigate this matter. Furthermore, as far as I can, I will examine the relationship between Gödel embedding and Girard embedding.
References:
A.S. Troelstra. Lectures on Linear Logic, CSLI-Lecture Notes 29,
Center for the Study of Language and Information, Stanford, California, 1992.
A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory. 2nd edn. Cambridge University Press, 2000.
Venue
Rm. 1102 on the 11th floor, Building #26, Waseda University
Outline
In this seminar, we have two talks on the advanced research with respect to type theory and proof theory in mathematical logic.
The prospected audience are graduate students and researchers who have basic knowledge about them.
Coordinator
FUJIWARA, Makoto (Assistant Professor, Waseda University)
AKIYOSHI, Ryota (Associate Professor, Waseda University)
Prospected Audience
Faculty and staff members of a university, grad students, undergraduates, the general publics
Language
English
Organizer
Waseda Institute for Advanced Study, Waseda University
Registration
Free of charge. Please come to the event venue directly.
