古典述語論理に対応する項計算体系の研究

自然演繹計算はゲンツェンにより導入された形式的論理体系の一つであり、通常の数学において用いられる推論と密接な関係を持つ。その論理体系の基本的性質の一つとして、最大論理式の縮約方法に関する諸定理がある。その中の合流性定理、すなわち始点を共有する縮約列に関してそれを合流する縮約列を構成することができるという定理については、直観主義論理の特に可換性縮約を含まない体系について良く知られていたが、それ以外の体系については直接的な証明が必ずしも得られていなかった。それは、可換性縮約が縮約点の増長をもたらし、単純な合流性証明の適用ができないためである。本研究においては、この困難を克服する方法の改良を行った。そこでは、直観主義論理の可換性縮約のみならず、古典主義論理の二重否定除去に起因する縮約に関しても、構造的縮約として統一的に扱われている。表現の簡略化のためには、項計算体系を、伸縮性を持つ縮約点の連続的な縮約を表現できるように拡張する手法が用いられている。その際、特に古典論理に特有な、縮約点による木構造が項の生成規則に関して飛躍を持ち、それが互いに分離されない場合に関して、拡張された項表現を用いた代入形式を整備した。特に、構造的な縮約の連続において生成される木構造を、元の証明図あるいは項の部分構造に制限した場合、本来の木構造とはなり得ぬ集合を、潜在的な木構造として扱うことが必要となるが、それに対してさらに拡張された代入形式を定義し、その代入形式間の可換性に関する研究を進めた。

自然演繹計算はゲンツェンにより導入された形式的論理体系の一つであり、通常の数学において用いられる推論と密接な関係を持つ。その論理体系の基本的性質の一つとして、最大論理式の縮約方法に関する諸定理がある。その中の合流性定理、すなわち始点を共有する縮約列に関してそれを合流する縮約列を構成することができるという定理については、直観主義論理の特に可換性縮約を含まない体系について良く知られていたが、それ以外の体系については直接的な証明が必ずしも得られていなかった。それは、可換性縮約が縮約点の増長をもたらし、単純な合流性証明の適用ができないためである。本研究においては、この困難を克服する方法の改良を行った。そこでは、直観主義論理の可換性縮約のみならず、古典主義論理の二重否定除去に起因する縮約に関しても、構造的縮約として統一的に扱われている。表現の簡略化のためには、項計算体系を、伸縮性を持つ縮約点の連続的な縮約を表現できるように拡張する手法が用いられている。その際、特に古典論理に特有な、縮約点による木構造が項の生成規則に関して飛躍を持ち、それが互いに分離されない場合に関して、拡張された項表現を用いた代入形式を整備した。特に、構造的な縮約の連続において生成される木構造を、元の証明図あるいは項の部分構造に制限した場合、本来の木構造とはなり得ぬ集合を、潜在的な木構造として扱うことが必要となるが、それに対してさらに拡張された代入形式を定義し、その代入形式間の可換性に関する研究を進めた。