Spitters, Bas
Constructive algebraic integration theory without choice
Abstract
We present a constructive algebraic integration theory. The theory is constructive in the sense of Bishop, however we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos. Since we avoid impredicative methods the results may also be interpreted in MartinLÃƒÂ¶f type theory or in a predicative topos in the sense of Moerdijk and Palmgren.
We outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the
Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem.
BibTeX  Entry
@InProceedings{spitters:DSP:2006:290,
author = {Bas Spitters},
title = {Constructive algebraic integration theory without choice},
booktitle = {Mathematics, Algorithms, Proofs},
year = {2006},
editor = {Thierry Coquand and Henri Lombardi and MarieFran{\c{c}}oise Roy},
number = {05021},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Internationales Begegnungs und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2006/290},
annote = {Keywords: Algebraic integration theory, spectral theorem, choiceless constructive mathematics, pointfree topology}
}
2006
Keywords: 

Algebraic integration theory, spectral theorem, choiceless constructive mathematics, pointfree topology 
Seminar: 

05021  Mathematics, Algorithms, Proofs

Related Scholarly Article: 


Issue date: 

2006 
Date of publication: 

2006 