2002 Fiscal Year Annual Research Report
| Project/Area Number |
14740064
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
鹿島 亮 東京工業大学, 大学院・情報理工学研究科, 助教授 (10240756)
|
|---|
| Keywords | 数理論理学 / シークエント計算 / 直観主義論理 / 構成的否定 |
|---|
| Research Abstract |
本年度は主に,直観主義論理の変種に対するシークエント計算体系を用いた,次の2つの結果を得た.
直観主義述語論理に「構成的否定(constructible falsity)」を加えた論理に関して,いくつかの自然な公理といくつかの自然なモデル条件が対応していること(完全性と健全性)を,「木状のシークエント」を用いたシークエント計算体系を用いて明らかにした.具体的には次のようになる.構成的否定を持つ論理のKripkeモデルは「可能世界の集まり」と,各可能世界に対する「変数を解釈する対象領域」,「肯定される論理式の集合」(以後Pと表記),「否定される論理式の集合」(以後Nと表記)によって定まる.これらに関する次の三条件それぞれに対して完全かつ健全になる公理を発見した.(1)各可能世界において集合PとNは交わらない.(2)各可能世界に対して,そこから到達可能で集合PとNの和集合が全体集合になるような世界が存在する.(3)各可能世界はすべて同じ対象領域を持つ(定領域条件).
直観主義述語論理に上記の定領域条件に対応する公理を付け加えた論理はCDという名前で知られている.「CDに対して良いシークエント計算体系を与えよ」という問題は古くから考えられ,いくつかの解が与えられている.本研究では,この有名な問題に対する新たな解の可能性を明らかにした.具体的には,論理式から項を作り出す文法的機能を導入し,それを使って「カット規則がなく,すべてのシークエントの右辺が単数であるシークエント計算体系」を定義し,これがCDに対して完全であることを証明した.しかし残念ながら,この体系はCDに対して健全でないことが判明した.
|
Research Products
(3 results)
-
[Publications] Ryo Kashima: "A cut-free sequent calculus with ε-symbols"Proceedings of the 36th MLG meeting at Kinosaki, Japan, 2002. 6-7 (2003)
-
[Publications] Ichiro Hasuo, Ryo Kashima: "A proof-theoretical study on logics with constructible falsity"京都大学数理解析研究所講究録. 1301. 92-121 (2003)
-
[Publications] Ryo Kashima: "On semilattice relevant logics"Mathematical Logic Quarterly. 49・4(予定). (2003)
