Instance reducibility and Weihrauch degrees

We identify a notion of reducibility between predicates, called instancereducibility, which commonly appears in reverse constructive mathematics. Thenotion can be generally used to compare and classify various principles studiedin reverse constructive mathematics (formal Church's thesis, Brouwer'sContinuity principle and Fan theorem, Excluded middle, Limited principle,Function choice, Markov's principle, etc.). We show that the instance degreesform a frame, i.e., a complete lattice in which finite infima distribute overset-indexed suprema. They turn out to be equivalent to the frame of upper setsof truth values, ordered by the reverse Smyth partial order. We study theoverall structure of the lattice: the subobject classifier embeds into thelattice in two different ways, one monotone and the other antimonotone, and the$\lnot\lnot$-dense degrees coincide with those that are reducible to the degreeof Excluded middle. We give an explicit formulation of instance degrees in a relativerealizability topos, and call these extended Weihrauch degrees, because inKleene-Vesley realizability the $\lnot\lnot$-dense modest instance degreescorrespond precisely to Weihrauch degrees. The extended degrees improve thestructure of Weihrauch degrees by equipping them with computable infima andsuprema, an implication, the ability to control access to parameters andcomputation of results, and by generally widening the scope of Weihrauchreducibility