Weihrauch and constructive reducibility between existence statements

被引:1
|
作者
Fujiwara, Makoto [1 ]
机构
[1] Meiji Univ, Sch Sci & Technol, Kawasaki, Kanagawa, Japan
来源
关键词
Foundations of mathematics; Weihrauch reducibility; reverse mathematics; constructive mathematics; finite-type arithmetic; existence statements; REVERSE MATHEMATICS; PRINCIPLES; CHOICE;
D O I
10.3233/COM-190278
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finitetype arithmetic is identical to some formal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas. In addition, we demonstrate that our meta-theorem is applicable in some concrete examples from classical and constructive reverse mathematics.
引用
收藏
页码:17 / 30
页数:14
相关论文
共 50 条