2009

Foundations of Physics. Available at the arxiv as 0902.3201 bib

Communications mathematical physics. Available at the arxiv as 0709.4364. bib
Abstract We show how a C*-algebra naturally induces a topos in which the family of its commutative subalgebras becomes a commutative C*-algebra. Its internal spectrum is a compact regular locale, and the Kochen-Specker theorem is equivalent to this spectrum having no points. (Quasi-)states become integrals, and self-adjoint elements become functions to the pertinent generalised real numbers (the interval domain). This provides a probabilistic interpretation of propositions in quantum theory. The topos-theoretic truth value of such a proposition is the collection of pure states of commutative subalgebras that make it true; in a physical interpretation these are the pure states for a classical observer making the proposition true. These results were motivated by a topos-theoretic approach of the Kochen-Specker theorem by Isham and co-workers. Our main tool is the use of the internal mathematics of a topos, such as the constructive Gelfand duality of Banaschewski and Mulvey, which simplifies the computations and provides very natural connections between internal and external reasoning.

Integrals and Valuations (with Thierry Coquand) 

Logic and Analysis 1(3) p1-22. Available at the arxiv as 0808.1522 bib

Abstract We construct a homeomorphism between the compact regular locale of integrals on a Riesz space and the locale of (valuations) on its spectrum. In fact, we construct two geometric theories and show that they are biinterpretable. The constructions are elementary and mostly consist of explicit manipulations on a distributive lattice associated to a given Riesz space.

Constructive Gelfand duality for C*-algebras (with Thierry Coquand)

Mathematical Proceedings of the Cambridge Philosophical society 2009. Available at the arxiv as 0808.1518 bib.
Abstract We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras.

2007

The principle of general tovariance (with Chris Heunen and Klaas Landsman) Proc. XVI International Fall Workshop on Geometry and Physics (Lisbon, 2007), editor R. Picken et al., American Physical Society, 2008.
00003931 bib
Abstract We tentatively propose two guiding principles for the construction of theories of physics, which should be satisfied by a possible future theory of quantum gravity. These principles are inspired by those that led Einstein to his theory of general relativity, viz. his principle of general covariance and his equivalence principle, as well as by the two mysterious dogmas of Bohr's interpretation of quantum mechanics, i.e. his doctrine of classical concepts and his principle of complementarity. An appropriate mathematical language for combining these ideas is topos theory, a framework earlier proposed for physics by Isham and collaborators.
Our "Principle of general tovariance" states that any mathematical structure appearing in the laws of physics must be definable in an arbitrary topos (with natural numbers object) and must be preserved under so-called geometric morphisms. This principle identifies geometric logic as the mathematical language of physics and restricts the constructions and theorems to those valid in intuitionism: neither Aristotle's principle of the excluded third nor Zermelo's Axiom of Choice may be invoked. Subsequently, our "Equivalence principle" states that any algebra of observables (initially defined in the topos Sets) is empirically equivalent to a commutative one in some other topos.

Constructive analysis, types and exact real numbers. (with Herman Geuvers, Milad Niqui and Freek Wiedijk)
Constructive analysis, types and exact real numbers, special issue of Mathematical Structures in Computer Science (Bas Spitters, Herman Geuvers, Milad Niqui and Freek Wiedijk(eds.)) MSCS Volume 17, Issue 01, pp 3-36, 2007.
doi:10.1017/S0960129506005834 pdf bib
Abstract In the present paper, we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real arithmetic varying from concrete implementations, representation and algorithms to various models for real computation. We then put these models in a uniform framework using realisability, opening the door for the use of type theoretic and coalgebraic constructions both in computing and reasoning about these computations. We will indicate that it is often natural to use constructive logic to reason about these computations.

2006

A constructive view on ergodic theorems
Journal of Symbolic Logic, June 2006, 71(2) pp. 611-623
pdf bib tm html
Abstract Let T be a positive L₁-L_∞ contraction. We prove that the following statements are equivalent in constructive mathematics.

1. The projection in L₂ on the space of invariant functions exists;
2. The sequence (Tⁿ)_n∈N Ces�ro-converges in the L₂ norm;
3. The sequence (Tⁿ)_n∈N Ces�ro-converges almost everywhere.

2005

Constructive Results on Operator Algebras
Journal of Universal computation volume 11, issue 12 2005.
ps.gz pdf bib tm html
AbstractWe present a to following results in the constructive theory of operator algebras. A representation theorem for finite dimensional von Neumann-algebras. A representation theorem for normal functionals. The spectral measure is independent of the choice of the basis of the underlying Hilbert space. Finally, the double commutant theorem for finite von Neumann algebras and for Abelian von Neumann algebras.

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems (with Thierry Coquand)
Journal of Universal computation volume 11, issue 12 2005.
A slightly expanded version is available here. bib tm html
Abstract We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.

Constructive algebraic integration theory without choice
In: Thierry Coquand and Henri Lombardi and Marie-Francoise Roy, Mathematics, Algorithms, Proofs, Dagstuhl Seminar Proceedings 05021, Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany.
pdf bib
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� 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.

Almost periodic functions, constructively
LMCS Volume 1, issue 3, paper 4, 2005.
The paper can be downloaded here. bib
AbstractAlmost periodic functions form a natural example of an inseparable normed space. As such, it has been a challenge for constructive mathematicians to find a natural treatment of them. Here we present a simple proof of Bohr's fundamental theorem for almost periodic functions which we then generalize to almost periodic functions on general topological groups.

A constructive proof of the Peter-Weyl theorem (with Thierry Coquand)
Mathematical Logic Quarterly. Vol. 4, 2005, page 351-359. � Wiley VCH
pdf bib
Abstract We present a new and constructive proof of the Peter-Weyl theorem on the represe ntations of compact groups. We use the Gelfand representation theorem for commut ative C*-algebras to give a proof which may be seen as a direct generalization o f Burnside's algorithm. This algorithm computes the characters of a finite group . We use this proof as a basis for a constructive proof in the style of Bishop. In fact, the present theory of compact groups may be seen as a natural continuat ion in the line of Bishop's work on locally compact, but Abelian, groups.

Approximating integrable sets by compacts constructively.
in From Sets and Types to Topology and Analysis - Towards Practicable Foundations for Constructive Mathematics, Laura Crosilla and Peter Schuster (eds.)
ps ps.gz pdf bib
Abstract In locally compact spaces, (Borel-)measurable sets can be approximated by compact sets. Ulam [Oxtoby/Ulam] extended this result to complete separable metric spaces. We give a constructive proof of Ulam's theorem. It is first proved intuitionistically and then, using a logical `trick' due to Ishihara, a proof acceptable in Bishop-style mathematics is obtained. We feel this proof provides some insight into Ishihara's trick. Finally, we show how several intuitionistic measure theoretic theorems can be extended to regular integration spaces, that is integration spaces where integrable sets can be approximated by compacts. These results may help to understand Bishop's choice of definitions.

Constructive Algebraic Integration theory.
Annals of Pure and Applied Logic. � Elsevier, 2005
doi:10.1016/j.apal.2005.05.031
ps ps.gz pdf bib
Abstract For a long time people have been trying to develop probability theory starting from `finite' events rather than collections of infinite events. In this way one can find natural replacements for measurable sets and integrable functions, but measurable functions seemed to be more difficult. We present a solution. Moreover, our results are constructive (in the sense of Bishop).

2003

Program extraction from large proof developments. (with Lu�s Cruz-Filipe).
in Proceedings of 16th International Conference TPHOLs 2003 (in LNCS proceedings), D. Basin and B. Wolff (eds.), pages 205--220, LNCS 2758, 2003 � Springer-Verlag 2003 ps, ps.gz, pdf, bib.
Abstract It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement these algorithms on a computer; moreover, one runs the risk of making mistakes in the process. From a fully formalized constructive proof one can automatically obtain a computer implementation of such an algorithm together with a proof that the program is correct. As an example we consider the fundamental theorem of algebra which states that every non-constant polynomial has a root. This theorem has been fully formalized in the Coq proof assistant. Unfortunately, when we first tried to extract a program, the computer ran out of resources. We will discuss how we used logical techniques to make it possible to extract a feasible program. This example is used as a motivation for a broader perspective on how the formalization of mathematics should be done with program extraction in mind.

Locating the range of an operator with an adjoint. (with Douglas Bridges and Hajime Ishihara)
Indagationes Mathematicae, 13(4):433-440, 2003. � Elsevier, 2002
ps ps.gz pdf bib
Abstract In this paper we consider the following question: `given a bounded linear operator on a Hilbert space, can we compute the projection on the closure of its range?'

Located Operators.
Mathematical Logic Quarterly, 48(Suppl. 1):107-122, 2002. � Wiley, VCH 2002
ps ps.gz pdf bib
Abstract We study operators with located graph in Bishop-style constructive mathematics. It is shown that a bounded operator has an adjoint if and only if its graph is located. Locatedness of the graph is a necessary and sufficient condition for an unbounded normal operator to have a spectral decomposition. These results suggest that located operators are the right generalization of bounded operators with an adjoint.

Constructive and intuitionistic integration theory and functional analysis.
Ph. D. thesis, University of Nijmegen, 2002
pdf bib

A constructive converse of the mean value theorem. (with Wim Veldman)
Indagationes Mathematicae, 11(1):151-157, 2000. � Elsevier, 2000
ps ps.gz pdf bib
Abstract Consider the following converse of the Mean Value Theorem.
Let f be a differentiable function on [a,b]. If c in (a,b), then there are alpha and beta in [a,b] such that f(beta)-f(alpha)/(beta -alpha)=f'(c).
Assuming some weak conditions to be mentioned in Section 3, Tong and Braza were able to prove this statement. Unfortunately their proof does not provide a method to compute alpha and beta. We give a constructive proof.

Preprints

Metric complements of overt closed sets (jww Thierry Coquand and Erik Palmgren)

Available in the arxiv as 0906.3433. bib

Bohrification of operator algebras and quantum logic (with Chris Heunen and Klaas Landsman)

Locatedness and overt sublocales

Available in the arxiv as 0703561. bib
Abstract: Locatedness is one of the fundamental notions in constructive mathematics.
The existence of a positivity predicate on a locale, i.e. the locale being
overt, or open, has proved to be fundamental in constructive locale theory.
We show that the two notions are intimately connected.
Bishop defines a metric space to be compact if it is complete and totally
bounded. A subset of a totally bounded set is again totally bounded iff it
is located. So a closed subset of a Bishop compact set is Bishop compact iff
it is located. We translate this result to formal topology. `Bishop compact'
is translated as compact and overt. We propose a definition of located
predicate on subspaces in formal topology. We call a sublocale located if it
can be presented by a formal topology with a located predicate. We prove
that a closed sublocale of a compact regular locale has a located predicate
iff it is overt. Moreover, a Bishop-closed subset of a complete metric space
is Bishop compact --- that is, totally bounded and complete ---  iff its localic completion is compact overt.
Finally, we show by elementary methods that the points of the Vietoris
locale of a compact regular locale are precisely its compact overt
sublocales.
We work constructively, predicatively and avoid the use of the axiom of
countable choice. Consequently, all our results are valid in any predicative
topos.

Constructive pointfree topology eliminates non-constructive
representation theorems from Riesz space theory

Available at the arxiv as 0807.2454 bib

Abstract: In Riesz space theory it is good practice to avoid representation theorems
  which depend on the axiom of choice. Here we present a general methodology
  to do this using pointfree topology. To illustrate the technique we show
  that almost f-algebras are commutative. The proof is obtained relatively
  straightforward from the proof by Buskes and van Rooij by using the
  pointfree Stone-Yosida representation theorem by Coquand and Spitters.

A computer verified, monadic, functional implementation of the integral. (with Russell O'Connor)

Available at the arxiv as 0809.1552 bib