Constructive algebraic integration theory without choice

TY - GEN

T1 - Constructive algebraic integration theory without choice

AU - Spitters, Bas

N1 - Publisher Copyright: © 2006 Dagstuhl Seminar Proceedings. All rights reserved.

PY - 2006

Y1 - 2006

N2 - 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 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.

AB - 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 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.

KW - Algebraic integration theory

KW - choiceless constructive mathematics

KW - pointfree topology

KW - spectral theorem

UR - http://www.scopus.com/inward/record.url?scp=85134953181&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:85134953181

SN - 1862-4405

VL - 5021

JO - Dagstuhl Seminar Proceedings

JF - Dagstuhl Seminar Proceedings

T2 - Mathematics, Algorithms, Proofs 2005

Y2 - 9 January 2005 through 14 January 2005

ER -