研究分担者
研究課題基本情報（最新年度）
研究期間
1998年度〜1999年度研究分野
審査区分
一般
研究種目
基盤研究(C)
研究機関
千葉大学
配分額
- 総額：3800千円
- 1998年度：2200千円 (直接経費：2200千円)
- 1999年度：1600千円 (直接経費：1600千円)
研究概要（最新報告）
1.近年ラムダ計算を介して,部分構造論理,直観主義論理,古典論理の研究が一体化しつつある。その中で鹿島(東京工大)と古典論理の自然演繹体系について研究した。鹿島は古典論理の新しい自然演繹体系を発見した。古森はそれを一部改良し体系CKを得た。体系CKは「ならば除去」,「割増」,「場合わけ」の3つの推論規則を持っている。この体系の発見はまったく新しいものであり,部分論理式特性を持つ古典論理の自然演繹体系の最初のもの(結論がいくつもあるのを認めるとParigotのものがある)である。体系CKについては更にChurch-Rosser性などを調べているところである。この結果は,数学で普通に使われている論理についての結果であるので,各方面から注目されている。
2.上記の結果は新しい計算方式を生んでいる。その計算方式については上で述べたChurch-Rosser性だけでなく,その意味なども調べている。
3.複数の結論を持つ自然演繹体系およびλμ計算とその周辺の研究は,藤田により活発に行なわれ本報告書の研究発表の欄にある二つの論文を生んでいる。
4.BB'IW論理の決定問題はrelevant論理最大の未解決問題であるので,研究代表者,分担者全員で解決にあたっているが,問題が難しくみるべく成果は得られていない。
5.金沢はカテゴリー文法について,それらの構文論的性質や意味論的性質をより明らかにするよう研究を進め成果を得ている。
6.桜井は,ラムダ計算のカテゴリーモデルについての研究を進め,構文論的な性質を証明するためのモデルの構成法について成果を得ている。
1. Recently lambda calculus unites studies of substructural logics, the intutionistic logic and the classical logic. In this context, Kashima has posed a Natural deduction system for the classical implicational logic. His system has three rules, the elimination of the implication, the introduction of the implication and the case rule. Komori has noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system TAμ from Kashima's system by replacing the introduction of implication by the weakening. While the type assignment system TAλgives a natural deduction for implicational intuitionistic logic, the type assignment system TAμgives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem α there exists a proof of α in TAμ enjoying the subformula property. Still more λ-calculus can be simulated in μ-calculus.
2. A new system of calculus comes out of the above result. We are investigating the meaning of the new calculus.
3. Fujita has actively studied on multiple-conclusion natural deduction system and λμ-calculus, and then has written many papers.
4. The problem on the decidablity of BB'IW logic in one of the most difficult mathematical problem. We are wrestling with the problem.
5. Kanazawa has investigated Categorial Grammars and has gotten excellent results.
6. Sakurai has investigated Categorical model of lambda-calculus and has written two good papers.
このページのURI
http://kaken.nii.ac.jp/ja/p/10640103