Logical Structure: Choice and Bar Induction Principles

This lecture discusses the logical structure of principles equivalent to choice and bar induction. It begins by examining the contrapositive of bar induction, leading to the introduction of a generalized notion of dependent choice, termed GDC, which relates to a predicate on finite approximations of functions. The instructor outlines the strengths of GDC in various contexts, such as when A is countable or when B is a two-element set. The lecture also covers standard reverse mathematics of the axiom of choice, presenting well-known equivalent formulations like Zorn's lemma and the well-ordering principle. The instructor emphasizes the logical and computational perspectives of the axiom of choice, highlighting how intuitionistic proofs can be viewed as programs. Contributions include a classification of choice and bar induction principles and a discussion on maximality principles. The lecture concludes with a summary of the main results regarding choice and bar induction, illustrating the connections between these principles and their implications in constructive mathematics.