2003 Fiscal Year Final Research Report Summary
Comparative studies on nonstandard methods and constructive methods
| Project/Area Number |
13640098
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
TANAKA Kasuyuki Tohoku University, Graduate School of Science, Professor, 大学院・理学研究科, 教授 (70188291)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AKAMA Yohji Tohoku University, Graduate School of Science, Associate Professor, 大学院・理学研究科, 助教授 (30272454)
TAKEDA Masayoshi Tohoku University, Graduate School of Science, Professor, 大学院・理学研究科, 教授 (30179650)
MORITA Yasuo Tohoku University, Graduate School of Science, Professor, 大学院・理学研究科, 教授 (20011653)
YAMAZAK Takeshi Osaka Prefecture University, Dept.of Math.and Info.Sciences, Research Assistant, 総合科学部, 助手 (30336812)
|
|---|
| Project Period (FY) |
2001 – 2003
|
| Keywords | second order arithmetic / WKL_0 / nonstandard method |
|---|
| Research Abstract |
Second order arithmetic was first introduced by D.Hilbert around 1920's to set a firm foundation of analysis. Among many different formalizations of second order arithmetic, RCA_0 and WKL_0 are particularly important with respect to Hilbert's program. Tanaka and Yamazaki, in cooperation with Simpson, proved that one can eliminate, the compactness argument from proofs for a certain sort of theorems in WKL_0, namely WKL_0 is conservative over RCA_0 for the formulas in a certain form. They also showed that the bounded dependent choice scheme, which is often used in the computation of real numbers, can not be eliminated likewise. Thus, Tanaka and Yamazaki constructed an appropriate truth definition for the real number system via the quantifier elimination method, by which one can manipulate the reals freely in RCA_0. By sophisticating this argument, Tanaka, jointly with Sakamoto, could prove Hilbert's Nullstellensatz within RCA_0. Yamazaki and Sakamoto also studied uniform versions of WKL_0 and other statements within higher order arithmetic. Yamazaki investigated the logical strength of completeness theorems for intuitionistic logic.
|
