| 研究概要 |
昨年度までの成果として得られた,直観主義シーケント計算のカット除去で,一般除去規則を含む直観主義自然演繹の証明正規化と同型であるようなものについて,既存のシーケント計算に対応する計算体系との比較を行なった.既存体系として,Urbanやvan Bakelらによって,シーケント計算古典論理のカット除去に対応する計算体系が提案されているが,本研究ではその直観主義部分体系を定義し,これと我々の体系を比較した.この結果,Urbanらのカット除去では我々の体系のカット除去を模倣できないことが解った.具体的には,Urbanらの体系のカット除去手続きでは,置換簡約相当のカット置換を一ステップごとに分割して行なうことができず,連続して可能な置換簡約を一度に行なわなければいけないようになっている.このため,自然演輝における置換簡約を模倣できず,すなわち,一般除去規則と置換簡約を含む直観主義自然演繹の拡張にはなっていない.Urbanらの体系におけるカット除去の置換簡約に関するこの制限は,古典論理にけるカット除去として,対称性を持ち,強正規化可能であるものを得るために導入された制限であり,このことから,我々の直観主義シーケント計算のカット除去手続きを自然に拡張する形で古典シーケント計算のカット除去を得るためには,既存の手法とは異なる形式化を行なわなければならないことが解った.
|
