2022 Fiscal Year Research-status Report
Computability theory on intuitionistic logic and its application to constructive reverse mathematics
| Project/Area Number |
18K03392
|
|---|
| Research Institution | Hiroshima Institute of Technology |
|---|
Principal Investigator |
根元 多佳子 広島工業大学, 環境学部, 准教授 (20546155)
|
|---|
| Project Period (FY) |
2018-04-01 – 2024-03-31
|
| Keywords | 構成的数学 / 計算可能性理論 / 構成的逆数学 |
|---|
| Outline of Annual Research Achievements |
本年度は構成的逆数学の研究を行った。
構成的逆数学において重要な弱ケーニッヒの補題WKLには様々な亜種があるが、無限パスが高々１つ存在する無限二分木に制限した場合WKL!!も構成的には自明に成立するものではない。これはパスを計算するアルゴリズムが必ずしも存在しないということで、計算機科学的にも重要な問題である。
2022年度の研究では、
(1) WKL!!の論理原理と選択公理による特徴づけおよび
(2) WKLからケーニッヒの補題KLとを導く際に必要なheight-wise bounding function の存在の選択公理による特徴づけを行った。
(1) については、WKLの特徴づけが論理原理\Sigma^0_1-DMLと選択公理\Pi^0_1-AC^{\lor}で与えられたことに対し、それらよりも真に弱い論理原理 \Pi^0_1-DMLおよび(\Pi^0_1\lor\Pi^0_1)-DNSと選択公理dn-\Pi^0_1-AC^{\lor}および\Pi^0_1\-AC^{\lor}で特徴づけられることが明らかになった。この成果は論文として出版済みである。(2)については、height-wise bounding function の存在が「任意のxに対してA(x,y)なる最大のyが存在するとき、各xに対してそのA(x,y)なる最大のyを返す関数が存在する」という極めて自然な形の選択公理の一種で特徴づけられた。またheight-wise bounding function の存在は、帰納法原理と関係があることも明らかになりつつある。この成果について、投稿論文を準備中である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2022年度の研究では有限分木とケーニッヒの補題についての研究が順調に進展し、WKL!!の特徴づけが当初の予想よりも自然な選択公理と論理原理の組で得られた。また、WKLからKLを導くためのheight-wise bounding function の存在については、選択公理との特徴づけの他に帰納法原理との関係性も明らかになりつつある。全般的に論文執筆も進んだこと、さらに今後の課題も明らかになったことから、おおむね順調といえる。
|
| Strategy for Future Research Activity |
古典的逆数学では、ケーニッヒの補題の特徴づけは集合内包公理ACAで与えられるが、2022の研究では構成的逆数学では論理原理LLPO＋複数の種類の選択公理という形で与えられた。
今後の研究では、ACAとの関係も明らかにすることで、古典的逆数学の結果を拡張する。
また、直観主義論理下での次数の構造についての研究、特に直観主義論理下での優先法について研究を進める。
|
| Causes of Carryover |
計画当初は国際共同研究や国際学会における成果発表を予定していたため外国旅費の拠出を見込んでいたが、新型コロナウイルス感染症の拡大に伴い海外渡航が難しくなったため、旅費の未使用分が次年度使用額となった。
|
