Lab Lunch: 22 June 2021 - Michael Fourman

Title: Points and Spaces: Brouwer’s Choice Sequences Revisited

Abstract:

I will describe some work originally motivated by my ongoing interest in Brouwer’s Intuitionistic Mathematics. Brouwer describes Intuitionism as composed of, "two acts of which the first seems necessarily to lead to destructive and sterilizing consequences, whereas the second yields ample possibilities for recovery and new developments.” In the first act, Brouwer introduces a constructive interpretation of the logical connectives. In particular a constructive interpretation of the quantifiers leads Brouwer to a rejection of the law of the excluded middle — the tertium non datur of classical logic. The resulting intuitionistic logic was formalised by Heyting. In the first act Brouwer also admits inductively defined types, such as finite sequences and trees, and even infinitely proceeding sequences generated by laws. It is natural to identify such lawlike sequences with total recursive function,  The resulting constructive mathematics can readily be understood by a classical mathematician as a sterilised subset of classical mathematics. As a topologist, Brouwer found this first act incomplete — it does not provide a satisfactory account of the real continuum. To do this, Brouwer’s second act was to introduce the idea of an idealised mathematician creating choice sequences whose successive values are chosen, more or less freely, by this creating subject. By reflection on this intuition Brouwer derived a “proof” of an induction principle, Bar Induction, which he used to derive his theory of the continuum, including, for examples, the Heine-Borel theorem closed intervals are compact. The status of Brouwer’s “proof" has been the object of much discussion and controversy. To illustrate the notion of choice sequence, Brouwer pictures two mathematicians: A calls out successive values, freely chosen; B, following some law, constructs her own sequence, derived from the values called by A. We represent such a construction, of a choice sequence from a free choice sequence, as a monotone total recursive function from finite sequences to finite sequences, with the property that every infinite chain of inputs (corresponding to the successive values called by A), will lead B to construct an infinite sequence of outputs. [Imagine a Haskell function on infinite lists that computes successive initial segments of its output given successive initial segments of the input.] This leads us to model the inferences that an idealised mathematician might draw, by reflection on this model. We arrive at a simple (simple in the sense that it is described within the constructive mathematics of the first act) monoid model (in the sense of sheaves and logic) in which the Bar Induction principle is valid.