| Project/Area Number |
16H07289
|
|---|
| Research Category |
Grant-in-Aid for Research Activity Start-up
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Foundations of mathematics/Applied mathematics
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
|
|---|
| Research Collaborator |
KOHLENBACH Ulrich Technische Universität Darmstadt, Department of Mathematics, Professor
|
|---|
| Project Period (FY) |
2016-08-26 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
Fiscal Year 2017: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 構成的数学 / 計算可能数学 / 逆数学 / 存在定理 / 直観主義算術 / 論理原理 / 数学基礎論 |
|---|
| Outline of Final Research Achievements |
We show that for any existence sentences of some syntactical form, the solution is uniformly computable in the sense of primitive recursive functionals in all finite types and its verification can be carried out in the classical arithmetic containing arithmetical comprehension axiom in all finite types if and only if the existence sentence is provable in semi-intuitionistic finite-type arithmetic containing the numerical double negation shift scheme restricted to Sigma02 formulas with function parameters and the axiom schema of countable choice for numbers.
In addition, we analyze the interrelation between the semi-intuitionistic system mentioned above and other semi-intuitionistic systems considered in constructive reverse mathematics.
|
