WIAS Seminar :
“The epsilon calculus with equality predicate and Herbrand complexity” (September 10)
講演者 / Speaker
MIYAMOTO, Kenji （Research Assistant, University of Innsbruck）
日 時 / Date & Time
Monday, 10 September 2018, 16:00 – 17:30
会 場 / Venue
Meeting room #1 on the 5th floor, Building #9, Waseda University
主 旨 / Outline
証明論や計算理論に関わる先端研究をしている宮本賢治氏 (インスブルク大学，博士研究員)にご自身の研究に関する講演をしていただくことにより，当該分野の研究者間の研究交流を図ると共に，国内で関連分野を学ぶ人々(大学院生等)に先端研究を知る機会を提供する．
プログラム / Schedule
16:00～17:00 Presentation (in English)
17:00～17:30 Question-and-answer session
(Abstract)
Hilbert’s epsilon-calculus is based on an extension of the language of predicate logic by a term-forming operator $\varepsilon$ [1]. Two fundamental results about the epsilon-calculus, the first and second epsilon theorem, play a role similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand’s Theorem is a consequence of the epsilon theorems. Moser and Zach study the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure [2].We extend their results to epsilon-calculus with equality predicate. This is joint work with Georg Moser.
[1] D. Hilbert and P. Bernays, Grundlagen der Mathematik, vol. 2, Springer Berlin, 1939.
[2] G. Moser and R. Zach, The epsilon calculus and Herbrand complexity, Studia Logica, vol. 82 (2006), no. 1, pp. 133–155.
コーディネーター / Coordinator
FUJIWARA, Makoto (Assistant Professor, Waseda University)
言 語 / Language
English
対 象 / Prospected Audience
Faculty and staff members of a university, grad students
主 催 / Organizer
Waseda Institute for Advanced Study, Waseda University
申込み / Registration
Free of charge. Please come to the event venue directly.
