2004 Fiscal Year Annual Research Report
近似プログララムの計算論-古典論理の証明のテストにむけて-
| Project/Area Number |
15700001
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
|
|---|
| Keywords | monotone modified 実現可能性解釈 / 構成的論理 / lesser limited principle of omniscience / プログラム抽出 / Lifsitz' 実現可能性解釈 / Markov principle / 冠頭標準形定理 / 無限カット除去定理 |
|---|
| Research Abstract |
数学対象の構成的存在証明からは有意な情報を得られることが多いが、どのような構成的推論原理からどのような手法によりそれら有意な情報が抽出できるかが問題となるであろう。
我々は構成的推論原理としてMarkov Principle、弱 Koenig補題,単純全称(存在)量化式に対する排中律、Postの定理、に着目したが、それらの推論原理に現れる論理式を一般の冠頭標準形に拡張することにより、構成的推論原理の階層を考えた:
Σi冠頭標準形に対する二重否定除去原理(Σi-LEM)、
Σi冠頭標準形に対するLesser Limited Principle of Omniscience(Σi-LLPO)、
Σi冠頭標準形に対する排中律(Σi-LEM)
Pi^O_i冠頭標準形に対する排中律(Σi-LEM)
Δi式に対する排中律(Δi-LEM)。
そして、冠頭標準形定理(全ての論理式は同値な冠頭標準形を持つ)との関係をまず考察した。
次に全ての正整数iに対して以下を証明した:Heyting Arithmeticにおいて、
(1)Σi-LEM,Πi-LEM,Σi-LLPO,Δi-LEM Σ(i-i)-LEMの順に真に強い.またΣi-LEM,Σi-DNE,Δi-LEMの順に真に強い。
(2)Πi-LEMとΣi-DNEからΣi-LEMが証明できる。
逆向きがいえないことの示すために、形式証明からプログラムを抽出するための手法を用いた。具体的には、実現可能性解釈、無限カット除去定理、Kohlenbachのmonotone modified実現可能解釈,van OostenのLifschitz'実現可能解釈である。
|
