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位相表現を与えた。また、実数の集合（有理数の集合の完備化）は、有理数の基本列の集合とその上の同値関係で与えられる。古典的集合論では、基本列の集合を同値関係で割った商集合として実数の集合を定義する。商集合として定義すると、個々の基本列（代表元）の情報が失われ、それを取り出すためにはフルの選択公理が必要であり構成性が壊れてしまう。この状況を回避するために構成的集合論では実数全体を集合としてではなくセトイド（集合とその上の同値関係の対）として定義する必要があることが判明した。

从组成型逆数学的角度来看，“各种公理分析”的主要成就分析了具有单个解决方案的弱koenig的引理，这表明该参数可以分为两个逻辑公理和两个功能公理。此外，我们表征了使用公理和诱导的有限树的高度边界函数的存在。此外，作为本构逆逆数学的框架研究，我们分析了直观算术逻辑公理的层次结构的关系，以阐明结构。在“算术中的相互数学”中，我们正在利兹大学的一名联合研究人员探索算术中需要强公理的分析命题。最近的联合研究还发现，与超氧化公理相对应的主要命题。我们还研究了主张“从组成型逆数学的角度来看”的断言（命题）“ cantor间隔上的实际连续函数具有连续模量”。在“集合理论中的相互数学”中，我们给出了局部紧凑型空间拓扑的无点拓扑表示。此外，真实数字集（合理数字集的完成）由理性数字的基本序列和上述等价关系给出。经典集理论将一组实数定义为通过将基本序列除以等效关系而获得的商集。将其定义为商业集将丢失每个基本序列（代表源）的信息，为了检索它，需要进行完整的选择公理，从而导致构成性被打破。为了避免这种情况，构成集理论表明，有必要将整个实际数字定义为一组（上面的一对及其等价关系），而不是集合。

项目成果

構成的数学の景色

建构性数学景观

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

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

Delta^0_1 variants of the law of excluded middle and related principles

排中律的Delta^0_1变体及相关原理

• DOI: 10.1007/s00153-022-00827-5
• 发表时间: 2022
• 期刊: Archive for Mathematical Logic
• 影响因子: 0.3
• 作者: M.Kano;S. Maezawa;K. Ota;M. Tsugaki and T. Yamashita;Makoto Fujiwara
• 通讯作者: Makoto Fujiwara

証明作法

证明礼仪

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