ゲンツェンの証明論的手法を用いたブラウワーの知識論および言語論の再構築

用根岑的证明理论方法重建布劳尔的知识和语言学理论

• 批准号: 16J04925
• 负责人: 高橋 優太
• 金额: $ 1.83万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2016
• 资助国家: 日本
• 起止时间: 2016-04-22 至 2019-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-16J04925/
• 关键词: 論理学の哲学; 数学の哲学; 数学基礎論; 数理論理学; 証明論的意味論; 情報の哲学; 知識の哲学; 言語の哲学; 論理学

本研究課題は、現代論理学の一分野であるゲンツェン的証明論を用いて、ブラウワーによる知識論・言語論を発展させ、知識および言語を巡る数理哲学上の問題にアプローチすることである。最終年度となる本年度は次の研究(1a),(1b),(2),(3)を行なった。(1)ゲンツェン的証明論についての更なる探究：(1a)ゲンツェンによる無矛盾性証明の拡張となる解析学の無矛盾性証明のために、竹内外史により導入された順序図形(ordinal diagrams)について、項書換え(term rewriting)の観点から研究を行なった。本研究は慶應義塾大学文学部教授・岡田光弘氏との共同研究で進められた。(1b)ゲンツェン的証明論の先駆的理論であるヒルベルトのε計算を精査した。特に、アッカーマンによるε計算を用いた算術の無矛盾性証明、および、G・ミンツによるその現代的発展形を詳しく調べた。(2)ゲンツェン的証明論からブラウワーの知識論・言語論へ：ゲンツェン的証明論とブラウワーの知識論・言語論を結びつけるために、2階直観主義命題論理に対して、ゲンツェン的証明論に基づく意味論である証明論的意味論(proof-theoretic semantics)を構築した。本研究は日本大学商学部准教授・竹村亮氏との共同研究で進められた。(3)ゲンツェン的証明論によるブラウワーの知識論・言語論の展開：まず、ゲンツェン的な枠組みの中で定式化される局在論理(local logic)を扱うバーワイズおよびセリグマンによるチャンネル理論(channel theory)に着目した。そして、受入研究者である戸田山和久教授との議論を通して、証明行為が担う情報をチャンネル理論でもって表現し、エージェントの認識状態に対してきめの細かい分析を与えるブラウワー的知識モデル・言語モデルを構成するというアイデアが得られた。

The topic of this study is the application of proof theory in modern logic, the development of knowledge theory and speech theory, and the problem of mathematical philosophy. The final year is the year of research (1a),(1b),(2),(3). (1)Exploration of the theory of proof in Gundantinn: (1a) The expansion of non-contradictory proof in Gundantinn, the research of the introduction of ordinal diagrams and the focus of term rewriting in Takeuchi and external history. This research is conducted jointly by Professor Hiroshi Okada, Faculty of Literature, Keio University. (1b)The proof of the theory of Special, (2)The theory of proof of the theory of knowledge and the theory of speech: the theory of proof of the theory of knowledge and the theory of speech: the theory of proof of the theory of knowledge and the theory of speech: the theory of proof of the theory of knowledge and the theory of speech: the theory of proof of the theory of proof. This study is a joint study by Ryoshi Takemura, Associate Professor, Faculty of Business, Nihon University. (3)The development of knowledge theory and speech theory in the proof theory of Professor Kazuhisa Toda's comments were communicated to prove that behavior was responsible for information generation theory, performance analysis, and cognitive state analysis.

项目成果

Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms

二阶直觉命题逻辑关于证明项阶段语义的完备性

• DOI: 10.1007/s10992-018-9484-z
• 发表时间: 2018
• 期刊: Journal of Philosophical Logic
• 影响因子: 1.5
• 作者: Kana GOTO;Hiroki NAKAMOTO;Shiro MORI;Yuta Takahashi and Ryo Takemura
• 通讯作者: Yuta Takahashi and Ryo Takemura

On Quasi Ordinal Diagram Systems

关于拟序数图系统

• DOI: 10.4204/eptcs.288.4
• 发表时间: 2019
• 期刊: Electronic Proceedings in Theoretical Computer Science
• 作者: ○杉山在生人;梅津光央;中澤光;熊谷泉;Okada Mitsuhiro and Takahashi Yuta
• 通讯作者: Okada Mitsuhiro and Takahashi Yuta

Ordinal Diagrams and Well-Quasi-Orderings (preliminary report)

序数图和准排序（初步报告）

• 发表时间: 2018
• 作者: Yuta Takahashi;高橋優太;Yuta Takahashi;高橋優太;Mitsuhiro Okada and Yuta Takahashi;Mitsuhiro Okada and Yuta Takahashi
• 通讯作者: Mitsuhiro Okada and Yuta Takahashi

Contentual and Formal Aspect of Gentzen's Consistency Proofs

Gentzen 一致性证明的内容和形式方面

• 发表时间: 2016
• 作者: Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi and Grigori Mints;Ryota Akiyoshi and Kazushige Terui;Ryota Akiyoshi and Yuta Takahashi;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi;秋吉亮太;秋吉亮太;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi;Ryota Akiyoshi and Yuta Takahashi
• 通讯作者: Ryota Akiyoshi and Yuta Takahashi

On a disagreement about the finiteness of Gentzen's 1935 consistency proof for first-order arithmetic

关于 Gentzen 1935 年一阶算术一致性证明的有限性的分歧

• 发表时间: 2019
• 作者: Yuta Takahashi