2019 Fiscal Year Research-status Report
Research of formal provability by means of the investigation of incompleteness theorems
| Project/Area Number |
19K14586
|
|---|
| Research Institution | Kisarazu National College of Technology |
|---|
Principal Investigator |
倉橋 太志 木更津工業高等専門学校, 基礎学系, 講師 (10738446)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 数学基礎論 / 数理論理学 / 不完全性定理 / 証明可能性 / 形式的算術 / 様相論理 / 部分的な保存性 / クリプキ意味論 |
|---|
| Outline of Annual Research Achievements |
本研究は不完全性定理の分析を通じて，形式的体系の証明可能性のもつ構造の性質を明らかにすることを目標とする。
(1) 複数の理論に対して同時に Γ-保存的となる文の存在に関する Guaspari の問題について：Γ を n>0 に対する Σ_n もしくは Π_n とする。PA のΣ_1-定義可能な無矛盾拡大理論に対して，Γ-保存的な Γ^d 文が存在することが Guaspari によって示されており、これは Goedel の第一不完全性定理の強化版である。Bennet は特に２つの理論において同時に Σ_n-保存的となる文が存在するための必要十分条件を与えた。本研究では有限個の理論が同時に Σ_n-保存的となる文が存在するための必要十分条件を与えることで Bennet の結果を一般化し、さらに任意の有限個の理論に対して同時に Π_n-保存的となる文が存在することを証明した。これにより有限個の理論に対する Guaspari の問題が完全に解決した。本研究は千葉大学の大川裕矢氏とオランダの Shavrukov 氏との共同研究である。
(2) 証明可能性の様相論理 GL に"PA + B は PA + A 上で Γ-保存的" を表す論理式を加えることで様々な体系が得られる。特に ILM が Π_1-保存性の論理であることが知られている。IML は論理 IL の拡張であるが、Γ≠Π_1 に対しては IL の公理 J5 がもはや妥当ではないため、Γ-保存性の論理の分析の基盤となるのは IL から J5 を除いた CL という論理である。本研究では同様に IL から種々の公理を除いて得られる20個の論理に対するクリプキ完全性について分析を行った。特にそのうちの12個の論理がクリプキ完全であり、8個の論理が不完全であることを示した。本研究は千葉大学の大川裕矢氏との共同研究である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
40年未解決であった Guaspari の問題に進展があったためおおむね順調であるといえる。
また、部分保存的な文の分析に関する様相論理からのアプローチも議論の土台が出来上がってきたように思われる。
得られた研究成果については学術雑誌に投稿した。
|
| Strategy for Future Research Activity |
初年度に得られた結果をもとに引き続き研究を進める。特に Σ_1-保存性や Σ_2-保存性の論理に関する研究もスタートするとともに、論理 IL や CL に関する基本的な性質の分析についても合わせて行っていく。
関係する研究者との研究討論を行い、（状況的に可能であれば）学会や研究集会への参加を行う。
|
