intuitionistic topology & foundations of constructive mathematics

Welcome to my math page. As you can guess from the title, my interests are mainly in intuitionism, topology and constructive mathematics. My research is ongoing (but slow). A paper on exact computation over topological spaces has recently been submitted for publication, and I'm working on a simple (and constructive) proof of the Jordan-Brouwer separation theorem. I also maintain a Math & science & philosophy blog.

Some time ago my dear friend Wim Couwenberg and I started a wonderful project, aiming to explain the ideas behind intuitionism in a simple and enjoyable way.

This resulted in the recent book Natural Topology. The book shows that intuitionism and topology are closely -and very naturally- related.

Here is where you can find Wim's homepage for some interesting mathematical subjects (complex reflection groups, hypergeometric functions, theta functions, diophantine equations, recursive texture mapping, and more).

Some of my research (5 publications, click on the blue for pdf files and a more detailed description):

• Exact computation over topological spaces: constructive theory and practice (preprint 2013)

• Natural Topology (2011, 2012, with big support from Wim Couwenberg)

• On the foundations of constructive mathematics - especially in relation to the theory of continuous functions (2005)

• modern intuitionistic topology (my PhD thesis, 1996)

• Some elementary results in intuitionistic model theory (1996, with Wim Veldman)

 

---

 

Exact computation over topological spaces: constructive theory and practice (click for .pdf)

(2013 preprint, submittted to Logical Methods in Computer Science)

We give an exposition of Natural Topology (NToP), which highlights its advantages for exact computation. The NToP-definition of the real numbers (and continuous real functions) matches the recommendations for exact real computation in [Bauer&Kavkler2008] and [Bauer&Kavkler2009]. We derive similar and new results on the efficient representation of continuous real-valued functions (defined on a suitable topological space). This can be generalized to continuous functions between suitable topological spaces. Other than in [Bauer&Kavkler2009], we do not need Markov’s Principle (but for practice this is a cosmetic difference).

NToP is a conceptually simple theory of topological spaces in BISH. It combines a pointfree with a pointwise approach, by integrating the partial-order on the topological basis with a pre-apartness relation. Simpler than formal topology and (constructive) domain theory, NToP enables a smooth transition from theory to practice. We define ‘natural reals’ as sequences of ‘sufficiently shrinking’ rational intervals. The construction directly yields an apartness topology which is equivalent to the metric topology.

A similar construction works for all ‘effective’ quotient spaces of Baire space (obtained through a $Sigma_{0,1}$-apartness). We work with a countable set of ‘basic dots’ which are usually basic neighborhoods. This allows for an efficient representation of compact spaces by finitely branching trees (contrasting to the framework of formal topology). For the natural reals, we can suffice with lean dyadic intervals. All our spaces are (also) pointwise topological spaces, enabling the familiar pointwise style of BISH and CLASS, as well as an incorporation of earlier constructive work in analysis.

The concept of ‘refinement morphism’ is seen to adequately capture the notion of ‘continuous function’. A refinement morphism simply sends basic dots to basic dots, in such a way that ‘points go to points’. In the case of the reals, every BISH-continuous real function can thus be represented by a morphism sending lean dyadic intervals to lean dyadic intervals. For a large class of spaces we prove that continuous functions can be represented by morphisms, that is if we work in CLASS, INT or RUSS. This then should be enough validation also for BISH. We conclude that NToP addresses the need expressed in [Bauer&Kavkler2008], to have a framework for constructive topology which is both theoretically and computationally adequate.

Errata: So far I have found some minor typos, and an imprecise remark, which I will correct shortly.

 

---

 

Natural topology (click for .pdf)

(2012 Second edition, .pdf 1.1 Mb, first edition 2011)

Also available on arXiv: http://arxiv.org/abs/1210.6288

We develop a simple framework called `natural topology', which can serve as a theoretical and applicable basis for dealing with real-world phenomena. Natural topology is tailored to make pointwise and pointfree notions go together naturally. As a constructive theory in BISH, it gives a classical mathematician a faithful idea of important concepts and results in intuitionism.

Natural topology is well-suited for practical and computational purposes. We give several examples relevant for applied mathematics, such as the decision-support system Hawk-Eye, and various real-number representations.

We compare classical mathematics (CLASS), intuitionism (INT), recursive mathematics (RUSS), Bishop-style mathematics (BISH), formal topology and applied mathematics, aiming to reduce the mutual differences to their essence. To do so, our mathematical foundation must be precise and simple. There are links with physics, regarding the topological character of our physical universe.

Any natural space is isomorphic to a quotient space of Baire space, which therefore is universal. We develop an elegant and concise `genetic induction' scheme, and prove its equivalence on natural spaces to a formal-topological induction style. The inductive Heine-Borel property holds for `compact' or `fanlike' natural subspaces, including the real interval [α,β]. Inductive morphisms respect this Heine-Borel property, inversely. This partly solves the continuous-function problem for BISH, yet pointwise problems persist in the absence of Brouwer's Thesis.

By inductivizing the definitions, a direct correspondence with INT is obtained which allows for a translation of many intuitionistic results into BISH. We thus prove a constructive star-finitary metrization theorem which parallels the classical metrization theorem for strongly paracompact spaces. We also obtain non-metrizable Silva spaces, in infinite-dimensional topology. Natural topology gives a solid basis, we think, for further constructive study of topological lattice theory, algebraic topology and infinite-dimensional topology.

The final section reconsiders the question of which mathematics to choose for physics. Compactness issues also play a role here, since the question `can Nature produce a non-recursive sequence?' finds a negative answer in CT_phys. CT_phys, if true, would seem at first glance to point to RUSS as the mathematics of choice for physics. To discuss this issue, we wax more philosophical. We also present a simple model of INT in RUSS, in the two-player game LIfE (Limited Information for Earthlings).

Addenda and errata can be found on my Math & science & philosophy blog.

 

---

 

On the foundations of constructive mathematics - especially in relation to the theory of continuous functions (click for .pdf)

(2001, revised 2003, published in Foundations of Science , Volume 10, Number 3, September 2005, pp. 249-324, Springer Verlag [.pdf, 400Kb])

This article describes many foundational issues concerning what is known as constructivism in mathematics. First of all a flaw in the foundations of Bishop-style constructive mathematics BISH is discussed. A main theorem shows that the two current BISH-definitions of `continuous function' are not equivalent within BISH, and that -together with the natural properties of `continuous function'- they imply the axiom FT (fan theorem). This problem is closely related to the non-topological definition in BISH of `locally compact'.

The theorem sparks an investigation into the realm of topology, and the axioms underpinning intuitionism (INT), classical mathematics (CLASS), recursive mathematics (RUSS) and BISH.

Some new elegant axioms are introduced, to prove theorems showing that CLASS and INT are far closer than usually believed (`reuniting the antipodes'). The distance to RUSS is seen to be far greater, due perhaps to a philosophical difference regarding `real world' phenomena. In fact this is seen to tie in with the old philosophical debate on determinism. And perhaps with the modern physics' debate as well? In section 7 a real-world experiment is described which could cast an alternative mathematical light on this matter.

Axioms of choice are discussed (since the current BISH treatment is unsatisfactory in the author's eyes) and a simple axiom of choice CT₁₁ for RUSS is introduced. This is necessitated by the fact that there can be no common axiom of choice for RUSS on the one hand and CLASS and INT on the other.

The fundamental intuitionistic axiom BT (Bar Theorem or Brouwer's Thesis; also true in CLASS) is presented in a simplified and elegant version, and shown to be equivalent to Kleene's bar induction axiom BI_D combined with the bar-decidable-descent axiom BDD.

 

Remarks:

1. Only as late as 2011 I came across the nice (2006) book Techniques of Constructive Analysis by Douglas Bridges and Luminiţa Simona Vîţă. Unbeknownst to me earlier, it contains a modification of the definition of `continuous function' precisely along the lines of the above article, which is kindly referenced.
   
   
2. Another way for solving continuity problems in BISH: recent developments in formal topology have produced a nice partial solution in the field of constructive formal topology - see Erik Palmgren's paper `Continuity on the real line and in formal spaces'.
   
   
3. We refind this solution also in the contex of natural topology. In the meantime, in my humble opinion I don't think that the problem in general is solved for BISH. Although one can show that every continuous^BIS function from R to R is representable by a continuous mapping (morphism) in the corresponding formal or natural topology (and vice versa), the same cannot be said of R⁺. More specifically: the statement that every continuous^BIS function from [0,1] to R⁺ is representable by a continuous mapping (morphism) between the corresponding formal/natural topologies (which are indicated in the paper above and in the book `Natural topology'), implies the Fan Theorem.

   In the book `Natural topology' there is more discussion on this topic.

   [The issue of BISH continuity was already noted in my PhD-thesis in 1996, see below.]

 

---

 

modern intuitionistic topology (click for .pdf)

(PhD thesis 1996, Radboud University Nijmegen [.pdf, 1.5Mb])

This monograph holds a self-contained modern approach to intuitionistic topology.

First, a foundational framework is built up, including a non-impredicative definition of `topological space', which is classically equivalent to the usual impredicative definition. Local properties, separation axioms, homeomorphisms, compactness, metrizability,... are defined in a natural way, closely paralleling the classical approach.

Some interesting results are obtained. For instance the metrizability of star-finitary spaces, which closely resembles the classical metrization of paracompact spaces. The theory of star-finite refinements is developed to yield the tool of partitions of unity. From there on we prove a constructive version of the Dugundji extension theorem, and an intuitionistic version of the Michael selection theorem.

A promising new concept (although I seem to stand alone in this!) is that of a metric subspace being (strongly) halflocated in its mother space. The beautiful properties of this concept are brought to the fore.

A nice structure arising intuitionistically is an example of a pathwise connected compact space which is not arcwise connected. Many other positive examples are given, as well as counterexamples to natural conjectures.

Errata: a) Remark 3.3.2 is wrong. The in 3.3.2 (by countable induction) defined `weakly stable closure' is not always weakly stable.  For weak stability of the closure one needs to define the weakly stable closure with transfinite induction. Although this does not affect any of the main theorems in chapter 3, some theorems and examples which specifically are about the weakly stable closure should be examined closely to see what part still holds and what is false. The most important falsehood is thm. 3.3.9 that the weakly stable closure of a metric spread is always again spreadlike. This limits -imho- the usefulness of the concept `weakly stable closure'.

`Weakly stable' remains an interesting topological property, in my humble opinion. Wim Veldman has studied a similar concept `perhapsity', with the added benefit of correcting the above errors.

b)The proof of lemma 2.4.4. is incorrect. It is possible to repair this, by invoking AC₁₀ or by a more detailed construction which is given in the corresponding BISH proof in `Natural Topology'. 

 

---

 

Some elementary results in intuitionistic model theory (click for .pdf)

(together with Wim Veldman, the Journal of Symbolic Logic vol. 61, no. 3, pp 745-767, 1996; [.pdf, 1.3 Mb; this is a scanned document retrieved from the university library's webservice])

This paper contains most of the results found during my first two PhD-years on intuitionistic model theory. The rather incomplete abstract states: `We establish constructive refinements of several well-known theorems in elementary model theory. The additive group of the real numbers may be embedded elementarily into the additive group of pairs of real numbers, constructively as well as classically'.

The paper's beautiful style is Wim Veldman's, as he did the actual writing.

Perhaps I will post some additional results which were too complicated to easily include in the above paper.

 

---

 

If you think this site is worthwhile, please consider linking to it. All comments are welcome: info@fwaaldijk.nl. Last modified 22 September 2015.