WIAS 主催セミナー: “Type Theory and Proof Theory”(3/16)
講演者 / Speaker
XU, Chuangjie (博士研究員, Ludwig-Maximilians-Universität München)
山﨑 紗紀子 (博士課程, 首都大学東京)
プログラム / Schedule
講演および質疑応答 (1) 13:20~14:20
講演者:XU, Chuangjie
タイトル: The computer as referee in mathematics
アブストラクト: 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.
講演および質疑応答 (2) 14:30~15:30
講演者:山﨑 紗紀子 (YAMASAKI, Sakiko)
タイトル:An attempt at a new embedding of intuitionistic logic into linear logic-via multi-succedent G3-style sequent calculus for intuitionistic logic-
アブストラクト: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
早稲田大学 早稲田キャンパス 26号館 11階 1102教室
主 旨 / 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
藤原 誠 (早稲田大学 高等研究所 助教)
秋吉 亮太(早稲田大学 高等研究所 准教授)
対 象 / Prospected Audience
学部生・大学院生・教職員・一般
言 語 / Language
英語
主 催 / Organizer
早稲田大学 高等研究所
申込み / Registration
事前申込み不要です。直接会場にお越しください。