Computability theory on intuitionistic logic and its application to constructive reverse mathematics

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

本年度は構成的逆数学の研究を行った。構成的逆数学において重要な弱ケーニッヒの補題WKLには様々な亜種があるが、無限パスが高々１つ存在する無限二分木に制限した場合WKL!!も構成的には自明に成立するものではない。これはパスを計算するアルゴリズムが必ずしも存在しないということで、計算機科学的にも重要な問題である。2022年度の研究では、(1) WKL!!の論理原理と選択公理による特徴づけおよび(2) WKLからケーニッヒの補題KLとを導く際に必要なheight-wise bounding function の存在の選択公理による特徴づけを行った。(1) については、WKLの特徴づけが論理原理\Sigma^0_1-DMLと選択公理\Pi^0_1-AC^{\lor}で与えられたことに対し、それらよりも真に弱い論理原理 \Pi^0_1-DMLおよび(\Pi^0_1\lor\Pi^0_1)-DNSと選択公理dn-\Pi^0_1-AC^{\lor}および\Pi^0_1\-AC^{\lor}で特徴づけられることが明らかになった。この成果は論文として出版済みである。(2)については、height-wise bounding function の存在が「任意のxに対してA(x,y)なる最大のyが存在するとき、各xに対してそのA(x,y)なる最大のyを返す関数が存在する」という極めて自然な形の選択公理の一種で特徴づけられた。またheight-wise bounding function の存在は、帰納法原理と関係があることも明らかになりつつある。この成果について、投稿論文を準備中である。