| 研究概要 |
本研究では,直観主義シーケント計算のカット除去と直観主義自然演繹の証明正規化の間の関係を明らかにした.シーケント計算のカット除去の性質を,既にその計算論的性質が深く研究されている自然演繹の証明簡約を通して見ることにより,カット除去の計算論的性質を明らかにできる.古典論理はその形式化としてシーケント計算が適しているので,本研究の結果得られたカット除去に対する知見を古典論理への拡張に利用することにより,古典論理の計算論的意味を明らかにする手掛りが得られると期待できる.
今年度の成果としては,より具体的には以下の結果を得た.
直観主義シーケント計算の一つとして局所カット除去手続きをもつものを提案し,そのカット除去手続きが,ある種の自然演繹における証明正規化と同型であるものを示した.この自然演繹は,一般除去規則と呼ばれる除去規則と明示的代入を含むものである.また,シーケント計算の部分体系として,カットを特定の形のみに限定したものを提案し,この部分体系が一般除去規則を含む(明示的代入を含まない)自然演繹に同型対応すること,及びそのカット除去手続きの合流性と強正規化性を証明した.強正規化性については,CPS変換の変形であるCGPS変換の手法を用いた.さらに,もとのシーケント計算のカット除去手続きの合流性と強正規化性を部分体系の性質に帰着する方法で証明した.この手法は,明示的代入に対して提案されていた方法を適用したものである.
|
