intuitionistic topology & foundations of constructive mathematics

welcome to the math page of frank waaldijk. as you can guess from the title, my interests are mainly in intuitionism, topology and constructive mathematics. 

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 (4 publications, click on the blue for pdf files and a more detailed description): 

• Natural Topology (2011, 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 (1996)

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

Natural topology (click for .pdf)

(2011, published by the Brouwer Society, .pdf 1.1 Mb)

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 preserve this Heine-Borel property. 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).

~

Postscriptum: As always, after finishing I come across omissions, typos, and sometimes errors. I will probably post some addenda on my math blog. An important but not difficult addendum concerns the composition of path morphisms. 

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. Slow as I am, only recently I came across the nice new (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 even kindly referenced. For this, I am truly grateful.
   
   
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, 1Mb]) 

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