License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05021.9
URN: urn:nbn:de:0030-drops-2905
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/290/
Go to the corresponding Portal

Spitters, Bas

Constructive algebraic integration theory without choice

pdf-format:
05021.SpittersBas1.Paper.290.pdf (0.3 MB)

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 Martin-Lö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:DagSemProc.05021.9,
  author =	{Spitters, Bas},
  title =	{{Constructive algebraic integration theory without choice}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/290},
  URN =		{urn:nbn:de:0030-drops-2905},
  doi =		{10.4230/DagSemProc.05021.9},
  annote =	{Keywords: Algebraic integration theory, spectral theorem, choiceless constructive mathematics, pointfree topology}
}

Keywords: Algebraic integration theory, spectral theorem, choiceless constructive mathematics, pointfree topology
Collection: 05021 - Mathematics, Algorithms, Proofs
Issue Date: 2006
Date of publication: 16.01.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI