WIAS主催セミナー :
“The epsilon calculus with equality predicate and Herbrand complexity” (9/10)
講演者 / Speaker
宮本 賢治 （インスブルク大学 博士研究員）
日 時 / Date & Time
2018年9月10日（月） 16:00～17:30
会 場 / Venue
主 旨 / Outline
証明論や計算理論に関わる先端研究をしている宮本賢治氏 (インスブルク大学，博士研究員)にご自身の研究に関する講演をしていただくことにより，当該分野の研究者間の研究交流を図ると共に，国内で関連分野を学ぶ人々(大学院生等)に先端研究を知る機会を提供する．
プログラム / Schedule
16:00～17:00 講演 （*英語で行います）
17:00～17:30 質疑応答
(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
藤原 誠 （早稲田大学 高等研究所 講師）
言 語 / Language
英語
対 象 / Prospected Audience
大学院生・教職員
主 催 / Organizer
早稲田大学 高等研究所
申込み / Registration
事前申込み不要です。直接会場にお越しください。
