Sheaf models for choice sequences (Q798316)

The paper deals with models for intuitionistic theories of choice sequences in sheaves over monoids of continuous functions and in sheaves over topological spaces (some of them with a group-action). First it is shown that the internal Baire space in sheaves over the monoid of continuous maps from Baire space to Baire space (Cts(B,B)) is a model for the Kreisel-Troelstra theory CS. Restrictions to suitable submonoids of Cts(B,B) give rise to models of relativizations of CS with less closure properties. The next result presented is that the interpretation of CS in sheaves over Cts(B,B), when dealt with in a constructive metatheory, is (litterally) the elimination translation for CS. Then it is shown that with each of the monoid models for CS and its relativizations there is a corresponding model in sheaves over a topological space, whose points are sequences of elements of Cts(B,B). These spatial models are first order equivalent to the monoid models. The final sections of the paper deal with a sheaf model for the theory LS of lawless sequences in sheaves with a group action over a topological space homeomorphic to Baire space, and with the explanation of our interest in models in sheaves over topological spaces resembling Baire space: such models can be viewed as so called projection models, and may thus provide a reduction from various notions of choice sequence to the concept of lawlessness.