Fan/bar theorems and Cantor/Baire spaces/locales
Toby Bartels
Now I have a question.
What generally is known about the relationships between
Brouwer's fan and bar theorems (or "theorems") on the one hand
and the topological properties of Cantor and Baire space on the other?
I'm particularly interested in the question of whether
the localic (or formal) Cantor and Baire spaces are spatial,
or if you prefer whether these topological spaces are sober.
That and the question of whether Cantor space is compact.
--Toby Bartels
gc...@math.unipd.it
> What generally is known about the relationships between
> Brouwer's fan and bar theorems (or "theorems") on the one hand
> and the topological properties of Cantor and Baire space on the other?
> I'm particularly interested in the question of whether
> the localic (or formal) Cantor and Baire spaces are spatial,
> or if you prefer whether these topological spaces are sober.
> That and the question of whether Cantor space is compact.
M. Fourman, R. Grayson, ``Formal Spaces''. In: The
L.E.J. Brouwer Centenary Symposium, A.S. Troelstra and D. van
Dalen, eds. North Holland (1982), pp. 107-122.
is the classical reference on this topic.
Compactness of Cantor space <--> fan theorem <--> spatiality of formal Cantor
space.
Spatiality of formal Baire space <--> bar induction.
Best regards,
Giovanni Curi
-----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.
Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it
Paul Taylor
quite complex) question about the relationship between Brouwer's fan/bar
theorems and the topological properties of Cantor and Baire space.
However, I would like to take this opportunity to request that the experts
- pause to give a simple explanation of what Brouwer's somewhat
mysterious principles mean, and then
- take certain ALTERNATIVE points of view into consideration.
Bishop (and before him the Russian Recursive Analysts) had either to
adopt the fan principle or to reject (Heine--Borel) compactness of
Cantor space etc (and with it a simple definition of continuity that
includes the reciprocal function).
This was because they started from SETS OF POINTS.
There are, on the other hand, three theories of general topology that
are based on OPEN SUBSPACES instead of points, namely LOCALE THEORY,
FORMAL TOPOLOGY and ABSTRACT STONE DUALITY. In each of these,
Cantor space and the real closed interval are compact in the
Heine--Borel sense.
Bishop's followers like to say that the Heine--Borel theorem
is "not constructive", or that it depends on the Fan Theorem.
The practitioners of these three theories, on the other hand,
also consider themselves to be "constructive" mathematicians,
but they accept Heine--Borel whilst having no need for the Fan Theorem.
In particular, ASD's claim to constructivity is based on the fact
that every term is in principle a program, and I am currently working
on the theory behind turning that principle into practice.
All of the comments that I am making here, both about ASD and the
other theories, have more extensive explanation and references in
"The Dedekind Reals in Abstract Stone Duality
by Andrej Bauer and Paul Taylor
Mathematical Structures in Computer Science
August 2009, volume 19, pages 757--838
www.PaulTaylor.EU/ASD/dedras/
whilst the applications to elementary real analysis are in my
"A Lambda Calculus for Real Analysis"
www.PaulTaylor.EU/ASD/lamcra/
which has just been given final approval by the referees for another
journal.
Before we embarked on our paper, Andrej gave me quite a grilling, in
November 2004, because he too was skeptical that a recursive theory
could have the Heine--Borel theorem. We tried hard to find some way
in which ASD was related to the Fan Theorem, but we couldn't. So I
would really like to hear how the claim that Heine--Borel necessarily
depends on the Fan Theory applies to ASD.
When we regard topology as lambda-calculus, open subspaces of X
correspond bijectively to (continuous) maps X-->Sigma (as do closed
subspaces), and any compact subspace K gives rise to a (continuous) map
All_K: (X-->Sigma) --> Sigma.
Having introduced one term of higher type, of course we can define
others from it.
In particular, the (Dedekind) real line and Cantor space are subspaces
i:R >-----> Sigma^Q x Sigma^Q and i:2^N >----> Sigma^{N x N}
and they carry the subspace topology in a canonical way,
in the sense that there are (continuous) maps
I: Sigma^R --> Sigma^{Sigma^Q x Sigma^Q}
and I: Sigma^{2^N} --> Sigma^{Sigma^{NxN}}
such that Sigma^i . I = id.
These maps are interdefinable with the "All_K" that say that
the closed interval and Cantor space are (Heine--Borel) compact.
The theories that satisfy Heine--Borel can define the "I" maps,
whilst those that don't, can't.
While I have been writing this, Giovanni Curi got in with a citation
of Fourman and Grayson. The situation is similar to the need for the
Axiom of Choice to prove Tychonov's theorem and other results in
general topology: Locale Theory does not need Choice to prove
these theorems in the way that it understands them -- but Choice
is needed to find enough points to translate the theorem about
open subspaces into one about points.
I have a hunch that, in the next few years, the gradation in strength
classical topology > locale theory > formal topology > ASD
will begin to become more significant. I also think that the
stronger theories will raise more questions that lead to the need
for additional principles.
Using Dependent Choice, in both locale theory and ASD,
every definable overt subspace of Cantor space
is the direct image of an open subspace of N
in the sense that <>phi = Some n.phi(f n). I expect that this
is also true in formal topology, but I am not sufficiently familiar
with its foundations to prove it. It is trivial classically.
Since the stronger theories have more definable points, they have
more overt subspaces too.
Paul Taylor
Kreinovich, Vladik
The proof is very similar to the classical proof of Konig's lemma, we just need to show that is no such B exists, then the corresponding counter-example sequence is indeed pseudo-converging.
Toby Bartels
>M. Fourman, R. Grayson, ``Formal Spaces''. In: The
>L.E.J. Brouwer Centenary Symposium, A.S. Troelstra and D. van
>Dalen, eds. North Holland (1982), pp. 107-122.
>Compactness of Cantor space <--> fan theorem <--> spatiality of formal Cantor space.
>Spatiality of formal Baire space <--> bar induction.
Excellent, thank you, that is just what I was hoping for!
I am away from a library that has a copy of the cited proceedings,
but I'll check there for the details.
--Toby
Toby Bartels
>Bishop (and before him the Russian Recursive Analysts) had either to
>adopt the fan principle or to reject (Heine--Borel) compactness of
>Cantor space etc (and with it a simple definition of continuity that
>includes the reciprocal function).
It was Frank Waaldijk who put me wise to the last point;
see his papers at <http://home.kpn.nl/sufra/mathematics.html>.
He proves in BISH that the fan theorem is equivalent
to the existence of a reasonable notion of continuous function
(where of course he specifies what me means by "reasonable")
in a point-based approach to real analysis.
>This was because they started from SETS OF POINTS.
Since I see that this list sometimes has religious debates,
I'll state for the record where my sympathies lie:
with the "pointless" approaches to topology such as ASD.
Then Brouwer's work on bars and fans is simply not necessary.
Nevertheless, I'm also curious about what they amount to
in the traditional point-based approach.
--Toby
Paul Taylor
Hang on a minute, Toby, this is not FOM -- we are a family here, even
if we belong to different faiths. In particular, I have a very great
respect for Peter Schuster and Douglas Bridges.
I would, as I said, like to hear a good explanation of the Fan
Theorem.
When I challenge Bishop's followers (and others) to point out to me
where the Fan Theorem is connected with ASD and the other point-free
theories, I do so entirely in the spirit of scientific dialogue.
Paul Taylor
Fan Theorem, which I did honestly want to hear.
The following is connected with it in so far as I was concerned for a
long time that a Kleene tree might be involved in this, but it seems
not. Stephen Kleene is nevertheless involved in another way, namely
that this result depends on choice principles that (in ASD) are
themselves consequences of the Kleene normal form, on which I have
been working recently.
THEOREM Every non-parametric overt subspace of 2^N or R is of the form
<> V = Some y:M. (g y in V)
for some continuous function g:M-->2^N or R, where
M is an overt discrete Hausdorff (or "recursively enumerable") space.
PROOF See www.PaulTaylor.EU/drafts/overt-subsp.pdf for details.
Sketch: Both spaces have bases that are indexed by finite sequences;
in the case of R this representation is known as signed binary.
For any sequence A let (A) and [A] be the open and closed intervals
that it names.
Then
theta A = <>(A) = <>(A.(-1)) union <>(A.0) union <>(A.(+1)) ,
so, using dependent choice, we may extend any finite sequence A that
satisfies <>(A) to an infinite one of which any finite subsequence B
has <>(B).
In the case of R, the infinite sequence starting with A defines a real
number gA that belongs to [A], but not necessarily (A). Nevertheless,
if gA lies in (D) then we can show that <>(D).
Let M be the subspace of finite sequences A with <>(A) and g:M-->2^N or R
the function that we have just defined. Then <> is the direct image
of g. QED
Notice that this argument uses (dyadic) rational arithmetic,
convergence of Cauchy sequences and dependent choice, but not Dedekind
completeness or Heine--Borel. Apart perhaps from the dependent
choice, the result should be acceptable in any form of constructive
topology or analysis, although I am not sufficiently proficient in
Formal Topology to speak for that.
In constructive real analysis we therefore now have a very strong
connection amongst overtness, locatedness, total boundedness,
recursive enumerability and the Bolzano theorem.
On the other hand, it shows that overtness (and the other properties)
depend on the strength of the underlying logical system.
Paul Taylor
Bas Spitters
> In constructive real analysis we therefore now have a very strong
> connection amongst overtness, locatedness, total boundedness,
> recursive enumerability and the Bolzano theorem.
I have collected some connections that I am aware of in the papers below.
Indeed, overtness and locatedness are closely connected, but there are
important differences.
For instance, locatedness is not a topological, or even a metric property.
In the presence of compactness the connection is indeed very strong.
Best,
Bas
Locatedness and overt sublocales
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.
http://arxiv.org/abs/math/0703561
Metric complements of overt closed sets
Thierry Coquand, Erik Palmgren, Bas Spitters
We show that the set of points of an overt closed subspace of a metric
completion of a Bishop-locally compact metric space is located.
Consequently, if the subspace is, moreover, compact, then its
collection of points is Bishop compact.
http://arxiv.org/abs/0906.3433
Paul Taylor
Thanks to Bas for giving us the references to his papers "Locatedness
and overt sublocales" and "Metric complements of overt closed sets".
We had a discussion about overtness and related concepts in Padova
three years ago. Maybe it is time that we turned my notes of this,
www.PaulTaylor.EU/drafts/overt-brainstorm
into something slightly more formal - at least LaTeX and HTML!
Does anyone else have any papers or notes to add to this?
However, I should clarify that my note yesterday was about OVERT
subspaces of R and 2^N that are NOT NECESSARILY COMPACT, or even closed:
* Every <> operator is <>V = Some m.(g m in V) for some g:M-->R
* where M is overt discrete Hausdorff (recursively enumerable).
So I am thinking of connections, not only with locateness in
constructive analysis, but also recursively enumerable subsets
in Weihrauch's TTE.
I also wonder whether overtness might throw some light on the use
of dense subsets in classical analysis (Bolzano's theorem).
Paul
Andrej Bauer
> theta A = <>(A) = <>(A.(-1)) union <>(A.0) union <>(A.(+1)) ,
> so, using dependent choice, we may extend any finite sequence A that
> satisfies <>(A) to an infinite one of which any finite subsequence B
> has <>(B).
It should be possible to weaken Dependent Choice here to ordinary
Countable Choice. First, using Countable Choice, give yourself a
function c which chooses -1, 0 or +1 for each A such that <>(A) =
<>(A.(c(A)). Then you can extend A by repeated uses of c:
A_0 = A
A_{n+1} = A_n.(c(A_n))
Does this work?
By the way, how far does your result generalize? It seems to me it
should generalize quite a bit.
With kind regards,
Andrej
Paul Taylor
to ordinary Countable Choice. Indeed, I prove dependent choice in ASD
(ie for Sigma^0_1 predicates) from countable choice in Section 10 of
"Computability in locally compact spaces", on which I have been working:
www.PaulTaylor.EU/drafts/Kleene.pdf
Countable choice is in turn derived from the Kleene normal form for
my calculus. This amounts to the same thing as translating ASD into
PROLOG, about which I have been waving my hands for ten years now.
Since most of that paper is therefore about (the theory of) practical
computing, I felt embarrassed to use such a spectacularly infeasible
argument as is needed to prove Countable Choice. So I also thought of
a principle of "Feasible Choice": if the final result is independent
of the actual choice that is made, this choice can be simulated by
"memoising" the predicate.
Also, as Andrej says, the result about overt subspaces of R ought to
generalise a lot, and not just to R^n. I am trying to thing of a
way of defining a "graded basis" for any locally compact space that
would be analogous to using subsets of diameter 2^(-m) in R^n.
The note about overt subspaces of R,
www.PaulTaylor.EU/drafts/overt-subsp.pdf
also includes a result from a conference paper in 2002 that never
made it into the 2006 journal version; this is about filter bases
and the Baire category theorem in ASD.
The reason for thinking about this topic at this moment, and writing
out the proof of the characterisation of overt subspaces of R, is
that I wave my hands about dependent choice in "A lambda calculus
for real analysis", which will be going "to press" very shortly.
I wanted to be sure that overt subspaces of R and Cantor space,
unlike compact ones, would not involve Kleene trees.
Paul
Andrej Bauer
> generalise a lot, and not just to R^n. I am trying to thing of a
> way of defining a "graded basis" for any locally compact space that
> would be analogous to using subsets of diameter 2^(-m) in R^n.
Yes, I think several people on this list must have wondered about
"graded basis". I don't think there is a single answer. The last time
I hit against "graded basis" I settled for metric spaces and thought
it should be possible to do it with uniformities.
In your particular case I'd first try something easy. For example,
consider a locally compact space X with a basis U_i \subset K_i where
U_i is open and K_i is the associated compact set. Suppose in addition
that the K_i's are images of Cantor space (this will also mean they
are overt). The i's range over something that's like N (overt,
discrete, Hausdorff). Can't you then get a characterization of overt
subspaces of X from a characterization of overt subspaces of 2^N?
But I don't recall or know off the top of my head how often compact
overt subspaces are images of 2^N in ASD.
Perhaps all this is getting too specific for the general audience on this list.
With kind regards,
Andrej