2017 Fiscal Year Research-status Report
| Project/Area Number |
16K17653
|
|---|
| Research Institution | Kisarazu National College of Technology |
|---|
Principal Investigator |
倉橋 太志 木更津工業高等専門学校, 基礎学系, 講師 (10738446)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 数理論理学 / 数学基礎論 / 証明可能性述語 / 不完全性定理 / 形式的算術 / 証明可能性 / 超準モデル / 様相論理 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，形式的理論の証明および証明可能性に関する性質を構文論的・意味論的側面から分析し，理解を深めることである．
(1) T の証明可能性述語 Pr_T(x) について U において証明できる原理に関する命題証明可能性論理 PL_T(U) が GL_α, GL_β^-, D_β, S_β（ただしβは補有限）で尽くされることが Beklemishev(1989) らによって示されている（分類定理）．本研究では U を固定して T を動かした際に PL_T(U) がどのような論理になりうるのかを分析した．結果，L を上記の論理の１つとし（ただしαは r.e. でβは補有限），U を PA の r.e. 無矛盾拡大とすると，IΣ_1 の無矛盾な r.e. 拡大理論 T とその Σ_1 定義 τ(u) が存在して，PL_τ(U) が L と一致することを証明した．
(2) 対応する証明可能性論理が正規様相論理となる Rosser 証明可能性述語について分析し，次の２つの結果が得られた．1. 証明可能性論理がちょうど KD と一致するような Rosser 証明可能性述語が存在する．2. 証明可能性論理が KD を真に含むような Rosser 証明可能性述語が存在する．
(3) Sacchetti(2001) は GL より弱い様相論理 K+□(□^n p→p)→□p を導入し，その不動点定理を証明した．Sacchetti による不動点定理の証明は各論理式に対する具体的な不動点の構成を与えるものではなかったため，不動点定理の構成的な証明という問題が提起されていた．本研究では Sacchetti の論理に対する具体的な不動点の構成を与えるような不動点定理の証明を与えることで Sacchetti の問題に対する肯定的な解答を与えた．本研究は大川裕也氏（千葉大学院生）との共同研究である．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
昨年度に引き続きいくつかの結果が得られ，研究成果がまとまった内容については論文を作成し，学術雑誌に投稿することができた．特に研究 (2) について，「算術的完全となる証明可能性述語が存在するような正規様相論理」に関する研究において Rosser 証明可能性述語が有用であることが示されたため，今後この方針で分析をすすめることで更なる結果が得られることが期待される．
|
| Strategy for Future Research Activity |
初年度および二年度に得られた結果をもとに引き続き研究を進める．証明可能性述語について，対応する証明可能性述語が正規かどうかは導出可能性条件D1,D2を満たすかどうか，ということである．今後は特にこの導出可能性条件と，様相論理，および理論の証明可能性の間の関係をさらに分析するという方針で研究を進める予定である．関係する研究者と研究討論を行い，学会や研究集会においても発表を行う予定である．
|
| Causes of Carryover |
書籍の購入の予定を変更したため．未使用額分は書籍の購入に充てる．
|
