2016 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) 証明の論理 LP の算術的完全性定理の改良：Artemov (2001) による LP の算術的完全性定理の証明は通常の証明述語を固定するだけでは成立しないため，全ての Δ1 証明述語を考慮に入れることで行われていた．本研究では，うまく定義した Δ1 証明述語を固定するだけでも議論が通ることを示し，LP の算術的完全性定理を改良した．また一様算術的完全性定理の成立するような Σ1 証明述語の存在を証明した．本研究は岩田荘平氏（名古屋大，現神戸大）との共同研究である．
(2) 不完全性定理の一般化：Godel の第一不完全性定理は「PA を含む無矛盾かつ再帰的な理論からは真であるが証明できない Π1 命題がある」という形で述べることができる．この結果は Jeroslow (1975) によって拡張，Hajek (1977) によって一般化された．本研究では「PA を含む無矛盾な理論について，その定理全体の集合が Π_{n+1}-定義可能ならば，真であるが証明できない Π_n 命題がある」という定理を証明し，Jeroslow と Hajek の結果を拡張した．また Hajek による問題を否定的に解決した．本研究は菊池誠教授（神戸大）との共同研究である．
(3) Sacchetti の論理の算術的完全性：Sacchetti (2001) は証明可能性の論理 GL より弱い無限個の様相論理の族を定義した．本研究ではこれらの論理に対して，適切に Σ2 証明可能性述語を定めることで算術的健全性・算術的完全性が成立することを証明し，Sacchetti の問題を肯定的に解決した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
構文論的側面の研究は予定していたよりも順調に進み，特に研究 (3) において証明可能性の論理の研究の新たな方向性を見出すことができたことは大きな進展である．本年度に得られた結果によって，証明および証明可能性の研究の分析を更に進めることができると期待される．一方，意味論的側面の研究は十分な成果を得ることができなかった．
研究成果がまとまった内容については論文を学術誌に投稿した．
|
| Strategy for Future Research Activity |
初年度に得られた結果をもとに引き続き研究を進める．特に Σ2 証明可能性述語に基づく証明可能性論理については，これまでに対応のついた論理以外にも対応のつく論理があるのかを分析する．また，算術の超準モデルにおける証明構造の分析については Gothenburg 大の Blanck とともに研究を進める．関係する研究者との研究討論を行い，学会や研究集会への参加を行う．
|
| Causes of Carryover |
１月に出席を予定していた研究集会に参加することができなくなったため．
|
| Expenditure Plan for Carryover Budget |
国内では日本数学会，国外では Logic Colloquium 2017 などの研究集会・学会に出席し研究成果発表を行う予定であり，その旅費に科学研究費補助金を利用したいと考えている．また研究に関連する書籍も科学研究費補助金で購入することを予定している．
|
