Uniform computability verified in a mathematically strong system and semi-intuitionistic provability for existence sentences

2017 Fiscal Year Final Research Report

• 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: Fujiwara Makoto 早稲田大学, 高等研究所, 助教 (20779095)
• Research Collaborator: KOHLENBACH Ulrich Technische Universität Darmstadt, Department of Mathematics, Professor
• Project Period (FY): 2016-08-26 – 2018-03-31
• 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.

Free Research Field

数学基礎論