一句话:提出实例可归约性,证明实例度构成 frame,并推广为结构更丰富的扩展 Weihrauch 度。
逆向构造数学中若干原理需要统一的可归约性来比较和分类。作者提出谓词间的实例可归约性,并研究其实例度。证明实例度构成一个 frame,等价于真值上集合按反向 Smyth 偏序构成的 frame;子对象分类子以单调和反单调两种方式嵌入,¬¬-稠密的度恰可归约到排中律度。在相对 realizability topos 中给出实例度的显式表述,称为扩展 Weihrauch 度;在 Kleene-Vesley realizability 中,¬¬-稠密 modest 实例度恰对应 Weihrauch 度。扩展度通过可计算的下确界与上确界、蕴含、参数访问和结果计算控制,改进了 Weihrauch 度的结构并拓宽其范围。
We identify a notion of reducibility between predicates, called instance reducibility, which commonly appears in reverse constructive mathematics. The notion can be generally used to compare and classify various principles studied in reverse constructive mathematics (formal Church's thesis, Brouwer's Continuity principle and Fan theorem, Excluded middle, Limited principle, Function choice, Markov's principle, etc.). We show that the instance degrees form a frame, i.e., a complete lattice in which finite infima distribute over set-indexed suprema. They turn out to be equivalent to the frame of upper sets of truth values, ordered by the reverse Smyth partial order. We study the overall structure of the lattice: the subobject classifier embeds into the lattice in two different ways, one monotone and the other antimonotone, and the $\lnot\lnot$-dense degrees coincide with those that are reducible to the degree of Excluded middle. We give an explicit formulation of instance degrees in a relative realizability topos, and call these extended Weihrauch degrees, because in Kleene-Vesley realizability the $\lnot\lnot$-dense modest instance degrees correspond precisely to Weihrauch degrees. The extended degrees improve the structure of Weihrauch degrees by equipping them with computable infima and suprema, an implication, the ability to control access to parameters and computation of results, and by generally widening the scope of Weihrauch reducibility.