Uniform computability and constructive derivability between existence sentences
| Project/Area Number |
18K13450
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Meiji University (2019-2020)
Waseda University (2018) |
|---|
Principal Investigator |
Fujiwara Makoto 明治大学, 研究・知財戦略機構(生田), 研究推進員(客員研究員) (20779095)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2018: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 計算可能数学 / 構成的逆数学 / 逆数学 / 直観主義算術 / 存在定理 / 相対的一様計算可能性 / 構成的数学 / 一様計算可能性 / 直観主義論理 |
|---|
| Outline of Final Research Achievements |
Most of mathematical theorems have a form that "for any X satisfying some condition, there exists some solution Y for X". Such theorems are called "existence theorems". In computable mathematics, their interrelation has been studied via Weihrauch reducibility.
In this project, we formalized the primitive recursive version of Weihrauch reducibility in finite-type arithmetic and showed that for any existence sentences P and Q of some syntactical form, P is primitive recursively Weihrauch reducibile to Q verifiably in a classical finite-type arithmetic T if and only if P is derivable from Q in the semi-intuitionistic counterpart iT of T with a proof of the standard structure. Then we established that this meta-theorem is applicable to many existence theorems by providing several concrete examples. In addition, we showed that the syntactical restriction in our meta-theorem cannot be avoided by providing a counterexample.
|
| Academic Significance and Societal Importance of the Research Achievements |
数学の定理の多くは「条件を満たす全てのXに対して，条件を満たす解Yが存在する」という形をしており，そのような何かしらの解の存在を主張する定理は「存在定理」と呼ばれる．存在定理同士の強さの関係を調べる研究が，計算可能数学や構成的逆数学のそれぞれの文脈において行われてきた．
本研究では，計算可能数学における存在定理の間の還元可能性を，直観主義論理に基づいた有限型算術における導出可能性を用いて部分的に特徴付けた．これにより．これまでそれぞれ独立に研究が進められてきた計算可能数学と構成的逆数学の直接的な関連性が一部明らかになった．
|
Report
(4 results)
Research Products
(6 results)
