直観主義認識論理の証明論的研究

点击翻译按钮获取中文摘要

研究目的は、古典論理と直観主義論理の区別は認識論理の分野において、いかなる帰結をもたらすかということを証明論的に解明することである。本年度では、前年度の研究成果（直観主義認識論理IELの証明論的研究および、BHK解釈とKripke意味論の関連性研究）をまとめて学術雑誌Studia Logicaに投稿した。本年度では国内の分散知識を専門としている研究者と共同研究を展開して、直観主義認識論理IELの分散知識拡張について研究をした。予定していたラベル付き推件式ではなく、よりストレートな通常の推件式計算を採用した。直観主義認識論理IELの拡張として、分散知識を扱える直観主義認識論理DIELの体系を構築した。DIELにカット除去定理が成り立つような推件式計算を与えて、Criag補間定理などの結果を示した。さらに、推件式計算に対して健全かつ完全なKripke意味論を与えた。前年度の研究に基づいて、古典認識論理と直観主義認識論理の区別を特徴づけるためには、翻訳の手法よりは、古典論理にない直観主義論理の論理演算子に関するBHK解釈がより効果的であるということが明らかになった。そこで、本来予定していた分散的知識概念を持つ古典認識論理と直観主義認識論理の翻訳研究ではなく、分散知識のBHK解釈研究を実施した。具体的には、分散知識演算詞にBHK解釈を与えて、公理の有効性を確認した。まとめた研究結果を国際会議であるLORI2021で発表した。