早稲田大学の藤原誠です。 先日ご案内させていただいた早稲田大学高等研究所 / 慶應義塾大学論理と感性のグローバル研究センター共催 「Workshop in Logic and Philosophy of Mathematics」 について最新の情報を流させていただきます。 14日15日ともに参加自由です。 どうぞふるってご参加ください。

-------------------------------------------------------------------

We apologize if you receive this message more than once.

---------------------------------------------------------------------

We announce the following “Workshop in Logic and Philosophy of Mathematics”.

The first day is at Mita campus of Keio University and the second day is at Waseda campus of Waseda University.

7月14日は慶應義塾大学三田キャンパス、7月15日は早稲田大学早稲田キャンパスでの開催になりますのでご注意下さい。

----

Workshop in Logic and Philosophy of Mathematics

Date: July 14 (Fri) and 15 (Sat), 2017

日時: 2017年7月14日(金), 7月15日(土)

Place: G-Lab, 6th floor, East Building, Mita campus of Keio University (14th); Meeting Room #1, 5th Floor, Bldg. 9, Waseda campus of Waseda University (15th).

場所: 慶應義塾大学三田キャンパス東館6階G-Lab (14日); 早稲田大学早稲田キャンパス9号館5階第一会議室 (15日).

For more details, please see the following page: 詳細は以下をご覧ください。 https://www.waseda.jp/inst/wias/news/2017/07/04/4467/

----

Program:

1. July 14 (Friday, G-Lab, 6th floor, East Building, Mita campus of Keio University):

Time: 13:00-18:00

Speakers: Andrew Arana (Université Paris 1 Panthéon-Sorbonne, IHPST), Kengo Okamoto (Tokyo Metropolitan University), Ryota Akiyoshi (Waseda University), Makoto Fujiwara (Waseda University) The details will be announced soon at the following page: https://abelard.flet.keio.ac.jp/jindex.php https://abelard.flet.keio.ac.jp/jindex.php

2. July 15 (Saturday, Meeting Room #1, 5th Floor, Bldg. 9, Waseda Campus of Waseda University)

Talk 1: 13:00-14:00 Ryoma Shinya (The University of Tokyo) Title: Almost every simply typed λ-term has a long β-reduction sequence Abstract: It is well known that the length of a β-reduction sequence of a simply typed λ-term of order k can be huge; it is as large as k-fold exponential in the size of the λ-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed λ-terms have very long reduction sequences? We provide a partial answer to this question, by showing that asymptotically almost every simply typed λ-term of order k has a reduction sequence as long as (k − 2)-fold exponential in the term size, under the assumption that the arity of functions and the number of variables that may occur in every subterm are bounded above by a constant. The work has been motivated by quantitative analysis of the complexity of higher-order model checking.

Talk 2: 14:00-15:00 Taishi Kurahashi (National Institute of Technology, Kisarazu College) Title: On partial disjunction properties of theories containing PA Abstract: It is well-known that intuitionistic predicate logic and Heyting Arithmetic have the disjunction property (DP). For intuitionistic logic, DP seems to reflect its constructivity. In classical logic, DP plays a different role. If a theory T in classical logic has DP, then T is complete because the law of excluded middle is valid. Thus in classical logic, every \Sigma_1-definable consistent extension of Peano Arithmetic PA does not have DP by the Gödel–Rosser first incompleteness theorem. On the other hand, PA enjoys a partial disjunction property. Let \Gamma be a class of formula. We say that a theory T has the \Gamma-disjunction property (\Gamma-DP) iff for any \Gamma sentences \varphi and \psi, at least one of \varphi or \psi is provable in T whenever \varphi \lor \psi is provable in T. It is known that PA has \Sigma_1-DP but does not have \Pi_1-DP. In this talk, we present several results concerning partial disjunction properties and other related properties of theories containing PA which is not necessarily \Sigma_1-definable.

Talk 3: 15:20-16:20 Naosuke Matsuda (Kanagawa University) Title: Some extensions of de Jongh's theorem Abstract: It is obvious that if a propositional formula A is provable in intuitionistic propositional calculus, then each arithmetical instance is provable in Heyting Arithmetic. The converse of this statement is known as de Jongh's theorem. In this talk, I give an introduction to de Jongh's theorem and introduce some extensional works.

Talk 4: 16:20-17:20 Masahiko Sato (Kyoto University) Title: A common notation system for lambda calculus and combinatory logic Abstract: We present a notation system which can be used to faithfully represent both the terms of lambda calculus and combinatory logic. We show the faithfullness of the representations by observing that the representations respect the beta and eta reduction rules. We also argue that Curry's Last Problem (J.R.Hindley, Curry's Last Problem: Imitating lambda-beta-reduction in Combinatory Logic) in its original form is an ill-posed problem, and can be solved naturally by expressing the problem in our notation system.

---------------------------------------------------------------------

Organizers:

Ryota Akiyoshi (Waseda Institute for Advanced Study, Waseda University)

Makoto Fujiwara (Waseda Institute for Advanced Study, Waseda University)

Mitsuhiro Okada (Global Research Center for Logic and Sensibility, Keio University)

Co-host: Waseda Institute for Advanced Study (Waseda University), Global Research Center for Logic and Sensibility (Keio University)

Contact: Ryota Akiyoshi [email protected] mailto:[email protected]

============================================ 藤原 誠 (Makoto Fujiwara) 早稲田大学高等研究所 (Waseda Institute for Advanced Study, Waseda University) E-mail: [email protected] ============================================