| 研究課題/領域番号 |
24540125
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
菊池 誠 神戸大学, システム情報学研究科, 准教授 (60273801)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | 数学基礎論 / 不完全性定理 / 算術の超準モデル / 様相論理 / 矛盾許容型論理 |
|---|
| 研究概要 |
算術の超準モデルに関しては，算術の理論 T の超準モデル M 上で Rosser の可証性述語が定める理論が TA と一致するような M が存在するかという問題について，議論の鍵となることが予想される Guaspari & Solovay の証明述語の構成方法の詳細な検討を行なった．また，算術の超準モデルと不完全性定理に共通する問題として，通常の可証性述語が超準的な証明を許容する問題に対応するために提示された Artemov による証明論理について，超準的な証明が必然的に現れる例が存在するか，自己言及的で算術的な証明は存在するか，型理論としての証明論理の可能性，という新たな問題について検討を開始した．不完全性定理に関しては，無矛盾性命題の超限長の無限下降列は既知の方法によって構成可能であることが判明した．また，Goedel のオリジナルの証明を一般化することで，それ自身は矛盾し，論理式の中に現れる幾つかの命題変数に必然性を表す様相演算子を追加した場合には無矛盾となる命題論理式の存在から不完全性定理が導かれることを証明し，この方法を一般化することで Yablo の逆理から不完全性定理が導出可能であることを示して，通常の命題論理式を用いる場合には Yablo の逆理と同様の現象は現れないことを明らかにした．矛盾許容型論理に関しては，一般設計学で位相空間論が用いられることの理由を検討し，位相の概念は人工物を生産，使用する際の機能の安定性を形式的に議論するために重要であるという見方を提示した．また，存在可能であるが存在していない人工物と存在不可能な人工物の区別への矛盾許容型論理の適用可能性について検討を行なった．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
算術の超準モデルに関しては，Rosser の述語に関する問題については技術的検討が順調に進んでいるが，超準モデルの構造についての問題は遅れている．しかし，今後，大きな発展が期待される証明論理に関する新たな問題を見出だしたことは期待以上の進展である．不完全性定理に関しては，超限長の無矛盾性命題列に関する問題は既知の方法で解決可能であることが判明し，speed-up 定理に関しては遅れている．ただし，命題様相論理と関連した新たな問題について結果を得ており，全体としては順調である．矛盾許容型論理に関しては，期待された結果には到達していないが進展はしており，次年度以降での達成が期待される．以上から，現在までの達成度は概ね順調であると判断される．
|
| 今後の研究の推進方策 |
平成24年度の研究内容に引き続き研究を継続する．特に，以下の問題に集中して取り組む予定である．算術の超準モデルに関して，not Con(T) を満たす超準モデルの構造に関する問題と，証明論理に関する新たな幾つかの問題．不完全性定理に関して，Speed-up 定理に関する問題と，Kaplan-Montague による知識に関する議論や，様々な逆理と不完全性定理の証明の関係の分析．矛盾許容型論理に関して，一般設計学への新たな応用可能性の検討．そのため，国内外の研究者と適宜研究打ち合わせや小規模のセミナーを実施の予定である．
|
| 次年度の研究費の使用計画 |
平成24年度中に実施の予定であった国内研究者との研究打ち合わせの一つに日程の調整が出来ず平成24年度中に実施できなかったものがあった．平成25年度の経費と合わせて早期に，計画されていた研究打ち合わせを実施の予定である．
|
