Constructive reverse mathematics and computational content of mathematical theorems

构造性逆向数学和数学定理的计算内容

• 批准号: 21KK0045
• 负责人: 石原 哉
• 金额: $ 12.15万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Fund for the Promotion of Joint International Research (Fostering Joint International Research (B))
• 财政年份: 2021
• 资助国家: 日本
• 起止时间: 2021-10-07 至 2026-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21KK0045/
• 关键词: 構成的逆数学; 直観主義算術; 論理公理の階層; 超算術的公理; 構成的数学; 逆数学; プログラム抽出・合成

「様々な公理の解析」の主な成果は、唯一解をもつ弱ケーニヒの補題を構成的逆数学の観点から解析し、同主張が2つの論理公理と2つの関数存在公理に分離できることを示した。また、有限分木のheight-wise bounding function の存在の選択公理と帰納法による特徴づけを行った。さらに、構成的逆数学のための枠組み研究として、直観主義算術上の論理公理の階層構造の関係を詳しく解析し、その構造を明らかにした。「算術における逆数学」では、リーズ大学の研究者との共同研究により算術において強い公理を要請する解析学の命題の探索を進めている。最近の共同研究で超算術的公理系に対応する初等的命題も見つかった。また、「Cantor区間上の実連続関数が連続なモジュラスを持つ」という主張(命題)を構成的逆数学の観点から考察した。「集合論における逆数学」では、局所的コンパクト空間の位相のpoint-free位相表現を与えた。また、実数の集合（有理数の集合の完備化）は、有理数の基本列の集合とその上の同値関係で与えられる。古典的集合論では、基本列の集合を同値関係で割った商集合として実数の集合を定義する。商集合として定義すると、個々の基本列（代表元）の情報が失われ、それを取り出すためにはフルの選択公理が必要であり構成性が壊れてしまう。この状況を回避するために構成的集合論では実数全体を集合としてではなくセトイド（集合とその上の同値関係の対）として定義する必要があることが判明した。

The main result of "axiom analysis" is that the only solution is weak and the complement problem is composed of inverse mathematics. The point of analysis is the same as that of proposition. The logical axiom of 2 is the existence axiom of 2. The separation is shown. The axiom of the existence of a finite height-wise bounding function and the characteristic of the finite height-wise bounding function are discussed. A study of the inverse mathematics of composition and the hierarchical structure of logical axioms in straight-line arithmetic "Arithmetic and Inverse Mathematics" is a joint research of university researchers. Arithmetic and axioms are important. Analytic propositions are explored. Recent joint research on the axioms of hyperarithmetic is related to elementary propositions. The inverse mathematical point of proposition (proposition) is investigated. "Set theory" is the inverse of mathematics.また、実数の集合（有理数の集合の完备化）は、有理数の基本列の集合とその上の同値关系で与えられる。In classical set theory, the set of elementary columns is equal to the set of divisors. Quotient set definition, basic column (representative element) information is missing, and the selection axiom is necessary. This condition is avoided by the set theory of the whole set of numbers.

项目成果

構成的数学の景色

建构性数学景观

• 发表时间: 2023
• 作者: Fernandez-Duque D.;Shafer P.;Towsner H.;Yokoyama K.;Makoto Fujiwara;Makoto Fujiwara and Taishi Kurahashi;Makoto Fujiwara and Taishi Kurahashi;石原哉
• 通讯作者: 石原哉

半直観主義算術の階層と保存拡大定理，

半直观算术的层次结构和守恒展开定理，

• 发表时间: 2023
• 作者: Sakai Hiroyuki;Sato Hiroyuki;Iiduka Hideaki;藤原誠
• 通讯作者: 藤原誠

Metric fixed point theory and partial impredicativity

• DOI: 10.1098/rsta.2022.0012
• 发表时间: 2023-05-29
• 期刊: PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES
• 影响因子: 5
• 作者: Fernandez-Duque, D.;Shafer, P.;Yokoyama, K.
• 通讯作者: Yokoyama, K.

On the decomposition of WKL!!

• DOI: 10.1098/rsta.2022.0010
• 发表时间: 2023-05-29
• 期刊: PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES
• 影响因子: 5
• 作者: Fujiwara, Makoto;Nemoto, Takako
• 通讯作者: Nemoto, Takako

自然数論のモデルと逆数学

自然数论和逆数学模型

• 发表时间: 2023
• 作者: Fernandez-Duque D.;Shafer P.;Towsner H.;Yokoyama K.;Makoto Fujiwara;Makoto Fujiwara and Taishi Kurahashi;Makoto Fujiwara and Taishi Kurahashi;石原哉;藤原誠;横山啓太
• 通讯作者: 横山啓太