2000 Fiscal Year Annual Research Report
| Project/Area Number |
12740077
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
安東 祐希 法政大学, 第一教養部, 助教授 (40277687)
|
|---|
| Keywords | 自然演繹 / 古典論理 / 正規化定理 |
|---|
| Research Abstract |
自然演繹体系における最大論理式を除去する縮約手続きに関しては、従来プラヴィッツが直観主義論理体系および原始的論理記号を制限した古典主義論理体系に対し、弱正規化定理および強正規化定理を証明していた。その後、すべての論理記号を原始的に含む古典論理の自然演繹体系に対して縮約手続きを定義する試みが複数の研究者によって為されてきたが、そのうちの一つが筆者の1995年によるものであり、それはプラヴィッツの直観主義論理における手続きを自然に拡張したものであった。
しかしこれまではその正規化定理に関しては弱い形のもののみ証明されていたため、強い形の正規化定理を証明することが今年度の本研究の目標の一つであった。そしてその強正規化定理の証明が得られ、別記の通りその概要を発表した。
強正規化定理とは、「与えられた任意の証明図に対し、それから始まる任意の縮約列の長さが有限である」という主張である。われわれの体系、すなわちすべての論理記号を原始的に含む古典論理自然演繹体系において、最大論理式を縮約する場合、選言および存在演算子に対する論理記号の除去、および古典論理の二重否定の除去の推論に導かれる最大論理式は、構造的縮約点からなる木構造を見出すことにより、プラヴィッツの縮約の定義を拡張することができた。それに対する強正規化定理は、ド・グルートが直観主義論理において用いた拡張されたPCF翻訳の方法を適用することにより得られた。そのためには、型付きラムダ計算の体系の手法を用いることが必要であった。
|
Research Products
(1 results)
