Nuria Brede (IRIF), On a generic approach to constructive reverse mathematics

Schedule

Abstract

In joint work with Hugo Herbelin https://inria.hal.science/hal-03144849, we studied different choice and bar induction principles from a "generic" perspective: We showed how weak Kőnig's lemma, the fan theorem, bar induction, dependent choice, the Boolean prime ideal theorem and general choice have common contrapositive generalisations. In the talk, I will revisit this work and put it into perspective of an ongoing classification and formalisation effort to constructively relate various logical principles which are classically equivalent to choice axioms.