Andrej Bauer: Instance reducibilities

Abstract: Starting from a common proof technique for showing that one universal statement implies another universal statement, we identify a notion of logical reduction, which we call instance reducibility. We study instance reducibilities in a constructive setting (because it is trivial in classical logic) and show that it has rich structure. We then relate the instance reducibilities to Weirauch reducibility in computable mathematics. The relationship suggests a generalization of Weirauch reducibility that gives a better behaved structure of degrees.

 This is joint work with Kazuto Yoshimura from JAIST.