学位

• 博士（哲学）(慶應義塾大学 2010.3)

経歴

学歴

受賞

• 「言語処理学会第29回年次大会」委員特別賞
• 2013年度科学基礎論学会奨励賞
• 2008年度科学基礎論学会奨励賞

その他

• Workshop: “Self and Infinity II”（京都大学）（共同オーガナイザー）
• Workshop: “Self and Infinity”（フッサール文庫、パリ）（共同オーガナイザー）
• Second Workshop on Mathematical Logic and its Application（金沢，日本学術振興会研究拠点形成事業「数理論理学とその応用の国際拠点形成」 の一環） (共同オーガナイザーおよびプログラム委員)
• WIAS 主催セミナー "Type Theory and Proof Theory" （早稲田大学）（共同オーガナイザー）
• WIAS Top Runners' Lecture Collection "Proof Theory and Computation (1) and (2)" （早稲田大学）（共同オーガナイザー）
• 早稲田大学高等研究所主催 「論理学の哲学」ワークショップ：意味，証明，推論 （早稲田大学）（オーガナイザー）
• 早稲田大学 高等研究所・慶應義塾大学 論理と感性のグローバル研究センター 共催 「論理と数学の哲学」 Workshop “Logic and Philosophy of Mathematics" （慶應義塾大学，早稲田大学）（共同オーガナイザー）
• 高等研究所セミナー 「Logic and Game Theory」（早稲田大学）（共同オーガナイザー）
• 「論理と数学の哲学—論証の哲学に向けて」日仏ワークショップ Workshop “Philosophy of logic and Mathematics -- Towards Philosophy of Proofs" （慶應義塾大学）(共同オーガナイザー)
• 早稲田大学高等研究所主催ワークショップ ``Philosophy of Logic Workshop: Kant, Husserl, and Linear Logic" 「論理学の哲学ワークショップ：カント，フッサール，線型論理」（早稲田大学）(オーガナイザー)
• 早稲田大学高等研究所セミナー「可換環における逆数学」（早稲田大学）（オーガナイザー）
• 早稲田大学高等研究所セミナー Philosophy of Mathematics and Logic Seminar （早稲田大学）(オーガナイザー)
• 「数学の哲学と証明論」ワークショップ "Philosophy of Mathematics and Proof Theory" Workshop （慶應義塾大学）（共同オーガナイザー）
• 早稲田大学高等研究所 Top Runners' Lecture Collection 数学の哲学ワークショップ「計算，証明，直観」（早稲田大学）（オーガナイザー）
• 早稲田大学高等研究所セミナー "Phase transitions in logic: combinatorics and provability" （早稲田大学）（オーガナイザー）
• GCOE ロジックセミナー 江口直日（東北大学）講演会 （慶應義塾大学）（共同オーガナイザー）
• 数学の哲学セミナー 金子洋之（専修大学），高橋優太（慶應大学）講演会（慶應義塾大学）（共同オーガナイザー）
• Richard Zach（カルガリー大学）講演会 "The Epsilon Calculus" （慶應義塾大学）（共同オーガナイザー）
• 国際会議 "Proof Theory and Philosophy"「証明論とその展開シンポジウム」（慶應義塾大学）（共同オーガナイザー）
• 論理学・数学の哲学セミナー 伊藤遼（京都大学），大西琢朗（京都大学）講演会（慶應義塾大学）（共同オーガナイザー）
• Bob Hale（シェフィールド大学）講演会 "What is absolute Necessity?" （慶應義塾大学）（共同オーガナイザー）
• Arguing for contradictions: dialectical gamesi n Plato's dialogues （慶應義塾大学）（共同オーガナイザー）
• Akihiro Kanamori（ボストン大学）, Juliet Floyd（ボストン大学） 講演会 （慶應義塾大学）（共同オーガナイザー）
• 矢田部俊介（産業技術総合研究所）講演会「真理の度合い理論は適切か？」（慶應義塾大学）（共同オーガナイザー）
• 国際会議 "A Proof Theory Workshop with Lecture Series by Grigori Mints"（慶應義塾大学）（共同オーガナイザー）

論文

• A Note on Feferman and Takeuti II: Philosophical Perspectives on Inductive Definitions
• Annotation of Japanese Discourse Relations Focusing on Concessive Inferences
• A Note on Feferman and Takeuti: Their Thoughts on Predicativity and Finitism
• 逆接の推論関係に着目した日本語談話関係アノテーション [Othres link]
• Foundations of Mathematics a la Kyoto School: from Nishida to Takeuti via Suetsuna [Othres link]
• Logic of Alternative-I [DOI] [Othres link]
• 竹内の整礎性証明再訪 [Othres link]
• Takeuti’s proof-theory in the context of the Kyoto school [Othres link]
• A Formalization of Brouwer's Argument for Bar Induction [DOI]
• An Interpretation of Brouwer’s Argument for Bar Induction via Infinitary Proof Theory [DOI]
• Contentual and Formal Aspects of Gentzen's Consistency Proofs [Othres link]
• An Ordinal-Free Proof of the Complete Cut-Elimination Theorem for Π11-CA + BI with the ω-rule [Othres link]
• Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule [DOI]
• An Extension of the Omega-Rule [DOI]
• 鈴木俊洋『数学の現象学』に関するいくつかのリマーク [Othres link]
• Brouwer’s Argument for the Bar Induction Revisited
• ブラウワーのバー帰納法における基本仮定の理解に向けて [CiNii Research (CiNii Articles)] [CiNii Books] [Othres link]
• ゲンツェンを読むー三つの無矛盾性証明の統一的解釈ー（2013年度科学基礎論学会奨励賞受賞論文） [DOI] [CiNii Research (CiNii Articles)] [CiNii Books] [Othres link]
• 非可述性の分析としての証明論(<特集>あたらしい数理論理学の揺籃:証明論的な順序数と集合論的な順序数) [DOI] [CiNii Research (CiNii Articles)] [CiNii Books] [Othres link]
• An Extension of the Iterated Omega-Rule
• Gentzen's First Consistency Proof Revisited
• Tait's Conservative Extension Theorem Revisited [DOI]
• An Ordinal-Free Proof of the Cut-elimination Theorem for a Subsystem of \Pi^1_1-Analysis with omega-rule [CiNii Research (CiNii Articles)] [CiNii Books] [Othres link] [Othres link]
• Proof-Theoretic Investigations of Type Theory and Subsystems of Second-Order Arithmetic [Othres link]
• Takeuti's Reduction and Impredicativity
• On a Relationship between Goedel's Second Incompleteness Theorem and Hilbert's Program（2008年度科学基礎論学会奨励賞受賞論文） [DOI] [CiNii Research (CiNii Articles)] [CiNii Books] [Othres link]
• ヒルベルトとゲーデル

その他業績

• Towards proof-theoretic semantics for second-order logic
• Intuition in philosophy of mathematics
• Schwichtenberg’s Style Analysis of Parameter-Free Fragments of Girard’s System F
• The logic of presence
• Husserl and Schroeder
• Toward an Alternative to the Master-Slave Model: A View from East Asia
• On Gaisi Takeuti's Philosophy of Mathematics (abstract)
• "Proofs as Programs" Revisited (abstract)
• The Upperbound of the Length of the Reductions in a Subsystem of Girard's F
• A uniform idea behind Gentzen’s three consistency proofs (abstract)
• Proof-Theoretic Analysis of Brouwer's Argument of the Bar Induction (abstract)
• An Interpretation of Brouwer's Argument for Bar Theorem via Infinitary Proof Theory (abstract)
• Complete Cut-Elimination Theorem for Ω-Rule (abstract)
• これからの数学・論理学の哲学に向けて
• An Ordinal-Free Proof of the Cut-elimination Theorem for Π11-CA with ω-rule (abstract)
• 書評：『ゲーデルの２０世紀の論理学③不完全性定理と算術の体系』（田中一之編，東京大学出版会） [CiNii Research (CiNii Articles)] [CiNii Books] [Othres link]

講演・口頭発表等

• Annotation of Japanese Discourse Relations Focusing on Concessive Inferences
• Intuition in Kant, Fichte and Nishida
• Takeuti on finite and infinite sets
• 逆接の推論関係に着目した日本語談話関係アノテーション
• Towards Proof-Theoretic Semantics for Second-Order Logic
• ロボット倫理学における「主人-奴隷」モデルのオルタナティブの必要性：Navonを手がかりに
• スマートシティのELSI研究の紹介：具体的な調査を中心に
• 東アジア的自己観から多層的社会へ
• フッサールとシュレーダー
• Takeuti’s finitism in the context of the Kyoto school
• Takeuti’s argument of the well-foundedness of ordinals up to the epsilon_0
• Takeuti’s finitism in the context of the Kyoto school
• Takeuti’s Finitism Revisited
• On Gaisi Takeuti's philosophy of mathematics
• On Gaisi Takeuti's philosophy of mathematics
• 飯田氏の論理学・数学の哲学をめぐって
• On Takeuti's Finitism
• Takeuti’s Finitism Revisited
• Disagreement on Brouwer’s Argument for Bar Induction
• 形式主義の新展開に向けてー竹内外史を手がかりにー
• ゲンツェンとシュッテのカット消去法
• "Proofs as Programs" Revisited
• "Proofs as Programs" Revisited
• "Proofs as Programs" Revisited
• Gentle Introduction to the Omega-Rule: Part II
• A Formalization of Brouwer's Argument for Bar Induction
• Gentle Introduction to the Omega-Rule: Part I
• Brouwer's Argument of Bar Induction Revisited
• Strong normalization for the parameter-free subsystem of System F based on the Omega-rule
• Opening Remarks
• On Brouwer’s argument of bar induction
• Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule
• Contentual and Formal Aspect of Gentzen's Consistency Proofs
• Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule
• Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule
• ヒルベルト，ブラウワーからゲンツェンへ
• Opening Remarks
• Some Results in Proof-Theory for Pi11-CA
• A Uniform Idea behind Gentzen's Three Consistency Proofs
• A Constructive Justification of Brouwer’s Bar Induction
• 直観主義へのいざない
• An Interpretation of Brouwer's Argument of the Bar Induction via Infinitary Proof Theory
• Brouwer's Argument of the Bar Induction Revisited
• “Logical Inference and Proofs” Franco- Japanese Workshopにおけるゲストコメンテイター
• Ω-規則の拡張と応用
• ブラウワーを証明論的に読む
• ブラウワーのバー帰納法の証明論的分析
• 特別企画 鈴木俊洋『数学の現象学』合評会におけるコメンテイター [Othres link]
• Proof-Theoretic Analysis of Brouwer’s Argument of the Bar Induction
• An Introduction to Proof Theory of First- Order Arithmetic
• Proof-Theoretic Analysis of Brouwer’s Argument of the Bar Induction
• ブラウワーの基本仮定について [Othres link]
• "Philosophy of Mathematics and Logic” Meetingにおけるゲストコメンテイター
• Brouwer’s Proof of the Bar Induction Revisited
• An Interpretation of Brouwer’s Argument for the Bar Induction via Infinitary Proof Theory [Othres link]
• Proper Explanation of Brouwer's Fundamental Assumption
• Brouwer’s proof of the bar induction revisited
• Cut-Elimination for Pi^1_1-CA
• 余帰納法の証明論への応用：Ω 規則の観点から
• An extension of the Ωμ+1-rule
• 形式主義の再検討に向けて
• Ω 規則の拡張について
• Complete Cut-Elimination Theorem for Ω-Rule
• 非可述性の分析としての証明論
• 順序数を用いない証明論について
• ゲンツェンの無矛盾性証明再訪
• Finite Notations for Ωμ+1-rule
• Introduction to Proof Theory for Impredicative Systems (Tohoku University)
• An Interpretation of Takeuti’s Reduction
• Finite Notations for Ωμ-rule
• 証明論的手法による二階論理の論理哲学的研究
• 竹内の還元法と非可述性について
• An Ordinal-Free Proof of the Cut-Elimination Theorem for Pi^1_1-CA with ω-rule
• 証明論的手法による二階論理の論理哲学的探究
• An ordinal-free proof of the cut-elimination theorem for Pi^1_1-analysis with ω-rule
• 順序数を用いないカット消去定理の証明について
• An ordinal-free proof of the cut-elimination theorem for Pi^1_1-analysis with ω-rule
• 非可述な体系のカット消去定理の順序数を用いない証明について
• An ordinal-free proof of the cut-elimination theorem for Pi^1_1- analysis with ω-rule
• On a relationship between cut-elimination proofs by W. Tait and W. Buchholz
• テイトの保存拡大定理について
• テイトの保存拡大定理について
• 第二不完全性定理とヒルベルト・プログラム

書籍等出版物

• 現代論理学事典
• ドイツ哲学・思想事典
• よくわかる哲学・思想

作品等

共同研究・競争的資金等の研究課題

• 無限を巡る日本の数理哲学の再検討：竹内、末綱、西田を中心に
• 論理と深層学習の統合的視点に基づくリーズニングの学際的研究
• よりよいスマートWEを目指して：東アジア人文社会知から価値多層社会へ
• コミュニティのスマート化がもたらすELSIと四次元共創モデルの実践的検討
• 形式主義の哲学の新展開：竹内外史の論理哲学の解明を通じて
• 「証明の哲学」の視点に立つ「論理と数学の哲学」の新展開
• ブラウワー直観主義の証明論的手法による再検討
• フレーゲ論理学の証明論的および意味論的研究
• 「形式主義の証明論的手法による再検討」
• ゲーデルの不完全性定理以降の形式主義の再検討
• 「形式主義と直観主義の証明論的手法による比較再検討」
• 「証明論的手法による二階論理の論理哲学的研究」
• 「タイプ理論の証明論的分析」

メディア報道

産業財産権

所属学協会

• Association for Symbolic Logic
• 日本科学哲学会
• 科学基礎論学会

委員歴

担当経験のある科目

• Topics in History and Philosophy of Science
• 哲学特殊講義
• 論理学入門（文学部設置）
• Topics in Philosophy and Religion
• Introduction to Logic
• 論理的思考のすすめ
• ことばと論理Ａ・B
• 哲学倫理学特殊
• 記号論理学 II
• 情報数理学続論
• 数学の哲学
• 哲学A
• 記号論理学 I
• 論理学概論 A・B
• Advanced Topics in Philosophy of Science
• 論理学
• 哲学専門講義（英米哲学／現代哲学）
• 論理学入門（理工学部設置）

社会貢献活動

学術貢献活動