In intuitionistic mathematics, the concept of choice sequence introduced by L.E.J. Brouwer is a constructive notion of sequence that admits “free choices” (i.e. not necessarily “determined by a law”).
This has been formalized in various ways, sometimes by writing down axioms that follow from Brouwer’s philosophical description, other times by constructing models such as sheaf toposes.
Discussion of models for choice sequences in various sheaf toposes (usually involving Baire space or Cantor space) include:
Gerrit Van Der Hoeven? and Ieke Moerdijk, Sheaf models for choice sequences, Annals of Pure and Applied Logic, Volume 27, Issue 1, August 1984, Pages 63-107, DOI
Michael Fourman, Notions of Choice Sequence, Studies in Logic and the Foundations of Mathematics, Volume 110, 1982, Pages 91-105, DOI
Thierry Coquand, On a model of choice sequences, pdf
Last revised on April 10, 2019 at 20:58:52. See the history of this page for a list of all contributions to it.