Okada, Mitsuhiro

写真a

Affiliation

Faculty of Letters Department of Philosophy (Mita)

Position

Professor Emeritus

Related Websites

External Links

Profile 【 Display / hide

  • Towards clarifying logical thinking: An interdisciplinary,integrated research of logical reasoning Logic is one of the oldest forms of classical scholarship, and a great amount of research has been done since it was formulated by Aristotle in the 4th century BC. However, there are still a number of unresolved issues that remain in the study of logic and logical thinking in the 21st century. Through logic and logical research, I aim to clarify our understanding of how people think. In FY2013, I conducted multilateral logical research with a focus on philosopy, and from an intedisciplinary view including perspectives of mathematical logic, computational/informathion and cognitive science, neuroscience, and others. The main themes for the 2013 research were as found below. 1.Philosophical logic Presented a modern, re-evaluated perspectine of demonstration, computation theories, and philosophy of mathematics of such 20th century philosophers as Ludwig Wittgenstein and Edmund Husserl. 2.Cognitive science methods Began researching multi-attribute data design and presentathion(e.g.product catalogues)and decision-making by combining techniques from cognitive science(mainly eye tracking), social psychology and logical semantics. Moved foward with theoretical research and human subject research into diagrammatic reasoning and graphical reasoning theory. 3.Teoretical study of logical structure Researched basic logic theory known as linesr logic theory(a logic from which the distinction of the classical and intuitionistic logic emerges)with the aim of deconstructing it into a more basic set of logical inferences. 4.Behavioral genetics and logic, and decision-making Researched logical reasoning and rational decision-making through twin studies conducted with the behavioral genetics research group at Keio(the Ando lab). 5.Information logic and software science Researched logical methods of safety properties verification for software such as authentication(cryptographic communicathion) protocols. Much of the above research was conducted in the interdisciplinary research enviroment at the Global Research Center of Logic and Sensibility, for which I am currently serving as the head, as well as under the Next-Generation Research Projects program, the project of the Research Center for Thinking and Behavioral Judgement at Keio(Head:Prof.Ken Sekine), and the MEXT-funded research project, "Elucidation of the Neural Computation for Prediction and Decision Making". Finally, I cooperated with patner teams such as CNRS ans INRIA in France. My research in 2013 depended greatly on the help I received from collaborative partners both at Keio and beyond.

Other Affiliation 【 Display / hide

  • Research Center for Himan Intelligence、Keio University, Member

  • Global Research Center for Logic and Sensibility, Keio University, Director

  • Brain Science Research Institute, Tamagawa University, Brain Research institute, Visiting Professor

  • University of paris 1, institute of History and Philosophy of Science and Technology, Associate Member

Career 【 Display / hide

  • 1998.04
    -
    Present

    慶應義塾大学, 大学院文学研究科, 委員

  • 1996.04
    -
    Present

    慶應義塾大学, 文学部, 教授

  • 1990.09
    -
    1996.03

    慶應義塾大学, 文学部, 助教授

  • 2017.03
    -
    Present

    University of Paris-1, Institute of History and Philosophy of Science and Technology, Institute of History and Philosophy of Science and Technology, Associate Member

  • 2001.02

    University of Paris-1, (Pantheon-Sorbonne), Department of Philosophy, Professeur invite

display all >>

Academic Background 【 Display / hide

  • 1979.03

    The University of Tokyo, Faculty of Literature, 哲学科

    University, Graduated

  • 1983.03

    Keio University, Graduate School, Division of Letters

    Graduate School, Completed, Master's course

  • 1987.03

    Keio University, Graduate School, Division of Letters

    Graduate School, Completed, Doctoral course

Academic Degrees 【 Display / hide

  • 文学 , Keio University, Coursework, 1987.03

    弱い含意に制限した論理について

 

Research Areas 【 Display / hide

  • Philosophy/Ethics (Philosophy/Ethics / Philosophy of logic, Philosophy of mathematics,Wittgenstein, Informatic ethics, Psychology of decision making and logic, informatic logic)

Research Keywords 【 Display / hide

  • Computer security

  • Diagrammatic logic

  • Theoretical computer science

  • Philosophy of AI

  • Algorithmic ethics

display all >>

Proposed Theme of Joint Research 【 Display / hide

  • Logical reasoning, inference ability, decision making, logic and ethics of algorithm, decision making with diagrammatic-graphic representation by eyetracker and cognitive scientific measures

    Interested in joint research with other research organizations (including universities, etc.)

     View Message

    特に次のテーマに関して応用面に興味を持っている。1.論理推論の教育デザイン、論理推論略評価法、評価課題集などを開発してきた。
    2.図的・グラフィック情報提示に基づく意思決定・論理推論の研究地球蓄積を持ち、社会心理学的消費者行動意思決定への応用研究に関わる研究を進めている。

 

Books 【 Display / hide

  • Wittgenstein and Goodstein on Uniqueness of Primitive recursive arithmetic, in "Wittgenstein in the 1930s:Investigations to Philosophical Investigations" (ed. by David Stern)

    Mathieu Marion and Mitsuhiro Okada, Cambridge University Press, 2018.11

    Scope: Chapter authors

  • A Report of Reserch Center for Thinkingand and Behavioral Judgement

    Mitsuhiro Okada, Tatsuya Kashiwabata, Hisanori Tsuge, Juko Ando, Jun ichi Yamamoto, Takayuki Sakagami, Satoshi Umeda, Masao Ogaki, Hideo Akabayashi, Noburu Notomi, and Keiko Fujisawa., Research Centre for Thinking and Behavioral Judgment, Keio University, 2014.12

  • Effects of Representation Patterns in Multi-Attribute Decision-Making: An Eye-Tracking Study

    Masahiro Morii, Takashi Ideno, Shigetaka Okubo, and Mitsuhiro Okada, Research Centre for Thinking and Behavioral Judgment, Keio University, 2014.12

  • Eye-Tracking Study of Decision-Making with Graphically Represented Multi-Attribute Tables.

    Okubo,S.& Okada,M., Report of the Reserch Center for Thinking and Behavioral Judgement(ed.M.Okada et al.),Keio University, 2014

    Scope: 17-23

  • Logic and Cognition in Reasoning with Euler Diagrams: A Relational Perspective

    Mitsuhiro Okada, Global COE, GRALS, 2012

display all >>

Papers 【 Display / hide

  • Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

    GERGEI BANA, ROHIT CHADHA, AJAY KUMAR EERALLA, MITSUHIRO OKADA

    ACM Trans. Comput. Logic (Association for Computing Machinery)  to appear ( 1 )  2019.12

    Research paper (scientific journal), Accepted,  ISSN  15293785

     View Summary

    © 2019 Copyright held by the owner/author(s). In recent years, a new approach has been developed for verifying security protocols with the aim of combining the benefits of symbolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [8]. In this article, we argue that the real breakthrough of this technique is the recent introduction of its version for indistinguishability [9], because, with the extensions we introduce here, for the first time, there is a computationally sound symbolic technique that is syntactically strikingly simple, to which translating standard computational security notions is a straightforward matter, and that can be effectively used for verification of not only equivalence properties but trace properties of protocols as well. We first fully develop the core elements of this newer version by introducing several new axioms. We illustrate the power and the diverse use of the introduced axioms on simple examples first. We introduce an axiom expressing the Decisional Diffie-Hellman property. We analyze the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. We provide computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol formultiple sessions, without any restrictions on the computational implementation other than the DDH assumption. We also show authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, we axiomatize IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. We have formalized the axiomatic system in an interactive theorem prover, Coq, and have machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol.

  • Psychosocial Twin Cohort Studies in Japan: The Keio Twin Research Center (KoTReC)

    Ando J., Fujisawa K.K., Hiraishi K., Shikishima C., Kawamoto T., Nozaki M., Yamagata S., Takahashi Y., Suzuki K., Someya Y., Ozaki K., Deno M., Tanaka M., Sasaki S., Toda T., Kobayashi K., Sakagami M., Okada M., Kijima N., Takizawa R., Murayama K.

    Twin Research and Human Genetics (Twin Research and Human Genetics)  22 ( 6 ) 591 - 596 2019.12

    ISSN  18324274

     View Summary

    © The Author(s) 2020. The Keio Twin Research Center (KoTReC) was established in 2009 at Keio University to combine two longitudinal cohort projects - the Keio Twin Study (KTS) for adolescence and adulthood and the Tokyo Twin Cohort Project (ToTCoP) for infancy and childhood. KoTReC also conducted a two-time panel study of self-control and psychopathology in twin adolescence in 2012 and 2013 and three independent anonymous cross-sectional twin surveys (ToTcross) before 2012 - the ToTCross, the Junior and Senior High School Survey and the High School Survey. This article introduces the recent research designs of KoTReC and its publications.

  • On quasi-ordinal diagrams

    Mitsuhiro Okada and Yuta Takahashi

    38-49, EPTCS 288, Post-Workshop Proceedings of the 10th EOTCS Post-Proceedings of Workshop on Computation with Terms and Graphs (TermGraph 2018) (FEPTCS)     38 - 49 2019.03

    Research paper (international conference proceedings), Joint Work, Accepted

  • Following a Rule: Waismann's Version

    <UMarion Mathieu and Okada, Mitsuhiro(/)-#HR

    Publications of the Austrian Ludwig Wittgenstein Society – New Series (Austrian Ludwig Wittgenstein Society)   2019

    Research paper (international conference proceedings), Joint Work

  • On quasi ordinal diagram systems

    Okada M., Takahashi Y.

    Electronic Proceedings in Theoretical Computer Science, EPTCS (Electronic Proceedings in Theoretical Computer Science, EPTCS)  288   38 - 49 2019

    ISSN  20752180

     View Summary

    © M. Okada & Y. Takahashi. The purposes of this note are the following two; we first generalize Okada-Takeuti’s well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret’s version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz’s hydra game.

display all >>

Papers, etc., Registered in KOARA 【 Display / hide

display all >>

Reviews, Commentaries, etc. 【 Display / hide

  • Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68] (Theoretical Computer Science (2002) 272(1–2) (41–68), (S0304397500003479), (10.1016/S0304-3975(00)00347-9))

    Blanqui F., Jouannaud J.P., Okada M.

    Theoretical Computer Science (Theoretical Computer Science)  817   81 - 82 2020.05

    ISSN  03043975

     View Summary

    © 2000 Elsevier B.V. In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching definitions following a certain format, called the “General Schema”, which generalizes the usual recursor definitions for natural numbers and similar “basic inductive types”. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called “strictly positive”, and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

  • FATALIS: Real Time Processes as Linear Logic Specifications

    Koji Hasebe, V. Cremet, Jean-Pierre Jouannaud, Antonie Kremer, and Mitsuhiro Okada

    International Workshop on Automated Verification of Infinite-State Systems  2003

    Introduction and explanation (others), Joint Work

  • 歪んだ真珠(バロック)---音楽における規則性vs反規則性、または ロゴスvsパトス---

    岡田 光弘

    藝文研究  ( 9 )  2003

    Introduction and explanation (others), Single Work

  • 大会ワークショップ「フォーマルオントロジーの工学と哲学」報告

    日本科学哲学会   2002

    Other article, Single Work

  • うごめくウニは海の夢をみるか

    慶應義塾大学アートセンター 16   2-3 2001.10

    Other article, Single Work

display all >>

Presentations 【 Display / hide

  • Societal impacts of cybersecurity including elements relative to ethics, integrity, deontology and law

    Mitsuhiro Okada, Panelist

    The 5th France-Japan Workshop on Cybersecurity (Kyoto University) , 2019.04, Symposium, Workshop, Panelist (nomination), Keio University, NICT, French Embassy in Japan, INRIA, CNRS

  • normativity and rules

    OKADA MITSUHIRO

    French-Japanese Meeting on Philosophy of Logic and Mathematics, "rule, Normativity and Disagreement" (Keio University) , 2019.01, Symposium, Workshop, Panelist (nomination), French-japanese CNRA-Keio U Project

  • Formal language and logic

    Mitsuhiro Okada

    "Logic, Language and Ontology" Workshop (Keio University) , 2018.11, Oral Presentation(guest/special), "Logic, Language and Ontology" Workshop Organizing Committ

  • Why "formal" is needed for algorithmic ethics?

    Mitsuhiro Okada

    French-Japanese Meeting for Algorithmic Fairness, 2018.10, Oral Presentation(general)

  • A system of quasi-ordinal diagrams

    OKADA, MITSUHIRO-Takahashi,Yuta

    The 20th International Workshop on Computation with Terms and Graphs (Oxford) , 2018.07, Symposium, Workshop, Panelist (public offering), TermGraph2 018 Program Committee

display all >>

Research Projects of Competitive Funds, etc. 【 Display / hide

  • 論理的「不一致」の解明

    2020.01
    -
    2024.03

    MEXT,JSPS, Grant-in-Aid for Scientific Research, 岡田 光弘, Fund for the Promotion of Joint International Research (Home-Returning Researcher Development Research (B)), Principal Investigator

  • A New Development of "Philosophy of Logic and Mathematics" from the view point of "Philosophy of Proofs"

    2017.04
    -
    2022.03

    JSPS, Grant-in-Aid for Scientific Research, Mitsuhiro OKADA, Research grant, Principal Investigator

     View Summary

    We give new view points and new solutions to the fundamental issues in philosophy of logic and philosophy of mathematics

  • Information security research based on logical-formal methods-cruptographic protocols quantitative information flow analysys

    2016.04
    -
    2019.03

    JSPS, AYAME-Program (JSPS-INRIA), Mitsuhiro OKADA, Commissioned research, Principal Investigator

     View Summary

    Weare developing theory and techniques of "provabl" secure cryptographic protocols, by which security properties are logically-formally provable.

  • Interdisciplinary study on logical philosophy based on intuitionistic logic

    2014.04
    -
    2018.03

    JSPS, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal Investigator

     View Summary

    哲学・倫理学

     View Remarks

    基盤研究(B)

  • Logic and computation for prediction, judgment and decision making

    2011.07
    -
    2016.03

    JSPS, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal Investigator

     View Summary

    予測と意思決定の脳内計算機構の解明による人間理解と応用

     View Remarks

    新学術領域研究(研究領域提案型)

display all >>

Works 【 Display / hide

  • 飯田「ウィトゲンシュタイン」書評

    2000
    -
    Present

    Other, Single

     View Details

    左記図書の書評

  • 公と私(石黒ひで氏との対談)

    1999.05
    -
    Present

    Other, Single

     View Details

    左記テーマでの対談

  • 「脳と心のモデル(安西他著)」書評

    1994
    -
    Present

    Other, Single

     View Details

    左記図書の書評

  • 大出「論理学入門」について

    1992.11
    -
    Present

    Other, Single

     View Details

    左記図書についての書評

Other 【 Display / hide

  •  View Details

    <書評>ウィトゲンシュタイン:言語の限界 飯田隆著, 講談社, 1997年. 哲學, 104:77-83, 1999年12月.

 

Courses Taught 【 Display / hide

  • CONTEMPORARY LOGIC ISSUES 2

    2020

  • CONTEMPORARY LOGIC ISSUES 1

    2020

  • COMPUTATIONAL LOGIC

    2020

  • ADVANCED STUDIES IN PHILOSOPHY AND ETHICS 2I

    2020

  • ADVANCED STUDIES IN PHILOSOPHY AND ETHICS 1I

    2020

display all >>

 

Social Activities 【 Display / hide

  • 三田哲学会誌「哲学」

    1997.04
    -
    2000.03

Memberships in Academic Societies 【 Display / hide

  • Takeuti Symposium, 

    2003.12
  • Consciousness Meeting, 

    2003.12
    -
    Present
  • Workshop "Logic and Philosopy of Math", 

    2003.12
  • 「ヒルベルト・ワークショップ」, 

    2002.01
    -
    Present
  • 日仏情報学ワークショップ(フランス外務省主催), 

    2001.12
    -
    Present

display all >>

Committee Experiences 【 Display / hide

  • 2019.04
    -
    Present

    Chair of the Editorial Board, Philosophy of Science Society, Japan

  • 2019.01
    -
    Present

    大会実行委員会委員長, 日本科学哲学会

     View Remarks

    2018年大会委員長内定

  • 2017.04
    -
    Present

    理事会理事, 日本科学基礎論学会

  • 2017.04
    -
    Present

    理事会理事, 日本科学哲学会

  • 2016.01
    -
    Present

    Executive Committee Member (執行委員会委員) A, ssessor, Division of Logic, Methodology and Philosophy of Science and Technology, International Union of History and Philosophy of Science and Technology (国際科学・技術史科学・技術哲学学会連合)

display all >>