研究実績の概要 |
本研究は、非古典述語論理、特に超直観主義的述語論理(superintuitionistic predicate logics)に対する意味論としてjoinやmeetの「完備化」によらないexistsやforallの意味論を構築することを目指すものであった。この拡張は、圏論(category theory)における随伴(adjoint)の概念を援用してなされる。このためには、existsやforallの随伴となるものをいかに合理的に構築することができるかがカギとなった。関数記号の導入には、技術的な困難があったため、変数(自由変数と束縛変数を区別した体系の自由変数として導入)たちの作る有限列と、これを自然数の全体が作る自然な圏を活用して、上記の構造をHeyting代数の圏への関手として構成した。関数記号を持たない命題関数としての「論理式(formula)」、変数の有限列としての「context」の対が作るformula-in-contextを考えた時、これらを結ぶ関手として自然に導入されるものになる。この構造(formula-in-contextとHeyting代数の圏と上記の関手)がexistsやforallの随伴を自然にadjointとする意味論を導く。 最終年度には、これまでの成果を援用して、超直観主義的述語論理におけるexistence propertyやそれに関連したいくつかのpropertiesに関して、相互関係を調べることができた。これを国内学会で4件、国際学会(Logic Colloquium 2016, Leeds, UK)で1件の発表を行った。また、学術論文が2つ受理され、印刷中である。 補助事業期間全体での研究成果の発表は、学術論文4件(うち2つが査読後の印刷まち)、図書(分担執筆)1件、国内学会発表17件、国際学会発表14件、うち招待講演4件となった。
|