Constructive reverse mathematics and computational content of mathematical theorems

点击翻译按钮获取中文摘要

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