2014 Fiscal Year Annual Research Report
| Project/Area Number |
26887045
|
|---|
| Research Institution | Kisarazu National College of Technology |
|---|
Principal Investigator |
倉橋 太志 木更津工業高等専門学校, その他部局等, 講師 (10738446)
|
|---|
| Project Period (FY) |
2014-08-29 – 2016-03-31
|
| Keywords | 数理論理学 / 数学基礎論 / 可証性述語 / 不完全性定理 / 形式的算術 / 証明可能性 / 超準モデル |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，不完全性定理の証明において特に重要な意味を持つ，形式的体系の証明可能性を表現する論理式である可証性述語の性質について調べ，それを通じて形式的証明や形式的証明可能性に関する理解を深めることである．
１．構文論的研究：ゲーデル・ロッサーによる第一・第二不完全性定理を，算術的に定義可能な理論に対して拡張する研究を行った．可証性述語を用いた不完全性定理の証明は，理論の計算可能性を仮定しない場合でも，理論の健全性の仮定を強めることで実行可能であることを示した．また，算術的定義可能な理論における無矛盾性言明の証明可能性に関する成果も得た．本成果は従来の古典的な不完全性定理の議論の枠を超えようとするものであり，理論の証明可能性の分析に新たな視点を与えると考えられる．
２．意味論的研究：算術の超準モデルにおける証明構造の研究を，超準モデルにおける可証性述語の振る舞いについて調べることによって行った．定理集合が包含関係をもたないような２つのモデル（比較不能なモデル）は特にお互いに相反する定理を証明すること，PA+Con(PA+Con(PA))のモデルがその終拡大に比較不能なモデルをもつこと，その定理集合が自然数の超準モデルにおける定理集合より真に大きい超準モデルは実際には証明できないような正しい命題を証明できることなどを示した．本研究により，PA+Con(PA)の超準モデルにおける証明可能性や証明の構造に関する理解が深まり，それに伴って矛盾に至る証明をもつ超準モデルにおける証明構造の全体像の解明も進んだと考えられる．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
可証性述語を中心とした，構文論的，意味論的研究についてそれぞれ新たな結果が得られた．構文論的研究については，不完全性定理に関する研究に新たな方向性を見出したことが大きな進展である．これによって形式的証明可能性の分析を更に進めることができると期待される．意味論的研究については未解決な問題が残されているものの，研究成果がまとまったため，論文を学術誌に投稿した．
|
| Strategy for Future Research Activity |
初年度に得られた成果をもとに，引き続いて研究を行う．特に，算術的に定義可能な理論における可証性述語の振る舞いを調べることによって，形式的証明可能性の分析をさらに進める．また，超準モデルにおける証明について，そのステップ数などに関する既存の結果との対応関係を調べながら，超準モデルにおいて矛盾に至る証明の全体構造の解明を進める．そのためにも，関係する研究者との打ち合わせや研究集会・学会等への参加を行う．
|
