Sheaf models for choice sequences
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.
- Model theory for sheaves of modules
- scientific article; zbMATH DE number 7700630
- scientific article; zbMATH DE number 120343
- scientific article; zbMATH DE number 31601
- Some model theory of sheaves of modules
- scientific article; zbMATH DE number 6845518
- Sheaves of ordered spaces and interval theories
- scientific article; zbMATH DE number 1400011
- Sheaves over infinite posets
- Model category structures on chain complexes of sheaves
- A remark on free choice sequences and the topological completeness proofs
- An interpretation of intuitionistic analysis
- Concepts of general topology in constructive mathematics and in sheaves
- First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
- Formal systems for some branches of intuitionistic analysis
- Grothendieck toposes have boolean points a new proof
- scientific article; zbMATH DE number 3645093 (Why is no real title available?)
- scientific article; zbMATH DE number 3691320 (Why is no real title available?)
- scientific article; zbMATH DE number 3779318 (Why is no real title available?)
- scientific article; zbMATH DE number 3552491 (Why is no real title available?)
- scientific article; zbMATH DE number 3216177 (Why is no real title available?)
- scientific article; zbMATH DE number 3253161 (Why is no real title available?)
- scientific article; zbMATH DE number 3334147 (Why is no real title available?)
- Open maps of toposes
- A constructive manifestation of the Kleene-Kreisel continuous functionals
- scientific article; zbMATH DE number 7229466 (Why is no real title available?)
- scientific article; zbMATH DE number 3867322 (Why is no real title available?)
- scientific article; zbMATH DE number 3941537 (Why is no real title available?)
- Small decidable sheaves
- Higher order functions and Brouwer's thesis
- A syntactic approach to continuity of T-definable functionals
- A Gentzen-style monadic translation of Gödel's system T
- Separating Markov's principles
- Extended bar induction in applicative theories
- Smooth spaces versus continuous spaces in models for synthetic differential geometry
This page was built for publication: Sheaf models for choice sequences
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q798316)
