Re: "Kantor dust"

Re: "Kantor dust"

[Vaughan Pratt]

Prof. Peter Johnstone wrote:
> Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
> looks like, it must (thanks to Lambek) be isomorphic to N x itself,
> and therefore (since equality for N is decidable) must have lots of
> complemented subobjects {0} x itself, {1} x itself, ... The point of
> the continuity theorem for functions R --> R is that there are toposes
> in which R has *no* nontrivial complemented subobjects [...]
> The only way to get round it (apart from using glue)
> is to replace N by some "nonstandard natural number object" having no
> nontrivial complemented subobjects -- but where you get that from, I
> don't know.

You're assuming product distributes over sums, which would be true for
ordinary product but I specified lexicographic product, with the left
argument as the "high order digit" (converse of the usual convention for
ordinal product in ordinal arithmetic).  Why should {0} x N be a
complemented subobject of N x N  when lexicographic product attaches the
"end" of it to {1} x {0} , which I would expect it will in a topos of
sheaves when participating in a final coalgebra for N x X.

Vaughan

Re: "Kantor dust"

[Vaughan Pratt]

Toby Bartels wrote:
> Prof. Peter Johnstone wrote in part:
>
>> The trouble with the Conway construction is not that it's non-
>> constructive, but that it isn't (in any reasonable sense) a
>> construction of the reals. If you stop it at the point when it
>> finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
>> on, then it has also succeeded in constructing lots of non-real
>> numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
>> do you distinguish the numbers you want from the ones you don't?
>
> Can you get anywhere by imposing (at that stage) some Archimedean conditions?
> We need to know first how to interpret natural numbers as Conway numbers,
> then take the subset of those x such that -n < x < n for some n,
> and identify x and y if -1 < (x-y)n < 1 for every n.

Pretty much.  Peter was speaking of day \omega.  With your
identification applied to that day, the only other step needed is to
remove \omega and -\omega and then you have exactly the field R.

A more uniform way of arriving at R is to take the subset consisting of
those numbers expressible as a nonempty proper sup or nonempty proper
inf in an even number of ways.  This is because at day \omega you have
\omega, -\omega, D \cdot 3 in the sense of ordinal product, where D is
the set of dyadic rationals and 3 = {-1/omega < 0 < 1/omega} (the range
of adjustments to each dyadic rational), and the dyadic irrationals.
\omega is a proper sup of the integers but not a nonempty inf (though it
is the empty inf), and dually for -\omega.  The dyadic rationals are not
a proper sup or inf of anything (their increments on either side prevent
this) but the increment on the left is a proper sup but not a proper
inf, and dually on the right.  The dyadic irrationals are both a proper
sup of what's below them and a proper inf of what's above them.

Puzzle.  Bearing in mind that on all days prior to day \omega, every
number satisfies this criterion, on what other days besides day \omega
does this criterion produce a field?

Vaughan

Re: "Kantor dust"

[Bas Spitters]

Let me use this as an excuse to advertise the work of Russell O'Connor, who is
about to complete a PhD in Nijmegen working with me.

O'Connor's project was to implement exact real numbers in type theory in a
machine verified way. His implementation is fairly efficient and completely
verified in the Coq proof assistant.
Real numbers are implemented using (a variant of) Cauchy sequences. He used
the completion monad on metric spaces to write a Haskell-style "effectful"
functional program in Coq (http://arxiv.org/abs/cs/0605058).

He combined the same monad with the list monad to obtain an implementation of
compact sets (pictures, graphs, i.e. Cantor set).
http://arxiv.org/abs/0806.3209

Together we implemented the Riemann integral by combining the step function
monad with the completion monad:
http://arxiv.org/abs/0809.1552

It was very pleasant to see how much category theory pops up naturally when
one tries to implement exact real numbers in a certified way.

To come back to your question: there is a *certified implementation* of
compact sets of the plane. Cantor set is an example of this.
O'Connor's paper includes much more discussion than what I would like to
repeat here. I recommend it.

Bas


On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
> [Note from moderator: this may have been sent incorrectly earlier,
> apologies if you have received it twice.]
>
> Dear Category group,
>
>       Here is a definition of Cantor dust ....
> http://en.wikipedia.org/wiki/Cantor_set.
>
>       My question is from a constructivist viewpoint does this set really
> exist and if so, why?
>
> Very kind regards,
>
> Vasili

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Wed, 11 Feb 2009, Vaughan Pratt wrote:

> Prof. Peter Johnstone wrote:
>>  Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
>>  looks like, it must (thanks to Lambek) be isomorphic to N x itself,
>>  and therefore (since equality for N is decidable) must have lots of
>>  complemented subobjects {0} x itself, {1} x itself, ... The point of
>>  the continuity theorem for functions R --> R is that there are toposes
>>  in which R has *no* nontrivial complemented subobjects [...]
>>  The only way to get round it (apart from using glue)
>>  is to replace N by some "nonstandard natural number object" having no
>>  nontrivial complemented subobjects -- but where you get that from, I
>>  don't know.
>
> You're assuming product distributes over sums, which would be true for
> ordinary product but I specified lexicographic product, with the left
> argument as the "high order digit" (converse of the usual convention for
> ordinal product in ordinal arithmetic).

For goodness' sake, Vaughan! How many times do I have to tell you that
I'm talking about *the underlying object* of the final coalgebra, and
not its order structure or its topology? If the underlying object of
the lexicographic product is the ordinary (cartesian) product -- and
if it's not, then I don't know what it is -- then it distributes over
sums because that's what products do in a topos.

> Why should {0} x N be a
> complemented subobject of N x N  when lexicographic product attaches the
> "end" of it to {1} x {0} , which I would expect it will in a topos of
> sheaves when participating in a final coalgebra for N x X.
>
The order structure can't do any sort of "attaching" that negates the
complementedness of the underlying subobject, and neither can the
topology. The only thing that can do that is to make identifications
between endpoints -- i.e. to use "glue" a la Freyd.

Peter

Re: "Kantor dust"

[Toby Bartels]

Dusko Pavlovic wrote in part:

[Prof. Johnstone responded to most of this, but I want to address one point.]

>there are
>many things that need to be computed with the reals, and no one
>representation fits for all purposes. so the statement

>>nobody uses the binary reals

>probably has more counterexamples than, say, the statement "nobody
>uses toposes". even if "the" binary reals were completely wrong.

What I meant is that no practising constructivist accepts
that the binary reals are the (or a) good notion of real number,
especially since no practising constructivist believes they form a ring.
I don't intend this as a dogamatic statement, and I'd be very interested
to here of any exceptions, but nevertheless I believe that it is true.

I certainly don't mean that nobody, not even a constructivist,
uses the binary reals as an approximation to real numbers
for the purposes of convenient calculations.
And of course, classical mathematicians do believe
that the binary reals are (all of) the reals.

As I suggested in a reply to Steve Stevenson,
constructive mathematics is about what can in principle be computed exactly.
What can in practice be computed closely enough is another question,
quite a useful one to ask but not at all the same thing.
(And what can in practice be computed exactly is another good question,
 one that I'm interested in but don't know enough about.)


--Toby

Re: "Kantor dust"

[Toby Bartels]

Prof. Peter Johnstone wrote in part:

>The trouble with the Conway construction is not that it's non-
>constructive, but that it isn't (in any reasonable sense) a
>construction of the reals. If you stop it at the point when it
>finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
>on, then it has also succeeded in constructing lots of non-real
>numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
>do you distinguish the numbers you want from the ones you don't?

Can you get anywhere by imposing (at that stage) some Archimedean conditions?
We need to know first how to interpret natural numbers as Conway numbers,
then take the subset of those x such that -n < x < n for some n,
and identify x and y if -1 < (x-y)n < 1 for every n.


--Toby

Re: "Kantor dust"

[Toby Bartels]

Vaughan Pratt wrote in part:

>Toby Bartels claims it's obvious, in which case there should be a short
>construction of a nonconstant function from N^N (as a final coalgebra)
>to 2 (or to N, the codomain Toby spoke of) in the topos of sheaves on R.
> Toby, what is it?

An element s of N^N as a final coalgebra of X |-> N x X
decomposes into an element s0 of N and an element s+ of N^N.
In this notation, the easiest of the desired functions is s |-> s0.
Other functions N^N -> N include s |-> s+0, s++0, ...; there are more.
This can be done in any topos (actually in more categories than that).
If any of these is constant, then N is a terminal object,
so if it's an NNO (as it should be to justify the notation N^N)
we are in the terminal category (the inconsistent topos).


--Toby Bartels

Re: "Kantor dust"

[Bhupinder Singh Anand]

On Sunday, February 08, 2009 8:33 PM, Paul Taylor wrote in Categories:

" ... people should be clear about WHICH OF MANY "CONSTRUCTIVE" THEORIES OF
MATHEMATICS they mean as the context of their comments. ... If you want to
construct Cantor space from the reals by the "missing third" construction, I
would think that it makes little difference whether you start from Cauchy or
Dedekind."

Actually, there seem to be two issues involved here.

The minor of the two: that the "missing third" construction yields a
'limit', namely the "Kantor dust";

The other: whether we can agree on any 'constructive' concept at all, such
as, say, the standard interpretation of first-order Peano Arithmetic.

As to the first: Consider an equilateral triangle ABC of height h and side
s. Divide the base AC in half and construct two isosceles triangles of
height h.d and base s/2, where 1>d>0. Iterate the construction on each
constructed triangle ad infinitum.

If the "Kantor dust" is a legitimate (fractal) set, then this construction,
too, should yield a limiting configuration.

Since the height of the constructed triangles at the n'th construction is
h(d^n), and 1>d>0, it would seem that the base AC of the original
equilateral triangle will always be the limiting configuration of the
opposing sides.

This is indeed so if 1/2>d>0, since the total length of the opposing sides
is a Cauchy sequence whose limiting value is, indeed, the length s of the
base AC.

However, if d=1/2, the total length of all the sides opposing their base on
AC is always 2s!

Moreover, if d>1/2, the total length of all the sides opposing their base on
AC is a monotonically increasing value.

(To give it a practical flavour, let s be one light-year, and consider how
long it would take a light signal to travel from A to C along the sides
opposing the base in each of the above cases; and whether it makes any sense
to assert that all the cases must have a limiting configuration.)

So, whatever it is that the "missing third" construction is supposed to
yield, it certainly cannot have any relation to the terms "third",
"construction", "limit" and "set" under any interpretation of these terms
that we normally conceive of in mathematics.

The issue - as Thoralf Skolem emphasised in "Some remarks on axiomatized set
theory", delivered in an address before the Fifth Congress of Scandinavian
Mathematicians in Helsinki, 4-7 August 1922, with respect to the the Axiom
of Choice - is that set-theory admits statements that are essentially
non-verifiable under any conceivable interpretation; statements, moreover,
which do not express any definable content and cannot, therefore, be
expected to communicate any meaningful information unambiguously under
interpretation:

"So long as we are on purely axiomatic ground there is, of course, nothing
special to be remarked concerning the principle of choice (though, as a
matter of fact, new sets are not generated univocally by applications of
this axiom); but if many mathematicians---indeed, I believe, most of
them---do not want to accept the principle of choice, it is because they do
not have an axiomatic conception of set theory at all. They think of sets as
given by specification of arbitrary collections; but then they also demand
that every set be definable. We can, after all, ask: What does it mean for a
set to exist if it can perhaps never be defined? It seems clear that this
existence can be only a manner of speaking, which can lead only to purely
formal propositions---perhaps made up of very beautiful words---about
objects called sets. But most mathematicians want mathematics to deal,
ultimately, with performable computing operations and not to consist of
formal propositions about objects called this or that."

That the problem lies deeper - in fact at the very core of our fundamental
assumptions - is seen if we note that our logical thinking is universally
founded upon the validity of Aristotle's particularisation.

This holds that an assertion such as, 'There exists an x such that F(x)
holds'---usually denoted symbolically by  '(Ex)F(x)'---can be validly
inferred in the classical logic of predicates from the assertion, 'It is not
the case that, for any given x, F(x) does not hold'---usually denoted
symbolically by '~(Ax)~F(x)'.

Now, in his 1927 address, Hilbert reviewed in detail his axiomatisation of
classical Aristotlean predicate logic as a formal first-order
epsilon-predicate calculus, in which he used a primitive choice-function
symbol, 'epsilon', for defining the quantifiers 'for all' and 'exists'.

In an earlier address "On The Infinite", delivered in Munster on 4th June
1925 at a meeting of the Westphalian Mathematical Society, Hilbert had shown
that the formalisation proposed by him would adequately express Aristotle's
logic of predicates if the epsilon-function was interpreted to yield
Aristotlean particularisation.

This, as Hilbert remarked in his 1927 address, was what he had set out to
achieve as part of his 'proof theory':

"... The fundamental idea of my proof theory is none other than than to
describe the activity of our understanding, to make a protocol of the rules
according to which our thinking actually proceeds."

What came to be known later as Hilbert's Program---which was built upon
Hilbert's 'proof theory'---can be viewed as, essentially, the subsequent
attempt to show that the formalisation was also necessary for communicating
Aristotle's logic of predicates effectively and unambiguously under any
interpretation of the formalisation.

This goal is implicit in Hilbert's remarks:

"Mathematics in a certain sense develops into a tribunal of arbitration, a
supreme court that will decide questions of principle---and on such a
concrete basis that universal agreement must be attainable and all
assertions can be verified."

"... a theory by its very nature is such that we do not need to fall back
upon intuition or meaning in the midst of some argument."

The difficulty in attaining this goal constructively along the lines desired
by Hilbert---in the sense of the above quotes---lies in the fact that, as
Rudolf Carnap emphasised in a 1962 paper, "On the use of Hilbert's
epsilon-operator in scientific theories", the Axiom of Choice is formally
derivable as a theorem in a set theory ZF_epsilon, which is, essentially,
Zermelo-Fraenkel set theory where the quantifiers are defined in terms of
Hilbert's epsilon-function.

The significance of this lies in the accepted interpretation of Paul Cohen's
argument in his 1963-64 papers; they are primarily taken as definitively
establishing that the Axiom of Choice is independent of a set theory such as
ZF.

Now, Cohen's argument---in common with the arguments of many important
theorems in standard texts on the foundations of mathematics and
logic---appeals to Aristotle's particularisation when interpreting the
existential axioms of ZF (or statements about ZF ordinals) in the
application of the seemingly paradoxical (downwards) Lowenheim-Skolem
Theorem for legitimising putative models of a language (such as the standard
model 'M' of ZF, and its forced derivative 'N', in Cohen's argument).

Thus, Cohen's argument should really be taken to establish that, not only is
Aristotle's particularisation 'stronger' than the Axiom of Choice, but that
there is no sound interpretation of ZF that can appeal to Aristotle's
particularisation.

Moreover, the larger significance of Hilbert's formalisation of Aristotle's
particularisation is that---in formal languages that prefer the more
familiar '[A]' - as in '[(Ax)]' - as a primitive symbol to Hilbert's more
logical choice function 'epsilon'---it implicitly gives formal legitimacy to
Alfred Tarski's standard definitions of the satisfaction, and truth, of the
formulas of a formal language under an interpretation, since these
definitions faithfully mirror the particular interpretation of Hilbert's
formalisation that appeals to Aristotle's particularisation.

The reason: Under Tarski's definitions, the formally defined logical
constant '[E]' in an occurrence such as '[(Ex)]'---which is formally defined
in terms of the primitive (undefined) logical constant '[Ax]' as '[~(Ax)~
...]'---always appeals to an interpretation such as 'There is some x such
that ...' in any formal first-order mathematical language.

In other words, Tarski's definitions ensure that, if the first-order
predicate calculus of a first-order mathematical language admits
quantification, then any putative model of the language must interpret
existential quantification as Aristotle's particularisation.

Selecting such a strong interpretation---i.e., one which favours Aristotle's
particularisation---for the standard interpretation, say S, of the formal
Peano Arithmetic PA has significant consequences.

For instance, if we accept the logical validity of such interpretation, then
S is sound (i.e., every PA-theorem interprets as true under S.

Further, if S is sound, then PA is omega-consistent (i.e., we cannot have a
PA-formula [F(x)] such that [F(n)] is PA-provable for any given PA-numeral
[n], and [~(Ax)F(x)] is also PA-provable).

Now, in his seminal 1931 paper, Godel showed that if a Peano Arithmetic such
as his formal system P is omega-consistent, then it is incomplete, in the
sense that he could constructively define a P-formula [R(x)] such that
neither [(Ax)R(x)] nor [~(Ax)R(x)] are P-provable.

However, he also showed in this paper that if P is consistent and [(Ax)R(x)]
is assumed P-provable, then [~(Ax)R(x)] is P-provable.

By Godel's definition of P-provability, it follows that there is a finite
sequence [F_1], ..., [F_n] of P-formulas such that [F_1] is [Ax)R(x)], [F_n]
is [~(Ax)R(x)], and, for 2=< i =< n, [F_i] is either a P-axiom or a logical
consequence of the preceding formulas in the sequence by the rules of
inference of P.

Now, a proof sequence of P necessarily interprets as a sound deduction
sequence under any sound interpretation of P. It follows that we cannot have
a sound interpretation of P under which [(Ax)R(x)] interprets as true and
[~(Ax)R(x)] as false.

Since both [(Ax)R(x)] and [~(Ax)R(x)] are closed P-formulas, it follows that
the P-formula [(Ax)R(x) => ~(Ax)R(x)] interprets as true under every sound
interpretation of P.

By Godel's completeness theorem, [(Ax)R(x) => ~(Ax)R(x)] is, therefore,
P-provable; whence [~(Ax)R(x)] is P-provable.

Since Godel also showed that, if P is consistent, then [R(n)] is P-provable
for any given P-numeral [n], it follows that P is not omega-consistent.

Since Godel's argument holds in PA, we further have that the standard
interpretation S of PA is not sound; moreover, no sound interpretation of PA
can appeal to Aristotle's particularisation!

Thus the difficulty in agreeing upon the concept of a 'constructive' theory
is deep-rooted in our dependence on Aristotle's logic of predicates which,
whilst allowing us the luxury of expressing the most subjectively conceived
of our abstract concepts not only in languages of common discourse such as
English, but also in mathematical languages such as ZF, is inadequate for
ensuring that that which we express in the most basic of our mathmatical
languages, namely Peano Arithmetic, can be communicated effectively and
unambiguously.

That a sound interpretation of Peano Arithmetic exists - moreover, one that
allows us to communicate effectively and unambiguously - is indicated by the
fact that we unhesitatingly entrust our lives each moment of each day to
mechanical and electronic artefacts whose reliability is essentially founded
on the ability of PA to admit unambiguous and effective communication.

Accordingly, in a recently arXived paper (link below), I consider a
weakened, finitary, interpretation B (of an omega-inconsistent PA) which
avoids appealing to Aristotlean particularisation in the interpretation of
the existential quantifier, and which is actually implicit in Turing's 1936
analysis of computable functions.

This is the interpretation B of PA obtained if, in Tarski's inductive
definitions---of the satisfaction and truth of the formulas of PA under the
'standard' interpretation S of PA---we apply Occam's razor and weaken the
definition of subjective Tarskian satisfiability by replacing it with an
algorithmically verifiable definition of objective Turing-satisfiability.

Not only is the interpretation sound, but it implies that PA is categorical;
we can thus, in principle, communicate perfectly with technologically
advanced extra-terrestrial intelligences.

http://arxiv.org/PS_cache/arxiv/pdf/0902/0902.1064v3.pdf

Regards,

Bhup

Re: "Kantor dust"

[Greg Meredith]

Dr Johnstone,
Many thanks for the response. A couple of years ago, i did come up with a
scheme for sifting through the widgets generated by the Conway construction.
There's a one-liner translation of the Conway construction into a reflective
process calculus
<http://www.springerlink.com/index/f5547884k02u112q.pdf>[1]. Then,
using the
type schemes devised by Luis
Caires<http://ctp.di.fct.unl.pt/~lcaires/papers/CALCO-Caires-1.0.pdf>
,
you can use behavioral types -- in principle -- to sort through the gadgets
the Conway construction generates.

This idea shares much of the spirit of the work done by Mads Dam on proof
systems for the pi-calculus <http://www.csc.kth.se/~mfd/Papers/pspcl.pdf> in
his examples of logical specifications of process models of the naturals --
though to the best of my knowledge he never applied his ideas to the Conway
construction. i cooked up this hair-brained idea in search of a more natural
typing of a notion of quantity that is grounded in a conception of computing
that i know how to reduce to practice.

Best wishes,

--greg

[1] i'm ignoring a bunch of issues about which domain you use to solve the
domain equations that present the reflective process calculus -- which
impact how wide your summations and parallel compositions can be, which
impact how wide the left and right side of the Conway games can be. But,
therein lies at least on connection to category theory. Be that as i may,
here is the 1-liner translation

[| G |] =
\Sigma_{G^L}  @ [| G^L |] ?(x)(*x | [| G^L |]) | \Sigma_{G^R}  @ [| G^R |]!(
[| G^L |] )

The syntax of the reflective calculus that is the target of this translation
is given below

P,Q ::= 0 | x?A | x!C | *x | P+Q
A ::= (y1,...,yN)P, C ::= (P1,...,PN)
x,y ::= @P

See the link above for a brief account of the calculus and a corresponding
logic.

i should note that the translation is horrifically inefficient and it was
wading through the different optimizations -- while preserving nice
compositional properties of the translation so that the definitions and
proofs given by Conway easily port over through the translation to natural
operations on the process models -- that sapped my motivation.

On Tue, Feb 10, 2009 at 2:18 PM, Prof. Peter Johnstone <
P.T.Johnstone@dpmms.cam.ac.uk> wrote:

> On Tue, 10 Feb 2009, Greg Meredith wrote:
>
>  Categorically minded,
>>
>> Many thanks for an interesting thread! Just out of curiousity, is the
>> Conway
>> construction clearly identified with the Dedekind reals? How does the
>> construction fit into the constructivist debate?
>>
>> Best wishes,
>>
>> --greg
>>
>>  The trouble with the Conway construction is not that it's non-
> constructive, but that it isn't (in any reasonable sense) a
> construction of the reals. If you stop it at the point when it
> finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
> on, then it has also succeeded in constructing lots of non-real
> numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
> do you distinguish the numbers you want from the ones you don't?
>
> I did, in both my first Topos Theory book and the Elephant, borrow
> Conway's recursive definition of multiplication to give a
> constructively valid definition of multiplication for Dedekind reals.
> I'm not aware of anyone else who has done that; but it seems to
> me the only intellectually respectable way to do it.
>
> Peter Johnstone
>

Re: "Kantor dust"

[Vaughan Pratt]

Vaughan Pratt wrote:
> Similar reasoning should also rehabilitate the constructivity of binary
> fractions, where the final coalgebra surely deletes the open set
> separating 0111... from 1000...  Perhaps ASD has something to say about
> this---Paul?

Unfortunately the reasoning is not similar enough to make this work.
The crucial difference is that in the representation of [0,oo) ~
[0,1)[1,2)[2,3)... as N^N, there is no largest element of [0,1) whence
the Scott topology omits the open set separating [0,1) from [1,0).  With
binary fractions however we have two points 0111... and 1000... with
nothing between them and the inequality 0111... < 1000..., which the
Scott topology must respect by preserving the open set separating them.

There is (as far as I'm aware) no such localic alternative of the kind I
was envisaging to either omitting 0111... or identifying it with
1000..., both of which are intrinsically spatial solutions to the
problem of converting Cantor space 2^N to the continuum.  In contrast
the Alexandroff-to-Scott conversion of N^N to the continuum is localic
in character, in that it operates on open sets instead of points.

The crucial difference between classical and sheaf-theoretic toposes is
that localic procedures are meaningless in the former.  The latter
permit the finer distinctions to be drawn that are needed to explicate
constructivity, starting with the distinction between not-not and identity.

(Unlike some other buggy posts of mine that I've been able to retract
before Bob forwarded them to the list, this one went through too
promptly for me to catch it in time.  I made this mistake by incorrectly
visualizing the gap between 0111... and 1000... as though it were the
gap between

     .0 < .01 < .011 < .0111 < ... and ... < .1000 < .100 < .10 < .1

This makes no sense (a) because the finite sequences on the right should
all be identified and (b) there are no finite sequences to begin with,
the binary fractions are properly understood as infinite sequences,
namely maps N --> 2.  The paragraph was an afterthought I tacked on with
insufficient consideration before posting.)

Vaughan Pratt

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Tue, 10 Feb 2009, Vaughan Pratt wrote:

> Apropos of my
>
>>  PS. [...] That said, I would
>>  still like to know whether our final coalgebra, for FX = N x X where x
>>  is "lexicographic product" suitably defined for an NNO N in a topos, is
>>  or is not equally real in these toposes.  If it is then this would be a
>>  situation where apartness is not needed to produce the reals
>>  constructively, presumably contradicting Brouwer.
>
> I returned to this question after a pleasant dinner this evening with
> Sol Feferman, Paul Eklof, and Grisha Mints, and it occurred to me almost
> immediately (my subconscious must have been working on it without my
> permission) that in a topos over any sufficient category of topological
> spaces (not that I have the faintest idea how to make that rigorous), it
> must be the case that the final coalgebra for the functor F described
> above is the "real reals."
>
Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
looks like, it must (thanks to Lambek) be isomorphic to N x itself,
and therefore (since equality for N is decidable) must have lots of
complemented subobjects {0} x itself, {1} x itself, ... The point of
the continuity theorem for functions R --> R is that there are toposes
in which R has *no* nontrivial complemented subobjects -- indeed, in
which the sentence

(\forall S : PR)((\forall x : R)((x \in S) \vee \neg(x\in S))
     \implies ((S = R)\vee (S = \emptyset)))

is valid. This is purely a matter of logic: it has nothing to do with
the order, topological or any other sort of structure carried by
the final coalgebra. So invoking Alexandroff and Scott isn't going to
help at all. The only way to get round it (apart from using glue)
is to replace N by some "nonstandard natural number object" having no
nontrivial complemented subobjects -- but where you get that from, I
don't know.

Peter

Re: "Kantor dust"

[Michael Shulman]

On Tue, Feb 10, 2009 at 4:18 PM, Prof. Peter Johnstone
<P.T.Johnstone@dpmms.cam.ac.uk> wrote:
>> Many thanks for an interesting thread! Just out of curiousity, is
>> the Conway construction clearly identified with the Dedekind reals?
>> How does the construction fit into the constructivist debate?
>
> The trouble with the Conway construction is not that it's non-
> constructive, but that it isn't (in any reasonable sense) a
> construction of the reals. If you stop it at the point when it
> finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
> on, then it has also succeeded in constructing lots of non-real
> numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
> do you distinguish the numbers you want from the ones you don't?

And it isn't just "infinite" and "infinitesimal" numbers like \omega and
1/\omega that come along for the ride, either.  Classically, the copy of
the natural numbers sitting inside the surreal numbers is actually the
*finite ordinal numbers*, and constructively there are many more ordinal
numbers below \omega than there are natural numbers.  For instance,

{ 0 | P }

where P is an undecidable statement, is a perfectly good ordinal
number that lies "somewhere between 0 and 1."

Mike

Re: "Kantor dust"

[Toby Kenney]

On Tue, 10 Feb 2009, Vaughan Pratt wrote:

> As a (surely constructive!) witness to the surjectivity, indeed
> bijectivity, of R,  define the inverse S: [0,oo) --> N^N  of R as
> follows.  (R converts sequences to Reals, which S turns back into
> Sequences.)
>
>   S(x)(0) = floor(x)
>   S(x)(n+1) = S(g(x mod 1))(n)
>
> where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is
> the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition
> of R.
>

The trouble with this is that the floor function isn't constructive - the
question "is x<2" is undecidable in the reals, but decidable in the
natural numbers.

The problem with the obvious definition:
"Take the set of natural numbers below x, and take the join of this set."
is that the natural numbers don't have K~-finite joins, only K-finite
ones.

Incidentally, has anyone looked at semilattices with K~-finite joins? (Or
whatever your favourite notion of finiteness is.) Is there any use for
something like the completion of N under K~-finite joins, other than
allowing us to define the floor function?

Toby

Re: "Kantor dust"

[Vaughan Pratt]

Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT:
> The reason is that you have to know in advance that a binary
> sequence isn't going to end in an infinite string of 1's; by excluding
> those sequences, you make the question "Is x < 1/2?" decidable,
> which is not constructively true of either the Cantor reals or the
> Dedekind reals.

I had always been somewhat dissatisfied intuitively by the idea of
excluding sequences of the form 01111....  It seemed more natural to
identify them with those of the form 10000....  However I just assumed
that these were equivalent approaches.

Your point about making x < 1/2 decidable is a good one.  I'm now
convinced that it is better to identify than delete.  Identification can
be accomplished spatially, but perhaps it is more elegant to do so
localically, namely by removing the open set that separates the two
halves to be glued together.  In a T0 space, doing so will identify the
points anyway.  However in the situation [0,1)[1,2) of my previous
messages where there is no point on the left adjacent to the point 1 on
the right, identification of points is not an option.  The only
remaining concern then is whether there's an open set separating [0,1)
and [1,2).  Finality should eliminate spurious open sets that have no
reason to stick around.

Vaughan

Re: "Kantor dust"

[Vaughan Pratt]

Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT:
> The reason is that you have to know in advance that a binary
> sequence isn't going to end in an infinite string of 1's; by excluding
> those sequences, you make the question "Is x < 1/2?" decidable,
> which is not constructively true of either the Cantor reals or the
> Dedekind reals.

I had always been somewhat dissatisfied intuitively by the idea of
excluding sequences of the form 01111....  It seemed more natural to
identify them with those of the form 10000....  However I just assumed
that these were equivalent approaches.

Your point about making x < 1/2 decidable is a good one.  I'm now
convinced that it is better to identify than delete.  Identification can
be accomplished spatially, but perhaps it is more elegant to do so
localically, namely by removing the open set that separates the two
halves to be glued together.  In a T0 space, doing so will identify the
points anyway.  However in the situation [0,1)[1,2) of my previous
messages where there is no point on the left adjacent to the point 1 on
the right, identification of points is not an option.  The only
remaining concern then is whether there's an open set separating [0,1)
and [1,2).  Finality should eliminate spurious open sets that have no
reason to stick around.

Vaughan

Re: "Kantor dust"

[Vaughan Pratt]

Apropos of my

> PS. [...] That said, I would
> still like to know whether our final coalgebra, for FX = N x X where x
> is "lexicographic product" suitably defined for an NNO N in a topos, is
> or is not equally real in these toposes.  If it is then this would be a
> situation where apartness is not needed to produce the reals
> constructively, presumably contradicting Brouwer.

I returned to this question after a pleasant dinner this evening with
Sol Feferman, Paul Eklof, and Grisha Mints, and it occurred to me almost
immediately (my subconscious must have been working on it without my
permission) that in a topos over any sufficient category of topological
spaces (not that I have the faintest idea how to make that rigorous), it
must be the case that the final coalgebra for the functor F described
above is the "real reals."

The intuitition behind this is that N together with an upper bound
thereon (call it oo) has only two possible T0 topologies whose
specialization order is the standard linear one, namely the Alexandroff
and Scott topologies.  These differ by a single open set, which is
present in the former and absent from the latter.  In the former it
isolates oo from N, in the latter its absence allows oo to link up with
  N in the sense that every ultimately constant function on N must map
oo to the limiting value of that function.

There is a unique map from the Alexandroff to the Scott topology on this
set preserving the NNO structure, and no map back (where would you send
the Alexandroff open witnessing the solitude of oo?).  So in any
competition for a final coalgebra Scott is going to beat Alexandroff.

Now in N^N as a representation of the isomorphism [0,oo) ~
[0,1)[1,2)[2,3)..., the objection that will naturally be raised to any
claim that this could be the continuum is that, even though [0,1)[1,2)
*looks* like it should glue together seamlessly, its implementation in
terms of continued fractions will create a gap between [0,1) and [1,2)
that is not found in the "real reals".  While this gap cannot be used in
the topos Set to distinguish N^N from the Freyd coalgebra, where things
are so discrete that all realizations of the reals suffer from gaps, in
a more topologically sensitive topos it becomes possible to find open
sets willing to testify to these gaps in those cases where insufficient
care has been taken to bump off these witnesses, as surely happens when
one defines N^N naively as simply an exponential.  Implementing the glue
of the Freyd coalgebra via apartness bumps off all such witnesses to the
disconnectedness of the Freyd continuum, making it thus far the sole
survivor in this competition to define the reals constructively.  (If
there is another why isn't it in the Elephant?)

In any topos with sufficiently accommodating open sets as to permit this
Alexandroff-Scott distinction (surely not a tall order given that only
one open set need be removed to pass from Alexandroff to Scott), I claim
that the final coalgebra for the functor Dusko and I exhibited in our
CMCS'99 paper bumps off the Alexandroff open witnessing a gap between
[0,1) and [1,2), where the 1 in [1,2) plays the role of oo in my earlier
discussion of N and oo.

If the topos of sheaves on R, or on whichever essentially small version
of Top Peter Johnstone prefers over R itself, does not result in
removing this open set in a way that leaves no other witnesses to
disconnectedness then I will be bitterly disappointed.

If it does however then we have what as far as I'm aware must be the
first alternative since Brouwer to apartness in formulating the
continuum to the constructive standards set by toposophers.  And
moreover using much older technology than the Freyd coalgebra, namely
good old continuous fractions (done right of course, none of this
antimonotone 1/(1+x) stuff totally disconnecting them).

(How old?  Continued fractions are ancient, appearing in Euclid and no
doubt going back a lot further as with much of Euclidean mathematics.
They are a very natural and convenient way of representing reals, though
with subtleties to trip one up, just as with the Freyd coalgebra.)

Similar reasoning should also rehabilitate the constructivity of binary
fractions, where the final coalgebra surely deletes the open set
separating 0111... from 1000...  Perhaps ASD has something to say about
this---Paul?

Vaughan Pratt

Re: "Kantor dust"

[Toby Bartels]

Steve Stevenson wrote in part:

>Toby Bartels wrote:

>>Floating-point reals have terrible theoretical properties;
>>they're not even a ring (not even classically).
>>This is why even after all of Kahan's good work on algorithms,
>>rounding errors are unavoidable (the "Table-Maker's Dilemma").

>Being left-handed and old, I'll propose in my dotage that we may be
>asking the wrong question. In a rewording, what constructive real
>numbers are there for the purpose of

>1. Being a model of an axiomatic characterization of the reals.
>2  Being usable in supercomputing to compute values needed for modeling
>and simulation.

I would distinguish two slightly different purposes:
1. Being usable in principle to compute values
2. Being usable in practice to compute values needed for modeling, etc.
And I'd say that constructive mathematics is inherently about (1),
although often (and like even classical mathematics, usually best when)
with an eye towards (2).  But (2) itself is something different
(applied mathematics, to give it a name; numerical analysis straddles these.)

Although I've redefined them, I think that this remains true:

>Number 1 requires that we have nice theoretical properties. Number 2
>requires something that is bounded only the dollars and life span. Those
>interested in either purpose have (presumedly) a solution for
>themselves.

Interval arithmetic, despite being more complicated than arithemetic
with either floating-point reals or Dedekind/Cauchy/whatever reals,
is an interesting subject that promises to satisfy both (1)&(2).
This is good for both: good for (1) on the general grounds
that applied mathematics usually leads to good pure mathematics
(especially, but not only, when that mathematics is constructive);
and good for (2) since you'll have theorems that you can be sure of.

>I'm willing to
>live with a demonstrably correct approximation given that we are in an
>uncertain world.

Right, and interval arithmetic promises to get us such approximations.
There's still the question of whether demonstrably correct ones
are actually calculable in practice; that depends on the application.
At some point, you have to go beyond even interval arithmetic
and start dealing with probability distributions as your values,
which is yet more complicated theoretically but matches yet more closely
what one actually has in applications.

I'm not sure how much this has to do with category theory anymore,
but as interval arithmetic is already stretching my expertise,
I don't think that I have much more to say anyway.


--Toby

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Tue, 10 Feb 2009, Greg Meredith wrote:

> Categorically minded,
>
> Many thanks for an interesting thread! Just out of curiousity, is the Conway
> construction clearly identified with the Dedekind reals? How does the
> construction fit into the constructivist debate?
>
> Best wishes,
>
> --greg
>
The trouble with the Conway construction is not that it's non-
constructive, but that it isn't (in any reasonable sense) a
construction of the reals. If you stop it at the point when it
finally constructs the real numbers 1/3, \sqrt{2}, \pi and so
on, then it has also succeeded in constructing lots of non-real
numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how
do you distinguish the numbers you want from the ones you don't?

I did, in both my first Topos Theory book and the Elephant, borrow
Conway's recursive definition of multiplication to give a
constructively valid definition of multiplication for Dedekind reals.
I'm not aware of anyone else who has done that; but it seems to
me the only intellectually respectable way to do it.

Peter Johnstone

Re: "Kantor dust"

[Greg Meredith]

Categorically minded,

Many thanks for an interesting thread! Just out of curiousity, is the Conway
construction clearly identified with the Dedekind reals? How does the
construction fit into the constructivist debate?

Best wishes,

--greg

On Mon, Feb 9, 2009 at 2:47 PM, Prof. Peter Johnstone <
P.T.Johnstone@dpmms.cam.ac.uk> wrote:

> On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
>
>  QUESTION 1: re peter johnstone's
>>
>>  > >   In the topos of sheaves on the real line,
>>> > >   every function from [0,1) to N is constant,
>>> > >   yet there are obviously many other functions from N^N to N.
>>> > >   Thus N^N and [0,1) are not constructively isomorphic as sets,
>>> > >   so there is no way to give N^N the order type of [0,1)
>>> > >   constructively.
>>>
>>
>> are you claiming that this statement is true with respect to every base
>> topos
>> and every real line in it? (the discussion seems to have touched upon the
>> various constructions of the various real lines. it would be nice to know
>> where is the one, over which you build the topos, is coming from.)
>>
>>  That's actually a quote from Toby Bartels, not from me.
> It's a statement about a topos built over the classical topos of sets;
> the argument is a rather ad hoc one, and I'm not sure to what extent
> it's possible to make it constructive. However, as I said elsewhere, I
> prefer to work with the gros topos of spaces (i.e. sheaves on a suitable
> full subcategory of spaces for the coverage consisting of jointly-
> surjective families of open inclusions) and there it's quite clear
> what you need: namely, Heine--Borel (equivalently, exponentiability
> of R in your category of spaces). That's not true in all toposes;
> you could try to get round it by basing your gros topos on locales
> rather than spaces (the locale of formal reals being constructively
> locally compact), but it's not clear (to me, at least) what the
> result would actually mean if you based yourself on a topos where
> the formal reals aren't spatial.
>
>  QUESTION 2: is there a branch of constructivism that would reject as
>> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as
>> the
>> coefficients of continued fractions?
>>
>>  I don't think there is any doubt that the map exists. The problem is
> that,
> for most if not all schools of constructivism, it's wildly non-surjective.
>
> Peter Johnstone
>
>
>
>


-- 
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105

+1 206.650.3740

http://biosimilarity.blogspot.com

Re: "Kantor dust"

[Steve Stevenson]

On Feb 8, 2009, at 7:31 PM, Toby Bartels wrote:

> Steve Stevenson wrote in part:
>
>> How about IEEE 754 reals? They're really "scientific notation".
>> <snip>
>
> Floating-point reals have terrible theoretical properties;
> they're not even a ring (not even classically).
> This is why even after all of Kahan's good work on algorithms,
> rounding errors are unavoidable (the "Table-Maker's Dilemma").
<snip>

Being left-handed and old, I'll propose in my dotage that we may be
asking the wrong question. In a rewording, what constructive real
numbers are there for the purpose of

1. Being a model of an axiomatic characterization of the reals.
2  Being usable in supercomputing to compute values needed for
modeling and simulation.

Number 1 requires that we have nice theoretical properties. Number 2
requires something that is bounded only the dollars and life span.
Those interested in either purpose have (presumedly) a solution for
themselves.

The first fix for number 2 might be to go to interval arithmetic ---
now what do I need to guarantee that the "real number (in 1)" is
trapped between two #2 numbers? Given the bandwidth and memory
capacity, we should be able to do those things worth doing: H5N1
infection prediction, climate modeling, malaria control, food
production ... I'm willing to live with a demonstrably correct
approximation given that we are in an uncertain world.  I'll never get
the exact answer, I'll only get an approximation.

Interval guarantees seems interesting to me.


---
Steve Stevenson

It's not that people don't know, it's so much of what they know ain't
so - Josh Billings.

Re: "Kantor dust"

[Vaughan Pratt]

Prof. Peter Johnstone wrote:
> On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
>> QUESTION 2: is there a branch of constructivism that would reject as
>> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N
>> as the coefficients of continued fractions?
>>
> I don't think there is any doubt that the map exists. The problem is that,
> for most if not all schools of constructivism, it's wildly non-surjective.

There is more than one notion of continued fraction.  I suspect you're
thinking of one of the more commonly used ones, but in the light of
Dusko and my CMCS'99 paper, which talks about a number of notions of
continued fraction, I imagine Dusko had one in mind for which the map is
classically a bijection, and surely should continue to be so for at
least some schools of constructivism.  Let me give a (hopefully) careful
proof of this here.

As I observed in a previous post, the pathological definitions of
"continued fraction" giving the behaviour you may be thinking of are
those whose coinductive step is antimonotone, e.g. via a function from
[0,oo) to (0,1] such as 1/(1+x).  These appear in the literature not
from any desire to be pathological but merely because they tend to be
the first ones that come to mind, and their non-surjectivity is simply
not noticed by the naive programmer.

In contrast, monotone functions from [0,oo) to [0,1) such as x/(1+x) or
2*atan(x)/pi, with respective inverses x/(1-x) and tan(pi*x/2), do not
create this pathology in the continued fractions based on them, and give
rise to maps from N^N to [0,1) and [0,oo) that are not only surjective
but bijective, as well as monotone increasing with respect to the
lexicographic order on N^N.

Let R: N^N --> [0,oo) be the strictly monotone increasing function (with
respect to the lexicographic order on N^N) defined coinductively as

   R(s) = s(0) + f(R(s o succ))

where s: N --> N is a sequence in N^N (a function on N),
f: [0,oo) --> [0,1) is a strictly monotone increasing function, for
example f(x) = x/(1+x), and succ: N --> N is the successor operation of
the NNO N.

As a (surely constructive!) witness to the surjectivity, indeed
bijectivity, of R,  define the inverse S: [0,oo) --> N^N  of R as
follows.  (R converts sequences to Reals, which S turns back into
Sequences.)

   S(x)(0) = floor(x)
   S(x)(n+1) = S(g(x mod 1))(n)

where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is
the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition
of R.

As an aside for any visual thinkers reading this, the picture

   [0,oo)  ~  [0,1)[1,2)[2,3)...

may help.  This splits [0,oo) into N unit intervals each identifiable
with [0,1), each of which is blown back up to [0,oo) (under this
identification) by g(x) = x/(1-x).  The function S: [0,oo) --> N^N
converts nonnegative reals x to sequences of natural numbers by taking
the first element of the sequence to be floor(x), thereby selecting one
of the unit intervals, leaving x mod 1 to be accounted for within that
interval, of type [0,1), which is blown back up to type [0,oo) using g
and then inductively converted to the rest of the sequence by S.  In
this way we drill down into [0,oo) cranking out natural numbers as we
drill progressively deeper.

For the typing N^N --> [0,1) that Dusko asked about, the codomain of R
is easily converted from [0,oo) to [0,1) by composing the monotone
bijection  f : [0,oo) --> [0,1)  with the monotone bijection R : N^N -->
[0,oo) to give a monotone bijection from N^N to [0,1).

In the topos of sheaves on either R itself or the subcategory of Top you
prefer, I am not a topos hacker and have no idea whether there are more
than two functions from N^N to 2 = 1+1 when N^N is defined coinductively
as a final coalgebra (as distinct from being defined simply by
exponentiation, where surely there are more than two such functions).
Toby Bartels claims it's obvious, in which case there should be a short
construction of a nonconstant function from N^N (as a final coalgebra)
to 2 (or to N, the codomain Toby spoke of) in the topos of sheaves on R.
  Toby, what is it?

Vaughan Pratt

PS.  None of this contradicts the point you (PTJ) and Freyd have been
making, since around 2002 apparently, concerning the constructive merits
of apartness as an implementation of the glue used in the Freyd
coalgebra, which I only very belatedly came to appreciate, namely within
the past two days.  In view of this I retract my "The choice of poisons
is therefore manual glue vs. double induction" of last Wednesday.  I am
willing to believe that the Freyd coalgebra with manual glue implemented
via apartness produces the "real reals" in these toposes of sheaves, but
would like eventually to understand why of course.  That said, I would
still like to know whether our final coalgebra, for FX = N x X where x
is "lexicographic product" suitably defined for an NNO N in a topos, is
or is not equally real in these toposes.  If it is then this would be a
situation where apartness is not needed to produce the reals
constructively, presumably contradicting Brouwer.

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Mon, 9 Feb 2009, Dusko Pavlovic wrote:

> QUESTION 1: re peter johnstone's
>
>> > >   In the topos of sheaves on the real line,
>> > >   every function from [0,1) to N is constant,
>> > >   yet there are obviously many other functions from N^N to N.
>> > >   Thus N^N and [0,1) are not constructively isomorphic as sets,
>> > >   so there is no way to give N^N the order type of [0,1)
>> > >   constructively.
>
> are you claiming that this statement is true with respect to every base topos
> and every real line in it? (the discussion seems to have touched upon the
> various constructions of the various real lines. it would be nice to know
> where is the one, over which you build the topos, is coming from.)
>
That's actually a quote from Toby Bartels, not from me.
It's a statement about a topos built over the classical topos of sets;
the argument is a rather ad hoc one, and I'm not sure to what extent
it's possible to make it constructive. However, as I said elsewhere, I
prefer to work with the gros topos of spaces (i.e. sheaves on a suitable
full subcategory of spaces for the coverage consisting of jointly-
surjective families of open inclusions) and there it's quite clear
what you need: namely, Heine--Borel (equivalently, exponentiability
of R in your category of spaces). That's not true in all toposes;
you could try to get round it by basing your gros topos on locales
rather than spaces (the locale of formal reals being constructively
locally compact), but it's not clear (to me, at least) what the
result would actually mean if you based yourself on a topos where
the formal reals aren't spatial.

> QUESTION 2: is there a branch of constructivism that would reject as
> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as the
> coefficients of continued fractions?
>
I don't think there is any doubt that the map exists. The problem is that,
for most if not all schools of constructivism, it's wildly non-surjective.

Peter Johnstone

Re: "Kantor dust"

[Dusko Pavlovic]

hi.

i missed most of this thread, but even this one message that i did catch
raises several questions that i would like to share.

QUESTION 1: re peter johnstone's

>>>  In the topos of sheaves on the real line,
>>>  every function from [0,1) to N is constant,
>>>  yet there are obviously many other functions from N^N to N.
>>>  Thus N^N and [0,1) are not constructively isomorphic as sets,
>>>  so there is no way to give N^N the order type of [0,1) constructively.

are you claiming that this statement is true with respect to every base
topos and every real line in it? (the discussion seems to have touched
upon the various constructions of the various real lines. it would be nice
to know where is the one, over which you build the topos, is coming from.)

QUESTION 2: is there a branch of constructivism that would reject as
non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as
the coefficients of continued fractions?

COMMENT: IF the answer to either of the above questions is NO, then
maybe the tacit

   SLOGAN that "constructively valid" = "true in every topos"

needs to be taken *very carefully*. when we build toposes over classical
universes, then we may be able to force away more than any constructivist
would ever reject. the strict constructivist logics have already been
marginalized as too restrictive; lets not completely bury them just for
the joy of constructing counterexamples.

moreover, EVEN IF the answer to both of the above questions is YES, the
above SLOGAN still does not tell the whole story, IMHO.

the constructivists wanted to make our computations effective. that goal
led to some great philosophical debates in the first half of XX century.

later people built computers and paid lots of programmers to make
computations effective. besides brouwer, and heyting and kolmogorov, maybe
we should admit that people like gosper, and knuth, and dijkstra, and our
own vaughan pratt, also have an idea about what is effectively computable.

peter johnstone points out that the comparison test for the binary reals
(i presume the reals in base 2; there are many other representations, of
course) is undecidable. this actually applies to every base, and even to
the continued fraction representation (because it is irredundant). but in
the practice of effective computations, this is no showstopper. there are
many things that need to be computed with the reals, and no one
representation fits for all purposes. so the statement

> nobody uses the binary reals

probably has more counterexamples than, say, the statement "nobody
uses toposes". even if "the" binary reals were completely wrong.

the study of the various effective algebraic operations on the reals,
always reduced to one binary form or another, goes back at least to gosper
and schroepel, the original "hackers" from the 70s. they were, of course,
aware that the comparison test was undecidable. buyt people prefer to run
a program that may not terminate, or will terminate fast, over a program
guaranteed to terminate between tomorrow and 2 years from now.

gosper's continued fraction representation was improved by jean
vuillemin, who proposed in 1990s a redundant representation, where the
comparison test is decidable. this is what at least some people have
really been using in their real projects, sensitive enough to bring
the chaotic effects of the floating point arithmetic to the surface.

it would be interesting to understand whether the notion of computability
as embodied in toposes is related in some rational way with the notion of
computability as embodied in computers.

-- dusko

Re: "Kantor dust"

[Toby Bartels]

Paul Taylor wrote in part:

>Can anybody point me to a reasoned critique, or justification of the
>view that Cauchy sequences are "more appropriate" for purposes such
>as these?  All that I have ever heard is essentially a condemnation
>of Dedekind for the "heresy" of impredicativity, uncountability,
>non-computability, being a proper class, etc.

>I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of
>Dedekind and Heine--Borel", which I presented as if I were an
>advocate in a court of law.  Several type theorists and constructive
>analysts were present.   Beforehand, I had asked around for a statement
>of "the case against Dedekind", but nobody seemed to be able to state
>it for me.

Besides the case that you present briefly in your slides,
there is this:  The Cauchy reals exist an a Pi-W-pretopos
(equivalently, in a constructive set or type theory
with exponentiation but no power sets or even fullness
and with infinity but no countable choice).
But the Dedekind reals, as far as I can tell, do not;
excluded middle, power sets, fullness, or countable choice
would each do the job, but you need ~something~.
(ASD takes another approach, of course.)

And while I don't know any non-finitist practising constructivists
that doubt all of these, I do know at least one that doubts each.
Thus practising constructivists may happily use the Dedekind reals,
while formalists that want to cover all practising schools
find that they are not quite available in the obvious common denominator.
(Actually, Brouwer intuitionists don't really even accept exponenenation,
although they do accept N^N and AC_00 so do have Cauchy = Dedekind reals.)

I don't find this argument conclusive; the proper course is either
to accept the existence of the Dedekind reals as an axiom
(since everybody believes it, even if for different reasons)
or just to give up on point-set topology and use locales
(although these require subtlety to use predicatively).
But it's there, and it probably explains some logicians' positions.

>However, ASD is a recursively axiomatised and enumerable
>theory.  I don't like the notions of (un)countability or
>(im)predicativity, but, if you must apply them, ASD is countable
>and predicative.

But ASD with the underlying-set axiom is impredicative, yes?

I really like ASD, so don't interpet my post as opposition to your position,
but rather an attempt to clarify what the opposition may be thinking.


--Toby

Re: "Kantor dust"

[Toby Bartels]

Steve Stevenson wrote in part:

>How about IEEE 754 reals? They're really "scientific notation".  There
>has been a tremendous amount of work on them by William Kahan and others
>and now are the standard for the numerical analysis world and computers.
>Since this is the basics for computation, I'd propose that they can be
>tightened up even more to suit constructivist purposes.

Floating-point reals have terrible theoretical properties;
they're not even a ring (not even classically).
This is why even after all of Kahan's good work on algorithms,
rounding errors are unavoidable (the "Table-Maker's Dilemma").

A floating-point real basically consists of a rational number x
together with a rational maximum error e, subject to the condition
that, for some integer n, 10^n x is an integer and e = 10^{-n}/2.
(There is some redundancy in this simplified description.)
This is not acceptable constructively, since one cannot prove
(even with countable choice, impredicative power sets, etc)
that every real number has such a floating-point representation.

At the very least, one must add some epsilon to the maximum e;
to keep it simple, I would set e to 10^{-n} (so that 1.6 is acceptable
as the result of 5/3, although good algorithms would probably give 1.7).
This would remove rounding errors from the Table-Maker's Dilemma.
I believe (but I may be wrong through unfamiliarity with the literature)
that most researchers prefer instead to allow arbitrarily large e,
thus using interval arithmetic, even though this is more complicated.

(Actual implementations of floating-point arithmetic
usually also have maximum allowed values of both n and 10^n x,
leading to rounding errors from underflow and overflow.
However, overflow errors already arise in natural-number arithmetic,
so this is not really the fault of the floating-point idea.
One can delay all such errors until run-time memory limits.)


--Toby

Re: "Kantor dust"

[Steve Stevenson]

On Feb 7, 2009, at 5:58 PM, Toby Bartels wrote:

> Prof. Peter Johnstone wrote in part:
>
>> Vaughan Pratt wrote:
>
>>> Whose reals, Cauchy's or Dedekind's?
>
>> Toby was of course referring to the Dedekind reals

How about IEEE 754 reals? They're really "scientific notation".  There
has been a tremendous amount of work on them by William Kahan and
others and now are the standard for the numerical analysis world and
computers. Since this is the basics for computation, I'd propose that
they can be tightened up even more to suit constructivist purposes.

Steve
--------
D. E. Stevenson, Department of Computer Science
Director, Institute for Modeling and Simulation Applications
Clemson University, Clemson, SC 29634-0974

Re: "Kantor dust"

[Paul Taylor]

There have been several very interesting comments on this thread,
but I would like to repeat my request that people should be clear
about
      WHICH OF MANY "CONSTRUCTIVE" THEORIES OF MATHEMATICS
they mean as the context of their comments.   There are, as I said,
interesting mathematical points to be made, both within each of
these theories, and by comparing them.  However, without a clear
statement of the foundational context, the discussion degenerates.

The original question was about Cantor space, rather than either
the Cauchy or Dedekind reals.  If you want to construct Cantor space
from the reals by the "missing third" construction,  I would think
that it makes little difference whether you start from Cauchy or
Dedekind.  Or, indeed, from binary sequences, which of course form
a Cantor space in the first place, so that is really a question of
how to construct the reals from Cantor space rather than vice versa.

Vaughan Pratt said
> between Dedekind cuts and Cauchy sequences, the more appropriate notion
> of reals for constructive analysis would surely be the Cauchy reals
and I am certainly aware that, as a sociological fact, many type
theorists and exact real arithmetic programmers believe this.

Can anybody point me to a reasoned critique, or justification of the
view that Cauchy sequences are "more appropriate" for purposes such
as these?  All that I have ever heard is essentially a condemnation
of Dedekind for the "heresy" of impredicativity, uncountability,
non-computability, being a proper class, etc.

I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of
Dedekind and Heine--Borel", which I presented as if I were an
advocate in a court of law.  Several type theorists and constructive
analysts were present.   Beforehand, I had asked around for a statement
of "the case against Dedekind", but nobody seemed to be able to state
it for me.

Five years ago I had no opinion whatever on these matters, but, as you
gather, I now consider that both Dedekind completeness and the Heine--
Borel theorem are essential parts of "constructive" analysis.  Of
course, I think that because the reals in Abstract Stone Duality
satisfy them  (and because it puts me in agreement with mainstream
analysts).   However, ASD is a recursively axiomatised and enumerable
theory.   I don't like the notions of (un)countability or
(im)predicativity, but, if you must apply them, ASD is countable
and predicative.

Regarding computation,  last year Andrej Bauer gave a "proof of concept"
demonstration that one can compute efficiently with Dedekind reals
in the ASD language for R.  This of course uses interval arithmetic,
but in fact it also makes extremely novel use of back-to-front
("Kaucher") intervals, which appear but are very badly presented
in the interval analysis literature.   I have been trying to persuade
him to make this work publicly available.

Since I'm talking about the reals in ASD, I should say what the
difference is between the Cauchy and Dedekind reals is there.
I haven't actually written out a construction of the Cauchy reals,
but the evidence that I do have is that THEY ARE THE SAME.   More
precisely, Dedekind completeness is inter-derivable with sobriety
for R, just as definition by description is equivalent to sobriety
of N.   This means that if you construct the "Cauchy reals" as a
quotient of Cantor space by an equivalence relation (this is known
as the "signed binary" representation of reals) within ASD then
the result will be Dedekind complete.   The details of this are
set out in Section 14 of "The Dedekind reals in ASD" by Andrej and me,
www.PaulTaylor.EU/ASD/dedras

I think it is worth making a note of Vaughan's earlier comment that
> In concrete Stone duality, increasing structure on one side is offset
> by
> decreasing structure on the other.  One would hope for a similar
> phenomenon in abstract Stone duality.
>
> If we can consider constructivity as part of the structure of an
> object,
> then we should expect that the more constructive some type of object,
> the less constructive the "object of all objects of that type."   So
> for
> example if (total) recursive functions are demonstrably more
> constructive than partial recursive functions by some criterion, we
> should expect the set of all recursive functions to be *less*
> constructive than that of partial recursive functions by the same
> criterion, rather than more.
>
> The phenomena you're observing here seem entirely consistent with this
> principle, and point up the need to be clear, when judging
> constructivity in some context, whether it is the collection or the
> individuals therein being so judged, with the added complication that
> Stone duality makes the roles of collection and individual therein
> interchangeable, such as when elements of sets are understood as
> ultrafilters of Boolean algebras.

However, I think that the Galois--Stone contravariance applies WITHIN
a particular foundational system, and not to VARIATIONS of the degree
of constructivity.  Indeed, the usual experience in setting up a
Galois connection or Stone adjunction is that, in order to make the
comparison work at all, you need to make additional assumptions.

Paul Taylor

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Sat, 7 Feb 2009, Toby Bartels wrote:

>> Toby was of course referring to the Dedekind reals
>
> Actually, I was trying to keep it open,
> since different schools of constructivism have different opinions
> about which are the correct reals (as well as which are equivalent).
> But nobody uses the binary reals, since they can't subtract them.

Never mind subtraction -- you can't even add them. As I mentioned in my
last posting, the question "Is x < 1/2?" is decidable for Vaughan's binary
reals, but "Is x < 1/3?" is not (constructively), so the operation
of adding 1/6 can't be defined.

Peter Johnstone

Re: "Kantor dust"

[gcuri]

Quoting "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>:

> > If the latter then that's no
> > surprise---carrying out constructions with open order filters is less
> > constructive than with the Cauchy sequence concept.  Lubarsky and
> > Rathien in Logic and Analysis 1:2 131-152 have recently made the point
> > that whereas Cauchy reals can be understood constructively as a set, any
> > attempt to make Dedekind's reals constructive turns them into a proper
> > class.
> >
> > Between Dedekind cuts and Cauchy sequences, the more appropriate notion
> > of reals for constructive analysis would surely be the Cauchy reals.
>
> I could take issue with you on this. If you insist that "constructive"
> entails "predicative", then you are  of course right; but in a topos-
> theoretic context, where you don't have countable choice automatically
> available, it's very much the other way round.


Even if one insists that constructive entails predicative the appropriateness of
Cauchy reals is questionable: Lubarsky and Rathjen prove in fact that in a 
subsystem of CZF (Aczel' constructive set theory), i.e., in CZF with
Subset Collection replaced by exponentiation, the Dedekind reals  form a proper
class.
In ordinary CZF (that has no choice principle and no powersets),
the Dedekind reals *do* form a set (Aczel & Rathjen), as do more generally the
points of any weakly set-presented T^*_1 locale (Aczel & Curi),
in particular of any locally compact regular one.

It is also useful to recall that (in "On the Cauchy Completeness of the
Constructive Cauchy Reals", MLQ, 53, No. 4-5 (2007), pp. 396-414)
Lubarsky has  proved that the Cauchy Reals are not complete in intuitionistic
set theory without choice.

There's then the point of view that, constructively, the reals should be
considered as a `space', rather than a set, and that in this perspective they
are more properly regarded e.g. as a locale/formal space (rather than as a
set/class of points with a topology)...

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

Re: "Kantor dust"

[Toby Bartels]

Prof. Peter Johnstone wrote in part:

>Vaughan Pratt wrote:

>>Whose reals, Cauchy's or Dedekind's?

>Toby was of course referring to the Dedekind reals

Actually, I was trying to keep it open,
since different schools of constructivism have different opinions
about which are the correct reals (as well as which are equivalent).
But nobody uses the binary reals, since they can't subtract them.
(To get the first digit of 0.1000000000... - 0.01000000000...,
you need to know which sequence, if either, stops repeating first.)
I agree that one would default to Dedekind reals (or something equivalent),
since that seems to be agreed on by the "practising" schools
(that is, those constructivists trying to do ordinary mathematics,
 albeit constructively, rather than doing metamathematics).

>>Lubarsky and
>>Rathien in Logic and Analysis 1:2 131-152 have recently made the point
>>that whereas Cauchy reals can be understood constructively as a set, any
>>attempt to make Dedekind's reals constructive turns them into a proper
>>class.

I'll have to read what they mean, but to say ~any~ attempt seems too strong.
Even in a predicative theory, countable choice implies their equivalence,
so are they claiming that countable choice is not constructive?
(In my experience, Fred Richman is the only practising non-finitist analyst
 who doubts both excluded middle and countable choice.)
The Dedekind reals can also be constructed in CZF
(Peter Aczel's predicative constructive set theory)
even if you remove countable choice, using subset collection aka fullness.
Similarly, if you remove identity types from intensional type theory
(so breaking the justification of countable choice),
you can still justify the fullness axiom and so construct the Dedekind reals
(albeit not literally as sets of rational numbers).

>>Between Dedekind cuts and Cauchy sequences, the more appropriate notion
>>of reals for constructive analysis would surely be the Cauchy reals.

The experience in measure theory and Banach space theory since the 1980s
suggests that a Dedekind-complete ordered field is needed.
The only question is whether such a thing exists; most believe it does.
(If countable choice or excluded middle holds, the Cauchy reals work,
 which takes care of nearly every practising analyst, constructive or not.
 Fred Richman, the only exception I know, still uses the Dedekind reals,
 although that's easy for him since he is not predicativist.)

Note: everything above is about the ~located~ Dedekind reals;
a located Dedekind cut is a pair (L,U) of order-open inhabited sets
such that r in L and s in U => r < s => r in L or s in U.
This is what Freyd's coalgebra construction produces,
and it's what practising analysts want to use.


--Toby

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Fri, 6 Feb 2009, Vaughan Pratt wrote:
>
> Toby Bartels wrote:
>>  But it's not a constructive theorem that every such x has a binary
>>  expansion.
>>  That's still a neat result, that the binary reals are given by N^N,
>>  but the binary reals aren't constructively the same as the reals.
>
> Whose reals, Cauchy's or Dedekind's?

Toby was of course referring to the Dedekind reals, but your binary
reals are not constructively either the Cantor or the Dedekind reals.
The reason is that you have to know in advance that a binary
sequence isn't going to end in an infinite string of 1's; by excluding
those sequences, you make the question "Is x < 1/2?" decidable,
which is not constructively true of either the Cantor reals or the
Dedekind reals.

> If the latter then that's no
> surprise---carrying out constructions with open order filters is less
> constructive than with the Cauchy sequence concept.  Lubarsky and
> Rathien in Logic and Analysis 1:2 131-152 have recently made the point
> that whereas Cauchy reals can be understood constructively as a set, any
> attempt to make Dedekind's reals constructive turns them into a proper
> class.
>
> Between Dedekind cuts and Cauchy sequences, the more appropriate notion
> of reals for constructive analysis would surely be the Cauchy reals.

I could take issue with you on this. If you insist that "constructive"
entails "predicative", then you are  of course right; but in a topos-
theoretic context, where you don't have countable choice automatically
available, it's very much the other way round.
>>
>>  In the topos of sheaves on the real line,
>>  every function from [0,1) to N is constant,
>>  yet there are obviously many other functions from N^N to N.
>>  Thus N^N and [0,1) are not constructively isomorphic as sets,
>>  so there is no way to give N^N the order type of [0,1) constructively.
>
> Let's compare apples with apples here.  There are presumably going to be
> nonconstant *functions* from the Freyd coalgebra object to 2 in this
> topos, although they won't be continuous with respect to the topology
> induced on that object by its coalgebra structure.

No -- that's the whole point. In the topos of sheaves on R (better, in
the gros topos of sheaves on topological spaces) every function
R --> R is continuous, hence every function [0,1] --> 2 is constant.

Peter Johnstone

Re: "Kantor dust"

[Vaughan Pratt]

Toby Bartels wrote:
> But it's not a constructive theorem that every such x has a binary expansion.
> That's still a neat result, that the binary reals are given by N^N,
> but the binary reals aren't constructively the same as the reals.

Whose reals, Cauchy's or Dedekind's?     If the latter then that's no
surprise---carrying out constructions with open order filters is less
constructive than with the Cauchy sequence concept.  Lubarsky and
Rathien in Logic and Analysis 1:2 131-152 have recently made the point
that whereas Cauchy reals can be understood constructively as a set, any
attempt to make Dedekind's reals constructive turns them into a proper
class.

Between Dedekind cuts and Cauchy sequences, the more appropriate notion
of reals for constructive analysis would surely be the Cauchy reals.
Are these constructively different from the binary reals?  And if so, is
there any intuition underlying that difference that is as clear-cut as
the difference between either and the Dedekind reals?

>
>> is there a topos in
>> which the order type of the Freyd coalgebra is not that of the (forward)
>> lexicographic ordering of N^N (modulo endpoints)?
>
> In the topos of sheaves on the real line,
> every function from [0,1) to N is constant,
> yet there are obviously many other functions from N^N to N.
> Thus N^N and [0,1) are not constructively isomorphic as sets,
> so there is no way to give N^N the order type of [0,1) constructively.

Let's compare apples with apples here.  There are presumably going to be
nonconstant *functions* from the Freyd coalgebra object to 2 in this
topos, although they won't be continuous with respect to the topology
induced on that object by its coalgebra structure.  But neither will the
nonconstant functions from N^N to N be continuous with respect to the
order interval topology on N^N lexicographically ordered.  So I don't
see any progress here towards distinguishing the order type of the Freyd
coalgebra from the lexicographic order on N^N, in this topos or any other.

Vaughan Pratt

Re: "Kantor dust"

[Toby Bartels]

Vaughan Pratt wrote in part:

>Prof. Peter Johnstone wrote:

>>How do you (constructively) give N^N the order type of the nonnegative
>>reals?

>One way to see this is to replace the 0's in the usual binary expansion
>of x \in [0,1) by commas and read the resulting comma-separated blocks
>of 1's as tally notation.

But it's not a constructive theorem that every such x has a binary expansion.
That's still a neat result, that the binary reals are given by N^N,
but the binary reals aren't constructively the same as the reals.

>is there a topos in
>which the order type of the Freyd coalgebra is not that of the (forward)
>lexicographic ordering of N^N (modulo endpoints)?

In the topos of sheaves on the real line,
every function from [0,1) to N is constant,
yet there are obviously many other functions from N^N to N.
Thus N^N and [0,1) are not constructively isomorphic as sets,
so there is no way to give N^N the order type of [0,1) constructively.


--Toby

Re: "Kantor dust"

[Vaughan Pratt]

Prof. Peter Johnstone wrote:
> On Mon, 2 Feb 2009, Vaughan Pratt wrote:
>
>> How about the converse: does N entail K?  In any topos with NNO N the
>> underlying object of the final coalgebra of FX = X+X is presumably 2^N.
>>  Does the Elephant prove that 2^N can be made a final coalgebra of X+X?
>>
> It's not in the Elephant; but it's an easy exercise in primitive
> recursion, given a coalgebra structure X \to X + X, to define the
> transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N.

Ah, good, thanks.  In that case it should be almost as easy, given a
suitably "easy" coalgebra structure X --> N x X, to define the transpose
N x X --> N of the unique coalgebra morphism X --> N^N.

> How do you (constructively) give N^N the order type of the nonnegative
> reals?

The easiest one is forward lexicographic order (s < t when s(i) < t(i)
at the least i where distinct sequences s and t differ), which has the
order type of [0,oo), equivalently [0,1).

One way to see this is to replace the 0's in the usual binary expansion
of x \in [0,1) by commas and read the resulting comma-separated blocks
of 1's as tally notation.

Alternatively, any monotone bijection f: [0,oo) --> [0,1), such as
x/(x+1) giving one kind of continued fraction, or 2*atan(x)/pi for
"circular continued fractions", induces the monotone bijection
R: N^N --> [0,oo) defined coinductively as

   R(s) = s(0) + f(R(s o succ)).

These are among the coalgebraic presentations of the reals Dusko
Pavlovic and I spoke about in Amsterdam on 3/20/99 at CMCS, see ENTCS
19, 133-147 (1999), journal version TCS 280(1-2):105-122 (2002).

> I know how to give it the order type of the irrationals, but
> that's still zero-dimensional.

Reverse lexicographic order gives the irrationals, and is the one
usually encountered with the continued fractions used by "spigot
algorithm" programmers such as Bill Gosper, who don't seem to mind that
the space they're working in is totally disconnected.  This results from
not bothering to correct for the antimonotonicity of 1/(x+1).  Pedantic
spigot programmers who prefer working in a connected space can easily
substitute its monotonic complement, 1-1/(x+1) = x/(x+1), but
(digressing from mathematical reality for a moment) to what practical
advantage?  Presumably Brouwer would take Gosper's side here, it's not
as if the real line is going to crumble into dust when it becomes
totally disconnected by omitting a countable subset, it's still held
together by its metric.  Nature abhors topology.  A demonstrably
nondiscrete Hausdorff space in either nature or computer engineering
would be a great discovery worthy of the Nobel prize in physics or the
Turing award respectively.

Back to mathematical reality.

> However, Freyd's presentation of the
> real unit interval as a final coalgebra is done constructively (for any
> topos with NNO) in the Elephant, D4.7.17.

Freyd's post of 12/22/99 to this list introducing his presentation,

   http://north.ecc.edu/alsani/ct99-00(8-12)/msg00039.html

gives the general provenance for the coalgebraic approach to the reals
as our CMCS paper.  Our respective approaches to connecting up the bits
of our coalgebras to form a continuum differ mainly in that Peter
explicitly glues the abutting ends of 2xX ~ X+X together while we
exploit the open-ended nature of N (least but no greatest element, as
the discretization of a half-open interval) for a glue-less connection
at the expense of the additional induction needed when replacing 2 by N.
  The choice of poisons is therefore manual glue vs. double induction.

In light of your remark at the start of D4.7 that "there are different
constructions of the reals which are classically equivalent but may
yield different results in a non-Boolean topos," is there a topos in
which the order type of the Freyd coalgebra is not that of the (forward)
lexicographic ordering of N^N (modulo endpoints)?  Are they the same in
Grph, for example?

Vaughan Pratt

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Mon, 2 Feb 2009, Vaughan Pratt wrote:

> How about the converse: does N entail K?  In any topos with NNO N the
> underlying object of the final coalgebra of FX = X+X is presumably 2^N.
>  Does the Elephant prove that 2^N can be made a final coalgebra of X+X?
>
It's not in the Elephant; but it's an easy exercise in primitive
recursion, given a coalgebra structure X \to X + X, to define the
transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N.

> And if so, what other coalgebras are brought into existence by N?  For
> example can N^N be made a doubly inductive (inductive-coinductive)
> coalgebra encoding the lexicographic order that gives N^N the order type
> of the nonnegative reals?  That would give a pretty direct construction
> of the usual topology of the real line in any topos with NNO.  (This is
> the one-dimensional conception of the continuum, as opposed to the
> zero-dimensional conception preferred by descriptive set theorists, who
> take the continuum to be N^N with the ordinary product topology.)
>
How do you (constructively) give N^N the order type of the nonnegative
reals? I know how to give it the order type of the irrationals, but
that's still zero-dimensional. However, Freyd's presentation of the
real unit interval as a final coalgebra is done constructively (for any
topos with NNO) in the Elephant, D4.7.17.

Peter Johnstone

Re: "Kantor dust"

[Vaughan Pratt]

Prof. Peter Johnstone wrote:
> A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X)
> necessarily has a natural number object. Observe that the Cantor set K
> necessarily has a point (since 1 has an F-coalgebra structure), so the
> isomorphism K+K \cong K yields a monomorphism K \to K and a point
> disjoint from its image. From there on, use Corollary D5.1.3 in the
> Elephant.

Oh, of course: pick a point out of one half and recurse on the other.
Very plausible that that would work in any topos, but it's great to be
able to stare at an actual proof.  Thank you!

How about the converse: does N entail K?  In any topos with NNO N the
underlying object of the final coalgebra of FX = X+X is presumably 2^N.
  Does the Elephant prove that 2^N can be made a final coalgebra of X+X?

And if so, what other coalgebras are brought into existence by N?  For
example can N^N be made a doubly inductive (inductive-coinductive)
coalgebra encoding the lexicographic order that gives N^N the order type
of the nonnegative reals?  That would give a pretty direct construction
of the usual topology of the real line in any topos with NNO.  (This is
the one-dimensional conception of the continuum, as opposed to the
zero-dimensional conception preferred by descriptive set theorists, who
take the continuum to be N^N with the ordinary product topology.)

Does \Omega^N as the final coalgebra for FX = \Omega x X ever arise in
practical situations where \Omega is more than just a pointed version of
1+1 as in Set, e.g. graph theory?

Vaughan Pratt

Re: "Kantor dust"

[Prof. Peter Johnstone]

On Sat, 31 Jan 2009, Vaughan Pratt wrote:

> I'm not aware of any reason why a topos with a Cantor set object K has
> to also have a natural number object N, though I'm not enough of a topos
> hacker myself to know how to produce one with K but without N (but would
> be happy to learn).  Does such a topos exist in nature?  And what can be
> said of the free topos with Cantor set object?
>
A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X)
necessarily has a natural number object. Observe that the Cantor set K
necessarily has a point (since 1 has an F-coalgebra structure), so the
isomorphism K+K \cong K yields a monomorphism K \to K and a point
disjoint from its image. From there on, use Corollary D5.1.3 in the
Elephant.

Peter Johnstone

Re: "Kantor dust"

[Vaughan Pratt]

Galchin, Vasili wrote:
> i.e. a well-defined algorithm exists to construct Cantor dust but the Cantor
> dust cannot be constructed/built from the algorithm in a finite number of
> steps. Hence, Cantor dust represents potential infinity rather than actual
> infinity. This problem has nagged at me for a while.


Bill, if you mean this literally then you don't accept the existence of
the set N of natural numbers either.  If that's the case then for you it
is very reasonable to reject the Cantor set K as well, e.g. because
you're a finitist as Bas Spitters suggests.

However if you're ok with the idea of a natural numbers object N in a
topos, defined as an initial algebra for the functor F(X) = X+1, then
you would need to draw a fairly fine line to reject as nonconstructive a
Cantor set object K in a topos, defined as a final coalgebra for the
functor F(X) = 2X (~ X+X, 2 being 1+1 in a topos).

 From this standpoint the existence of a Cantor set object is more
plausible than a continuum object rather than less because more is
needed.  If you go with the double-induction approach of Pavlovic and
Pratt, where the functor is F(X) = NX (~ X+X+X+...) then the topos needs
a natural numbers object.  If instead you go with Freyd's
single-induction approach of connecting up (eliminating the gap between)
the two halves of K+K, as preferred e.g. by Tom Leinster, then the topos
needs structure sufficient tfor such gluing.

I'm not aware of any reason why a topos with a Cantor set object K has
to also have a natural number object N, though I'm not enough of a topos
hacker myself to know how to produce one with K but without N (but would
be happy to learn).  Does such a topos exist in nature?  And what can be
said of the free topos with Cantor set object?

Vaughan Pratt

Re: "Kantor dust"

[spitters]

It seems that what you are describing is usually called finitism.

Bas


On Saturday 31 January 2009 05:35:41 Galchin, Vasili wrote:
> i.e. a well-defined algorithm exists to construct Cantor dust but the
> Cantor dust cannot be constructed/built from the algorithm in a finite
> number of steps. Hence, Cantor dust represents potential infinity rather
> than actual infinity. This problem has nagged at me for a while.
>
> Regards, Vasili
>

Re: "Kantor dust"

[Galchin, Vasili]

i.e. a well-defined algorithm exists to construct Cantor dust but the Cantor
dust cannot be constructed/built from the algorithm in a finite number of
steps. Hence, Cantor dust represents potential infinity rather than actual
infinity. This problem has nagged at me for a while.

Regards, Vasili

On Fri, Jan 30, 2009 at 4:40 PM, Galchin, Vasili <vigalchin@gmail.com>wrote:

> I don't think it exists from a constructivist viewpoint because it has to
> be constructed in a finite number of steps.
>
> Vasili
>
> On Fri, Jan 30, 2009 at 3:52 PM, Bas Spitters <spitters@cs.ru.nl> wrote:
>
>> On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
>> >       Here is a definition of Cantor dust ....
>> > http://en.wikipedia.org/wiki/Cantor_set.
>> >
>> >       My question is from a constructivist viewpoint does this set
>> really
>> > exist and if so, why?
>>
>> Yes, it exists. In fact, it is a continuous image of 2^N.
>> It is Bishop compact, fan-like and compact overt (choose your taste of
>> constructivism).
>>
>> Bas
>>
>>
>

Re: "Kantor dust"

[Galchin, Vasili]

I don't think it exists from a constructivist viewpoint because it has to be
constructed in a finite number of steps.

Vasili

On Fri, Jan 30, 2009 at 3:52 PM, Bas Spitters <spitters@cs.ru.nl> wrote:

> On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
> >       Here is a definition of Cantor dust ....
> > http://en.wikipedia.org/wiki/Cantor_set.
> >
> >       My question is from a constructivist viewpoint does this set really
> > exist and if so, why?
>
> Yes, it exists. In fact, it is a continuous image of 2^N.
> It is Bishop compact, fan-like and compact overt (choose your taste of
> constructivism).
>
> Bas
>
>

Re: "Kantor dust"

[Bas Spitters]

On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
>       Here is a definition of Cantor dust ....
> http://en.wikipedia.org/wiki/Cantor_set.
>
>       My question is from a constructivist viewpoint does this set really
> exist and if so, why?

Yes, it exists. In fact, it is a continuous image of 2^N.
It is Bishop compact, fan-like and compact overt (choose your taste of
constructivism).

Bas

"Kantor dust"

[Galchin, Vasili]

[Note from moderator: this may have been sent incorrectly earlier,
apologies if you have received it twice.]

Dear Category group,

      Here is a definition of Cantor dust ....
http://en.wikipedia.org/wiki/Cantor_set.

      My question is from a constructivist viewpoint does this set really
exist and if so, why?

Very kind regards,

Vasili

"Kantor dust"

[Galchin, Vasili]

[-- Attachment #1: Type: multipart/alternative, Size: 238 bytes --]